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

A2: L is lower-bounded

hence L is Boolean by A2, A1, A3; :: thesis: verum

thus L is join-absorbing by STRUCT_0:def 10; :: thesis: ( L is meet-absorbing & L is Boolean )

A1: L is upper-bounded

proof

thus
L is meet-absorbing
by STRUCT_0:def 10; :: thesis: L is Boolean
set c = the Element of L;

take the Element of L ; :: according to LATTICES:def 14 :: thesis: for b_{1} being M3( the carrier of L) holds

( the Element of L "\/" b_{1} = the Element of L & b_{1} "\/" 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;take the Element of L ; :: according to LATTICES:def 14 :: thesis: for b

( the Element of L "\/" b

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

A2: L is lower-bounded

proof

A3:
L is complemented
set c = the Element of L;

take the Element of L ; :: according to LATTICES:def 13 :: thesis: for b_{1} being M3( the carrier of L) holds

( the Element of L "/\" b_{1} = the Element of L & b_{1} "/\" 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;take the Element of L ; :: according to LATTICES:def 13 :: thesis: for b

( the Element of L "/\" b

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

proof

L is distributive
by STRUCT_0:def 10;
set a = the Element of L;

let b be Element of L; :: according to LATTICES:def 19 :: thesis: ex b_{1} being M3( the carrier of L) st b_{1} 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;let b be Element of L; :: according to LATTICES:def 19 :: thesis: ex 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

hence L is Boolean by A2, A1, A3; :: thesis: verum