proposition: Corollary Strict_Included_Union_r {X : Type} (U V : Ensemble X) : Strict_Included V (Union U V) -> exists x : X, In U x /\ ~ In V x.
proof: Proof. rewrite Union_commutative. apply Strict_Included_Union_l. Qed.
imports: ZornsLemma(FunctionProperties) Coq(RelationClasses)