proposition: Lemma Strict_Rel_Transitive : Transitive U (Strict_Rel_of U D).
proof: Proof. red. intros x y z H' H'0. apply Strict_Rel_Transitive_with_Rel with (y := y); [ intuition | unfold Strict_Rel_of in H', H'0; intuition ]. Qed.
imports: Ensembles Relations_1