:: HIDDEN semantic presentation

begin

definition
mode set  ->  set ;
end;

definition
let x, y be set ;
predx = y;
reflexivity
 errorfrm ;
symmetry
 errorfrm ;
end;

notation
let x, y be set ;
antonym x <> y for x = y;
end;

definition
let x, X be set ;
predx in X;
asymmetry
 errorfrm ;
end;