Metamath Proof Explorer

Theorem gtso

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

Ref Expression
Assertion gtso 
|- `' < Or RR

Proof

Step Hyp Ref Expression
1 ltso 
 |-  < Or RR
2 cnvso 
 |-  ( < Or RR <-> `' < Or RR )
3 1 2 mpbi 
 |-  `' < Or RR