proposition: Lemma Exercise34b b: cardinalp b -> let B := Zo E (fun x => forall X, inc X (finv x) -> nonempty X -> cardinal X <=c b) in cardinal B <=c b.
proof: Proof. set B := Zo _ _ => cp /=. case: (emptyset_dichot B). by move ->; rewrite cardinal_set0; apply: cle0x. move => neb. have BE: sub B E by apply: Zo_S. move: (choice BE neb) => /Zo_P [ha hb]; apply: hb => //. by apply /Zo_P; split => //; apply/setP_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)