:: Built-in Concepts
:: by Andrzej Trybulec
::
:: Received January 1, 1989
:: Copyright (c) 1990-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
begin
:: 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 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;