proposition: Lemma Strict_Rel_Transitive_with_Rel : forall x y z:U, Strict_Rel_of U D x y -> @Rel_of U D y z -> Strict_Rel_of U D x z.
proof: Proof. unfold Strict_Rel_of at 1. red. elim D; simpl. intros C R H' H'0; elim H'0. intros H'1 H'2 H'3 x y z H'4 H'5; split. - apply H'2 with (y := y); tauto. - red; intro H'6. elim H'4; intros H'7 H'8; apply H'8; clear H'4. apply H'3; auto. rewrite H'6; tauto. Qed.
imports: Ensembles Relations_1