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;