enrich
oelem
with
functions
min : elem × elem → elem;
max : elem × elem → elem;
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