Metamath Proof Explorer


Theorem ltrelpr

Description: Positive real 'less than' is a relation on positive reals. (Contributed by NM, 14-Feb-1996) (New usage is discouraged.)

Ref Expression
Assertion ltrelpr
|- 


Proof

Step Hyp Ref Expression
1 df-ltp
 |-  

. | ( ( x e. P. /\ y e. P. ) /\ x C. y ) }

2 opabssxp
 |-  { <. x , y >. | ( ( x e. P. /\ y e. P. ) /\ x C. y ) } C_ ( P. X. P. )
3 1 2 eqsstri
 |-