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