proposition: Lemma Exercise3_6 E: exists X, sub X E /\ ~ (inc X E).
proof: Proof. ex_middle bad. have bad1: sub (\Po E) E. by move=> t /setP_P tE; ex_middle te1; case: bad; exists t. have eq1: \2c ^c (cardinal E) = cardinal (\Po E). by rewrite card_setP; apply: cpow_pr; aw. move: (cantor (CS_cardinal E)); rewrite eq1=> le1. by move: (cltNge le1 (sub_smaller bad1)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)