proposition: Theorem Strict_Rel_is_Strict_Included : same_relation (Ensemble U) (Strict_Included U) (Strict_Rel_of (Ensemble U) (Power_set_PO (Full_set U))).
proof: Proof. auto with sets. Qed.
imports: Ensembles Relations_1 Relations_1_facts Partial_Order Cpo