:: Built-in Concepts
:: by Andrzej Trybulec
::
:: Received January 1, 1989
:: Copyright (c) 1990-2011 Association of Mizar Users

begin

definition

mode set -> set ;

end;

definition

let x, y be set ;
pred x = 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 ;
pred x in X;
asymmetry
errorfrm ;

end;