:: BOOLE semantic presentation

theorem Th1: :: BOOLE:1

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

proof end;

theorem Th2: :: BOOLE:2

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

proof end;

theorem Th3: :: BOOLE:3

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

proof end;

theorem Th4: :: BOOLE:4

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

proof end;

theorem Th5: :: BOOLE:5

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

proof end;

theorem Th6: :: BOOLE:6

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

theorem Th7: :: BOOLE:7

for b₁, b₂ being set st b₁ in b₂ holds
not b₂ is empty

proof end;

theorem Th8: :: BOOLE:8

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

proof end;