:: BOOLE semantic presentation

theorem :: BOOLE:1

for X being set holds X \/ {} = X

proof end;

theorem :: BOOLE:2

for X being set holds X /\ {} = {}

proof end;

theorem :: BOOLE:3

for X being set holds X \ {} = X

proof end;

theorem :: BOOLE:4

for X being set holds {} \ X = {}

proof end;

theorem :: BOOLE:5

for X being set holds X \+\ {} = X

proof end;

theorem :: BOOLE:6

for X being set st X is empty holds
X = {} by XBOOLE_0:def 5;

theorem :: BOOLE:7

for x, X being set st x in X holds
not X is empty

proof end;

theorem :: BOOLE:8

for X, Y being set st X is empty & X <> Y holds
not Y is empty

proof end;