specification
using rename
weakord
by morphism
:Weakord → Tord;
< → <;
end rename
variables
a : Tord;
b : Tord;
c : Tord;
axioms
totality: a < b ∨ a = b ∨ b < a;
end specification