proposition: Remark ge_zero : (ge zero : Ensemble Ord) = ordinal.
proof: Proof. Proof with eauto with schutte. apply Extensionality_Ensembles. split. + red; split. + unfold ge ... Qed.
imports: Coq(Arith Logic.Epsilon Ensembles) ZornsLemma(CountableTypes)