Theorem son2lpi

Description: A strict order relation has no 2-cycle loops. (Contributed by NM, 10-Feb-1996) (Revised by Mario Carneiro, 10-May-2013)

	Ref	Expression
Hypotheses	soi.1	|- R Or S
	soi.2	|- R C_ ( S X. S )
Assertion	son2lpi	|- -. ( A R B /\ B R A )

Proof

Step	Hyp	Ref	Expression
1		soi.1	|- R Or S
2		soi.2	|- R C_ ( S X. S )
3	1 2	soirri	|- -. A R A
4	1 2	sotri	|- ( ( A R B /\ B R A ) -> A R A )
5	3 4	mto	|- -. ( A R B /\ B R A )