proposition: Lemma proper_members (A: Ensemble Ord) (H : proper_segment A) : exists a: Ord, Same_set A (members a).
proof: Proof. Proof with eauto with schutte. case (not_all_not_ex _ (fun b => ordinal b /\ ~ A b)). - intro H1; apply H;split. + unfold Included; split; auto. + intros x H2; apply NNPP; intro H3. apply (H1 x); split;auto. - intros x H1; case (@well_order _ lt AX1 (fun x => ordinal x /\ ~ A x) x). + auto. + intros y Hy. case Hy;intros H2 H3; destruct H2. exists y;split... * intros a H6; tricho a y T ... case H;auto. subst a; contradiction. red in Hy. destruct Hy. destruct H. red in H. specialize (H a y H6 T). contradiction. * red; unfold In;intros; apply NNPP. case Hy; intros H7 H8 H10. case (H8 x0 ). { red; split ... } { intro; subst. destruct (lt_irrefl H4). } intro; case (@lt_irrefl x0); apply lt_trans with y ... Qed.
imports: ZornsLemma(CountableTypes)