Theorem xrgtso

Description: 'Greater than' is a strict ordering on the extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Assertion	xrgtso	⊢ ◡ < Or ℝ*

Proof

Step	Hyp	Ref	Expression
1		xrltso	⊢ < Or ℝ*
2		cnvso	⊢ ( < Or ℝ* ↔ ◡ < Or ℝ* )
3	1 2	mpbi	⊢ ◡ < Or ℝ*