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 o. R ) C_ R <-> A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) )

Proof

Step	Hyp	Ref	Expression
1		cotrg	|- ( ( R o. R ) C_ R <-> A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) )