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

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 set;
end;

definition let x,y be set;
  pred x = y;
  reflexivity;
  symmetry;
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;
end;