proposition: Lemma epsilon_fam_pr7 C (E := cnext C) (F:= Zo E epsilonp) : infinite_c C -> cardinal E = cardinal F.
proof: Proof. move /epsilon_fam_pr6; rewrite -/F -/E; move => [_ _ [bf _ _] _]. apply /card_eqP; exists (Lf epsilon_fam E F); saw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)