Theorem sopo

Description: A strict linear order is a strict partial order. (Contributed by NM, 28-Mar-1997)

	Ref	Expression
Assertion	sopo	$$⊢R\mathrm{Or}A\to R\mathrm{Po}A$$

Proof

Step	Hyp	Ref	Expression
1		df-so	$$⊢R\mathrm{Or}A\leftrightarrow \left(R\mathrm{Po}A\wedge \forall x\in A\forall y\in A\left(xRy\vee x=y\vee yRx\right)\right)$$
2	1	simplbi	$$⊢R\mathrm{Or}A\to R\mathrm{Po}A$$