enrich
oelem
with
functions min : elem × elem → elem;
max : elem × elem → elem;
axioms min-def : ⊦ min(a, b) = (a < b ⊃ a;b);
max-def : ⊦ max(a, b) = (b < a ⊃ a;b);
end enrich