proposition: Lemma not_SIncl_empty : forall X:Ensemble U, ~ Strict_Included U X (Empty_set U).
proof: Proof. intro X; red; intro H'; try exact H'. lapply (Strict_Included_inv X (Empty_set U)); auto with sets. intro H'0; elim H'0; intros H'1 H'2; elim H'2; clear H'0. intros x H'0; elim H'0. intro H'3; elim H'3. Qed.
imports: Ensembles Constructive_sets Classical