proposition: Lemma Setminus_Included_empty: forall A s1 s2, Included A s1 s2 -> Setminus A s1 s2 = Empty_set A.
proof: Proof. intros. apply Extensionality_Ensembles. split. * intros x H1. inversion_clear H1. contradiction H2. intuition. * intuition. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset