theorem :: BAGORDER:30

for o being Ordinal holds GrInvLexOrder o is well-ordering