Theorem so2nr

Description: A strict order relation has no 2-cycle loops. (Contributed by NM, 21-Jan-1996)

	Ref	Expression
Assertion	so2nr	$$⊢\left(R\mathrm{Or}A\wedge \left(B\in A\wedge C\in A\right)\right)\to \neg \left(BRC\wedge CRB\right)$$

Proof

Step	Hyp	Ref	Expression
1		sopo	$$⊢R\mathrm{Or}A\to R\mathrm{Po}A$$
2		po2nr	$$⊢\left(R\mathrm{Po}A\wedge \left(B\in A\wedge C\in A\right)\right)\to \neg \left(BRC\wedge CRB\right)$$
3	1 2	sylan	$$⊢\left(R\mathrm{Or}A\wedge \left(B\in A\wedge C\in A\right)\right)\to \neg \left(BRC\wedge CRB\right)$$