proposition: Lemma Strict_inclusion_is_transitive_with_inclusion : forall x y z:Ensemble U, Strict_Included U x y -> Included U y z -> Strict_Included U x z.
proof: Proof. intros x y z H' H'0; try assumption. elim Strict_Rel_is_Strict_Included. unfold contains. intros H'1 H'2; try assumption. apply H'1. apply Strict_Rel_Transitive_with_Rel with (y := y); auto with sets. Qed.
imports: Ensembles Relations_1 Relations_1_facts Partial_Order Cpo