proposition: Corollary Strict_Included_Union_l {X : Type} (U V : Ensemble X) : Strict_Included U (Union U V) -> exists x : X, In V x /\ ~ In U x.
proof: Proof. rewrite Strict_Included_char. intros [H0 [x [Hx0 Hx1]]]. destruct Hx0 as [x Hx0|x Hx0]; try contradiction. exists x; split; auto. Qed.
imports: ZornsLemma(FunctionProperties) Coq(RelationClasses)