proposition: Lemma Strict_Included_char {X : Type} (U V : Ensemble X) : Strict_Included U V <-> (Included U V /\ exists x, In V x /\ ~ In U x).
proof: Proof. split. - intros [H0 H1]. split; auto. apply NNPP. intros Hn. contradict H1. apply Extensionality_Ensembles; split; auto; clear H0. intros x HVx. apply NNPP. intros HUx. contradict Hn. exists x; split; auto. - intros [H0 H1]. split; auto. intros ?; subst. destruct H1 as [? []]; auto. Qed.
imports: ZornsLemma(FunctionProperties) Coq(RelationClasses)