Journal of Formalized Mathematics
EMM, 2002
University of Bialystok
Copyright (c) 2002 Association of Mizar Users

### Boolean Properties of Sets --- Definitions

by
Library Committee

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;

```