proposition: Theorem Empty_set_is_Bottom : forall A:Ensemble U, Bottom (Ensemble U) (Power_set_PO A) (Empty_set U).
proof: Proof. intro A; apply Bottom_definition; simpl; auto with sets. Qed.
imports: Ensembles Relations_1 Relations_1_facts Partial_Order Cpo