hidden.miz
begin
definition
mode
object;
end
definition
mode
set ->
object ;
end
definition
let x,y be
object;
pred x
= y;
reflexivity ;
symmetry ;
end
notation
let x,y be
object;
antonym x
<> y for x
= y;
end
definition
let x be
object, X be
set;
pred x
in X;
end