Theorem ltso

Description: 'Less than' is a strict ordering. (Contributed by NM, 19-Jan-1997)

	Ref	Expression
Assertion	ltso	$$⊢<\mathrm{Or}ℝ$$

Proof

Step	Hyp	Ref	Expression
1		axlttri	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to \left(x<y\leftrightarrow \neg \left(x=y\vee y<x\right)\right)$$
2		lttr	$$⊢\left(x\in ℝ\wedge y\in ℝ\wedge z\in ℝ\right)\to \left(\left(x<y\wedge y<z\right)\to x<z\right)$$
3	1 2	isso2i	$$⊢<\mathrm{Or}ℝ$$