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


:: This article documents a part of the Mizar axiomatics - it shows how
:: the primitives of set theory are introduced in the Mizar Mathematical
:: Library.
:: Please note that the notions defined here are not subject to standard
:: verification, so the Mizar verifier and other utilities may report
:: errors when processing this article.
definition
mode element -> element ;
end;

definition
mode set -> element ;
end;

definition
let x, y be element ;
pred x = y;
reflexivity
errorfrm ;
symmetry
errorfrm ;
end;

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

definition
let x be element ;
let X be set ;
pred x in X;
asymmetry
errorfrm ;
end;