Theorem ltrelre

Description: 'Less than' is a relation on real numbers. (Contributed by NM, 22-Feb-1996) (New usage is discouraged.)

	Ref	Expression
Assertion	ltrelre	|-

Proof

Step	Hyp	Ref	Expression
1		df-lt	|- . | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z
2		opabssxp	|- { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z
3	1 2	eqsstri	|-