Theorem ltso

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

	Ref	Expression
Assertion	ltso	|- < Or RR

Proof

Step	Hyp	Ref	Expression
1		axlttri	|- ( ( x e. RR /\ y e. RR ) -> ( x < y <-> -. ( x = y \/ y < x ) ) )
2		lttr	|- ( ( x e. RR /\ y e. RR /\ z e. RR ) -> ( ( x < y /\ y < z ) -> x < z ) )
3	1 2	isso2i	|- < Or RR