proposition: Lemma less_than_empty : forall X:Ensemble U, Included U X (Empty_set U) -> X = Empty_set U.
proof: Proof. auto with sets. Qed.
imports: Ensembles Constructive_sets Relations_1 Relations_1_facts Partial_Order Cpo Powerset