:: BOOLE semantic presentation

theorem :: BOOLE:1

for b₁ being set holds b₁ \/ {} = b₁

let c₁ be set ;
thus c₁ \/ {} c= c₁ :: uses XBOOLE_0:def 10

let c₂ be set ; :: uses TARSKI:def 3
assume c₂ in c₁ \/ {} ;
then ( c₂ in c₁ or c₂ in {} ) by XBOOLE_0:def 2;
hence c₂ in c₁ by XBOOLE_0:def 1;

end;

let c₂ be set ; :: uses TARSKI:def 3
assume c₂ in c₁ ;
hence c₂ in c₁ \/ {} by XBOOLE_0:def 2;

end;

theorem :: BOOLE:2

for b₁ being set holds b₁ /\ {} = {}

proof

let c₁ be set ;
thus c₁ /\ {} c= {} :: uses XBOOLE_0:def 10

proof

let c₂ be set ; :: uses TARSKI:def 3
assume c₂ in c₁ /\ {} ;
hence c₂ in {} by XBOOLE_0:def 3;

end;

let c₂ be set ; :: uses TARSKI:def 3
assume c₂ in {} ;
hence c₂ in c₁ /\ {} by XBOOLE_0:def 1;

end;

theorem :: BOOLE:3

for b₁ being set holds b₁ \ {} = b₁

proof

let c₁ be set ;
thus c₁ \ {} c= c₁ :: uses XBOOLE_0:def 10

proof

let c₂ be set ; :: uses TARSKI:def 3
assume c₂ in c₁ \ {} ;
hence c₂ in c₁ by XBOOLE_0:def 4;

end;

let c₂ be set ; :: uses TARSKI:def 3
assume c₂ in c₁ ;
then ( c₂ in c₁ & not c₂ in {} ) by XBOOLE_0:def 1;
hence c₂ in c₁ \ {} by XBOOLE_0:def 4;

end;

theorem :: BOOLE:4

for b₁ being set holds {} \ b₁ = {}

proof

let c₁ be set ;
thus {} \ c₁ c= {} :: uses XBOOLE_0:def 10

proof

let c₂ be set ; :: uses TARSKI:def 3
assume c₂ in {} \ c₁ ;
hence c₂ in {} by XBOOLE_0:def 4;

end;

let c₂ be set ; :: uses TARSKI:def 3
assume c₂ in {} ;
hence c₂ in {} \ c₁ by XBOOLE_0:def 1;

end;

theorem :: BOOLE:5

for b₁ being set holds b₁ \+\ {} = b₁

proof

let c₁ be set ;
thus c₁ \+\ {} c= c₁ :: uses XBOOLE_0:def 10

proof

let c₂ be set ; :: uses TARSKI:def 3
assume c₂ in c₁ \+\ {} ;
then c₂ in (c₁ \ {} ) \/ ({} \ c₁) ;
then E1: ( c₂ in c₁ \ {} or c₂ in {} \ c₁ ) by XBOOLE_0:def 2;

per cases ( ( c₂ in c₁ & not c₂ in {} ) or ( c₂ in {} & not c₂ in c₁ ) ) by E1, XBOOLE_0:def 4;

suppose ( c₂ in c₁ & not c₂ in {} ) ;

hence c₂ in c₁ ;

end;

suppose ( c₂ in {} & not c₂ in c₁ ) ;

hence c₂ in c₁ by XBOOLE_0:def 1;

end;

let c₂ be set ; :: uses TARSKI:def 3
assume c₂ in c₁ ;
then ( c₂ in c₁ & not c₂ in {} ) by XBOOLE_0:def 1;
then c₂ in c₁ \ {} by XBOOLE_0:def 4;
then c₂ in (c₁ \ {} ) \/ ({} \ c₁) by XBOOLE_0:def 2;
hence c₂ in c₁ \+\ {} ;

end;

theorem :: BOOLE:6

for b₁ being set holds
( b₁ is empty implies b₁ = {} ) by XBOOLE_0:def 5;

theorem :: BOOLE:7

for b₁, b₂ being set holds
not ( b₁ in b₂ & b₂ is empty )

proof

let c₁, c₂ be set ;
assume c₁ in c₂ ;
then c₂ <> {} by XBOOLE_0:def 1;
hence not c₂ is empty by XBOOLE_0:def 5;

end;

theorem :: BOOLE:8

for b₁, b₂ being set holds
not ( b₁ is empty & b₁ <> b₂ & b₂ is empty )

proof

let c₁, c₂ be set ;
assume that E1: c₁ is empty
and E2: c₁ <> c₂ ;
c₁ = {} by E1, XBOOLE_0:def 5;
hence not c₂ is empty by E2, XBOOLE_0:def 5;

end;