:: BOOLE semantic presentation

begin

theorem :: BOOLE:1
for X being set holds X \/ {} = X
proof
let X be set ; ::_thesis: X \/ {} = X
thus  X \/ {} c= X :: according to XBOOLE_0:def_10 ::_thesis: X c= X \/ {}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X \/ {} or x in X )
assume  x in X \/ {} ; ::_thesis: x in X
then  ( x in X or x in {} ) by XBOOLE_0:def_3;
hence  x in X by XBOOLE_0:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in X \/ {} )
assume  x in X ; ::_thesis: x in X \/ {}
hence  x in X \/ {} by XBOOLE_0:def_3; ::_thesis: verum
end;

theorem :: BOOLE:2
for X being set holds X /\ {} = {}
proof
let X be set ; ::_thesis: X /\ {} = {}
thus  X /\ {} c= {} :: according to XBOOLE_0:def_10 ::_thesis: {} c= X /\ {}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X /\ {} or x in {} )
assume  x in X /\ {} ; ::_thesis: x in {}
hence  x in {} by XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {} or x in X /\ {} )
assume  x in {} ; ::_thesis: x in X /\ {}
hence  x in X /\ {} by XBOOLE_0:def_1; ::_thesis: verum
end;

theorem :: BOOLE:3
for X being set holds X \ {} = X
proof
let X be set ; ::_thesis: X \ {} = X
thus  X \ {} c= X :: according to XBOOLE_0:def_10 ::_thesis: X c= X \ {}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X \ {} or x in X )
assume  x in X \ {} ; ::_thesis: x in X
hence  x in X by XBOOLE_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in X \ {} )
A1: not x in {} by XBOOLE_0:def_1;
assume  x in X ; ::_thesis: x in X \ {}
hence  x in X \ {} by A1, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem :: BOOLE:4
for X being set holds {} \ X = {}
proof
let X be set ; ::_thesis: {} \ X = {}
thus  {} \ X c= {} :: according to XBOOLE_0:def_10 ::_thesis: {} c= {} \ X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {} \ X or x in {} )
assume  x in {} \ X ; ::_thesis: x in {}
hence  x in {} by XBOOLE_0:def_5; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {} or x in {} \ X )
assume  x in {} ; ::_thesis: x in {} \ X
hence  x in {} \ X by XBOOLE_0:def_1; ::_thesis: verum
end;

theorem :: BOOLE:5
for X being set holds X \+\ {} = X
proof
let X be set ; ::_thesis: X \+\ {} = X
thus  X \+\ {} c= X :: according to XBOOLE_0:def_10 ::_thesis: X c= X \+\ {}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X \+\ {} or x in X )
assume  x in X \+\ {} ; ::_thesis: x in X
then A1: ( x in X \ {} or x in {} \ X ) by XBOOLE_0:def_3;
percases ( ( x in X & not x in {} ) or ( x in {} & not x in X ) ) by A1, XBOOLE_0:def_5;
suppose ( x in X & not x in {} ) ; ::_thesis: x in X
hence  x in X ; ::_thesis: verum
end;
suppose ( x in {} & not x in X ) ; ::_thesis: x in X
hence  x in X by XBOOLE_0:def_1; ::_thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in X \+\ {} )
A2: not x in {} by XBOOLE_0:def_1;
assume  x in X ; ::_thesis: x in X \+\ {}
then  x in X \ {} by A2, XBOOLE_0:def_5;
hence  x in X \+\ {} by XBOOLE_0:def_3; ::_thesis: verum
end;

  Lm1:  for X being set st X is empty holds
X = {}
proof
let X be set ; ::_thesis: ( X is empty implies X = {} )
assume  for x being set holds not x in X ; :: according to XBOOLE_0:def_1 ::_thesis: X = {}
then  for x being set holds
( x in {} iff x in X ) by XBOOLE_0:def_1;
hence  X = {} by TARSKI:1; ::_thesis: verum
end;

theorem :: BOOLE:6
for X being set st X is empty holds
X = {} by Lm1;

theorem :: BOOLE:7
for x, X being set st x in X holds
not X is empty by XBOOLE_0:def_1;

theorem :: BOOLE:8
for X, Y being set st X is empty & X <> Y holds
not Y is empty
proof
let X, Y be set ; ::_thesis: ( X is empty & X <> Y implies not Y is empty )
assume that
A1: X is empty and
A2: X <> Y ; ::_thesis: not Y is empty
 X = {} by A1, Lm1;
hence  not Y is empty by A2, Lm1; ::_thesis: verum
end;