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	⊢ ≤ ⊆ ( ℝ* × ℝ* )
2		relxp	⊢ Rel ( ℝ* × ℝ* )
3		relss	⊢ ( ≤ ⊆ ( ℝ* × ℝ* ) → ( Rel ( ℝ* × ℝ* ) → Rel ≤ ) )
4	1 2 3	mp2	⊢ Rel ≤