proposition: Lemma sup_M_in_B : In B (|_| M).
proof: Proof. rewrite <- im_U_f. case f_cont. intros H [H0 H1]. rewrite H1; auto. - apply H. apply H0. + apply Inc_U_A. + apply inh_U. + apply den_U. - apply Inc_U_A. - apply inh_U. - apply den_U. Qed.
imports: ZornsLemma(CountableTypes)