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