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