Description: "Less than or equal to" is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | lerelxr | |- <_ C_ ( RR* X. RR* ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-le | |- <_ = ( ( RR* X. RR* ) \ `' < ) |
|
2 | difss | |- ( ( RR* X. RR* ) \ `' < ) C_ ( RR* X. RR* ) |
|
3 | 1 2 | eqsstri | |- <_ C_ ( RR* X. RR* ) |