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 | |- |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ltp | |- |
|
2 | opabssxp | |- { <. x , y >. | ( ( x e. P. /\ y e. P. ) /\ x C. y ) } C_ ( P. X. P. ) |
|
3 | 1 2 | eqsstri | |- |