Theorem sotrieq2

Description: Trichotomy law for strict order relation. (Contributed by NM, 5-May-1999)

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

Proof

Step	Hyp	Ref	Expression
1		sotrieq	$$⊢\left(R\mathrm{Or}A\wedge \left(B\in A\wedge C\in A\right)\right)\to \left(B=C\leftrightarrow \neg \left(BRC\vee CRB\right)\right)$$
2		ioran	$$⊢\neg \left(BRC\vee CRB\right)\leftrightarrow \left(\neg BRC\wedge \neg CRB\right)$$
3	1 2	bitrdi	$$⊢\left(R\mathrm{Or}A\wedge \left(B\in A\wedge C\in A\right)\right)\to \left(B=C\leftrightarrow \left(\neg BRC\wedge \neg CRB\right)\right)$$