let L be 1 -element LattStr ; :: thesis: ( L is join-absorbing & L is meet-absorbing & L is Boolean )
thus L is join-absorbing by STRUCT_0:def 10; :: thesis: ( L is meet-absorbing & L is Boolean )
A1: L is upper-bounded

proof

set c = the Element of L;
take the Element of L ; :: according to LATTICES:def 14 :: thesis: for b₁ being M3( the carrier of L) holds
( the Element of L "\/" b₁ = the Element of L & b₁ "\/" the Element of L = the Element of L )
let a be Element of L; :: thesis: ( the Element of L "\/" a = the Element of L & a "\/" the Element of L = the Element of L )
thus ( the Element of L "\/" a = the Element of L & a "\/" the Element of L = the Element of L ) by STRUCT_0:def 10; :: thesis: verum

end;

thus L is meet-absorbing by STRUCT_0:def 10; :: thesis: L is Boolean
A2: L is lower-bounded

proof

set c = the Element of L;
take the Element of L ; :: according to LATTICES:def 13 :: thesis: for b₁ being M3( the carrier of L) holds
( the Element of L "/\" b₁ = the Element of L & b₁ "/\" the Element of L = the Element of L )
let a be Element of L; :: thesis: ( the Element of L "/\" a = the Element of L & a "/\" the Element of L = the Element of L )
thus ( the Element of L "/\" a = the Element of L & a "/\" the Element of L = the Element of L ) by STRUCT_0:def 10; :: thesis: verum

end;

A3: L is complemented

proof

set a = the Element of L;
let b be Element of L; :: according to LATTICES:def 19 :: thesis: ex b₁ being M3( the carrier of L) st b₁ is_a_complement_of b
take the Element of L ; :: thesis: the Element of L is_a_complement_of b
A4: ( the Element of L "/\" b = Bottom L & b "/\" the Element of L = Bottom L ) by STRUCT_0:def 10;
( the Element of L "\/" b = Top L & b "\/" the Element of L = Top L ) by STRUCT_0:def 10;
hence the Element of L is_a_complement_of b by A4; :: thesis: verum

end;

L is distributive by STRUCT_0:def 10;
hence L is Boolean by A2, A1, A3; :: thesis: verum