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 ( ∅ , ℝ* , < ) < inf ( ∅ , ℝ* , < )

Proof

Step	Hyp	Ref	Expression
1		mnfltpnf	⊢ -∞ < +∞
2		xrsup0	⊢ sup ( ∅ , ℝ* , < ) = -∞
3		xrinf0	⊢ inf ( ∅ , ℝ* , < ) = +∞
4	1 2 3	3brtr4i	⊢ sup ( ∅ , ℝ* , < ) < inf ( ∅ , ℝ* , < )