B.4 XBOOLE_0

Boolean Properties of Sets --- Definitions

by Library Committee

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];

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

der 2 func X \/ Y -> set means x in it iff x in X or x in Y;

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

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

def 5 attr X is empty means X = {};

def 6 func X \+\ Y -> set equals (X \ Y) \/ (Y \ X);

def 7 pred X misses Y means X /\ Y = {};

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

def 9 pred X,Y are_c=-comparable means X c= Y or Y c= X;

def 10 redefine pred X = Y means X c= Y & Y c= X;

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

2 (for x holds not x in X iff (x in Y iff x in Z))

implies X = Y \+\ Z;

cluster {} -> empty;

cluster empty set;

cluster non empty set;

let D be non empty set, X be set;

cluster D \/ X -> non empty;

cluster X \/ D -> non empty;

3 X meets Y iff ex x st x in X & x in Y;

4 X meets Y iff ex x st x in X /\ Y;

5 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;