Metamath Proof Explorer

Theorem isogrp

Description: A (left-)ordered group is a group with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 23-Mar-2018)

Ref Expression
Assertion isogrp G oGrp G Grp G oMnd


Step Hyp Ref Expression
1 df-ogrp oGrp = Grp oMnd
2 1 elin2 G oGrp G Grp G oMnd