set B = BooleLatt X;
A1: BooleLatt X is 0_Lattice by Th3;
BooleLatt X is 1_Lattice by Th4;
then reconsider B = BooleLatt X as 01_Lattice by A1;
A2: B is complemented
proof
let x be Element of B; :: according to LATTICES:def 19 :: thesis: ex b1 being Element of the carrier of B st b1 is_a_complement_of x
A3: H1(B) = bool X by Def1;
reconsider y = X \ x as Element of B by Def1;
take y ; :: thesis: y is_a_complement_of x
thus y "\/" x = y \/ x by Th1
.= X \/ x by XBOOLE_1:39
.= X by A3, XBOOLE_1:12
.= Top B by Th4 ; :: according to LATTICES:def 18 :: thesis: ( x "\/" y = Top B & y "/\" x = Bottom B & x "/\" y = Bottom B )
hence x "\/" y = Top B ; :: thesis: ( y "/\" x = Bottom B & x "/\" y = Bottom B )
A4: y misses x by XBOOLE_1:79;
thus y "/\" x = y /\ x by Th1
.= {} by A4
.= Bottom B by Th3 ; :: thesis: x "/\" y = Bottom B
hence x "/\" y = Bottom B ; :: thesis: verum
end;
B is distributive
proof
let x, y, z be Element of B; :: according to LATTICES:def 11 :: thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z)
thus x "/\" (y "\/" z) = x /\ (y "\/" z) by Th1
.= x /\ (y \/ z) by Th1
.= (x /\ y) \/ (x /\ z) by XBOOLE_1:23
.= (x "/\" y) \/ (x /\ z) by Th1
.= (x "/\" y) \/ (x "/\" z) by Th1
.= (x "/\" y) "\/" (x "/\" z) by Th1 ; :: thesis: verum
end;
hence BooleLatt X is Boolean by A2; :: thesis: verum