proposition: Lemma not_SIncl_full {X : Type} (U : Ensemble X) : ~ Strict_Included Full_set U.
proof: Proof. intros ?. destruct H. apply H0. extensionality_ensembles; try constructor. apply H. constructor. Qed.
imports: ZornsLemma(FunctionProperties) Coq(RelationClasses)