proposition: Lemma Strict_super_set_contains_new_element : forall X Y:Ensemble U, Included U X Y -> X <> Y -> Inhabited U (Setminus U Y X).
proof: Proof. auto 7 using Inhabited_Setminus with sets. Qed.
imports: Ensembles Constructive_sets Classical