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