This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cotr

Description: Two ways of saying a relation is transitive. Definition of transitivity in Schechter p. 51. Special instance of cotrg . (Contributed by NM, 27-Dec-1996)

Ref Expression
Assertion cotr ⊢ R ∘ R ⊆ R ↔ ∀ x ∀ y ∀ z x R y ∧ y R z → x R z

Proof

Step Hyp Ref Expression
1 cotrg ⊢ R ∘ R ⊆ R ↔ ∀ x ∀ y ∀ z x R y ∧ y R z → x R z