enrich
tord
with
functions
min : tord × tord → tord;
max : tord × tord → tord;
variables
a : tord;
b : tord;
axioms
min-def: min(a, b) = (a < b ⊃ a;b);
used for: ls;
max-def: max(a, b) = (b < a ⊃ a;b);
used for: ls;
end enrich