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	$$⊢\le \subseteq {ℝ}^{*}\times {ℝ}^{*}$$

Proof

Step	Hyp	Ref	Expression
1		df-le	$$⊢\le =\left({ℝ}^{*}\times {ℝ}^{*}\right)\setminus {<}^{-1}$$
2		difss	$$⊢\left({ℝ}^{*}\times {ℝ}^{*}\right)\setminus {<}^{-1}\subseteq {ℝ}^{*}\times {ℝ}^{*}$$
3	1 2	eqsstri	$$⊢\le \subseteq {ℝ}^{*}\times {ℝ}^{*}$$