proposition: Lemma less_than_singleton : forall (X:Ensemble U) (x:U), Strict_Included U X (Singleton U x) -> X = Empty_set U.
proof: Proof. intros X x H'; try assumption. red in H'. lapply (Singleton_atomic x (Full_set U)); [ intro H'2; try exact H'2 | apply Full_intro ]. elim H'; intros H'0 H'1; try exact H'1; clear H'. elim (setcover_inv (Full_set U) (Empty_set U) (Singleton U x)); [ intros H'6 H'7; try exact H'7 | idtac ]; auto with sets. elim (H'7 X); [ intro H'5; try exact H'5 | intro H'5 | idtac | idtac ]; auto with sets. elim H'1; auto with sets. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset Powerset_facts Classical Classical_sets