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 b1 being M3( the carrier of L) holds
( the Element of L "\/" b1 = the Element of L & b1 "\/" 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 b1 being M3( the carrier of L) holds
( the Element of L "/\" b1 = the Element of L & b1 "/\" 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 b1 being M3( the carrier of L) st b1 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