HIDDEN

:: Built-in Concepts
::  by Andrzej Trybulec
::
:: Received January 1, 1989
:: Copyright (c) 1990-2026 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;