proposition: Lemma Strict_inclusion_is_transitive : Transitive (Ensemble U) (Strict_Included U).
proof: Proof. apply cong_transitive_same_relation with (R := Strict_Rel_of (Ensemble U) (Power_set_PO (Full_set U))); auto with sets. Qed.
imports: Ensembles Relations_1 Relations_1_facts Partial_Order Cpo