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 
 |-