proposition: Lemma complement_inclusion: forall {Y:Type} (S T:Ensemble Y), Included S T -> Included (Complement T) (Complement S).
proof: Proof. intros. red. intros. intro. contradiction H0. auto with sets. Qed.
imports: ZornsLemma(EnsemblesTactics Powerset_facts)