proposition: Lemma Strict_Included_inv : forall X Y:Ensemble U, Strict_Included U X Y -> Included U X Y /\ Inhabited U (Setminus U Y X).
proof: Proof. intros X Y H'; red in H'. split; [ tauto | idtac ]. elim H'; intros H'0 H'1; try exact H'1; clear H'. apply Strict_super_set_contains_new_element; auto with sets. Qed.
imports: Ensembles Constructive_sets Classical