Theorem supxrltinfxr

Description: The supremum of the empty set is strictly smaller than the infimum of the empty set. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Assertion	supxrltinfxr	$$⊢sup\left(\varnothing ,{ℝ}^{*},<\right)<inf\left(\varnothing ,{ℝ}^{*},<\right)$$

Proof

Step	Hyp	Ref	Expression
1		mnfltpnf	$$⊢\mathrm{-\infty }<\mathrm{+\infty }$$
2		xrsup0	$$⊢sup\left(\varnothing ,{ℝ}^{*},<\right)=\mathrm{-\infty }$$
3		xrinf0	$$⊢inf\left(\varnothing ,{ℝ}^{*},<\right)=\mathrm{+\infty }$$
4	1 2 3	3brtr4i	$$⊢sup\left(\varnothing ,{ℝ}^{*},<\right)<inf\left(\varnothing ,{ℝ}^{*},<\right)$$