Theorem gtso

Description: 'Greater than' is a strict ordering. (Contributed by JJ, 11-Oct-2018)

	Ref	Expression
Assertion	gtso	⊢ ◡ < Or ℝ

Proof

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