Metamath Proof Explorer


Theorem lerel

Description: "Less than or equal to" is a relation. (Contributed by FL, 2-Aug-2009) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion lerel
|- Rel <_

Proof

Step Hyp Ref Expression
1 lerelxr
 |-  <_ C_ ( RR* X. RR* )
2 relxp
 |-  Rel ( RR* X. RR* )
3 relss
 |-  ( <_ C_ ( RR* X. RR* ) -> ( Rel ( RR* X. RR* ) -> Rel <_ ) )
4 1 2 3 mp2
 |-  Rel <_