Metamath Proof Explorer


Theorem lerelxr

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

Proof

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