The abstract of the Mizar article:

Boolean Properties of Sets --- Definitions

by

Library Committee

Received April 6, 2002

MML identifier: XBOOLE_0

[ Mizar article, MML identifier index ]

environ

 vocabulary TARSKI, BOOLE, ZFMISC_1;
 notation TARSKI;
 constructors TARSKI;


begin

 reserve X, Y, Z, x, y, z for set;

scheme Separation { A()-> set, P[set] } :
   ex X being set st for x being set holds x in X iff x in A() & P[x];

definition
  func {} -> set means
:: XBOOLE_0:def 1
   not ex x being set st x in it;

 let X,Y be set;
  func X \/ Y -> set means
:: XBOOLE_0:def 2
   x in it iff x in X or x in Y;
  commutativity;
  idempotence;

  func X /\ Y -> set means
:: XBOOLE_0:def 3
   x in it iff x in X & x in Y;
  commutativity;
  idempotence;

  func X \ Y -> set means
:: XBOOLE_0:def 4
   x in it iff x in X & not x in Y;
end;

definition let X be set;
 attr X is empty means
:: XBOOLE_0:def 5
    X = {};

 let Y be set;
 func X \+\ Y -> set equals
:: XBOOLE_0:def 6
  (X \ Y) \/ (Y \ X);
 commutativity;

 pred X misses Y means
:: XBOOLE_0:def 7
   X /\ Y = {};
  symmetry;
  antonym X meets Y;

 pred X c< Y means
:: XBOOLE_0:def 8
    X c= Y & X <> Y;
 irreflexivity;

 pred X,Y are_c=-comparable means
:: XBOOLE_0:def 9
    X c= Y or Y c= X;
 reflexivity;
 symmetry;
 redefine pred X = Y means
:: XBOOLE_0:def 10
    X c= Y & Y c= X;
end;

theorem :: XBOOLE_0:1
    x in X \+\ Y iff not (x in X iff x in Y);

theorem :: XBOOLE_0:2 :: BOOLE'25:
    (for x holds not x in X iff (x in Y iff x in Z)) implies X = Y \+\ Z;



definition
 cluster {} -> empty;
 cluster empty set;
 cluster non empty set;
end;

definition let D be non empty set, X be set;
  cluster D \/ X -> non empty;
  cluster X \/ D -> non empty;
end;

theorem :: XBOOLE_0:3  :: BOOLE'1:
  X meets Y iff ex x st x in X & x in Y;

theorem :: XBOOLE_0:4 :: BOOLE'2:
    X meets Y iff ex x st x in X /\ Y;

theorem :: XBOOLE_0:5 :: SYSREL'1:
    X misses Y & x in X \/ Y implies
    ((x in X & not x in Y) or (x in Y & not x in X));

scheme Extensionality { X,Y() -> set, P[set] } :
  X() = Y() provided
  for x holds x in X() iff P[x] and
  for x holds x in Y() iff P[x];

scheme SetEq { P[set] } :
  for X1,X2 being set st
   (for x being set holds x in X1 iff P[x]) &
   (for x being set holds x in X2 iff P[x]) holds X1 = X2;