let L be 1 -element LattStr ; :: thesis: ( L is join-absorbing & L is meet-absorbing & L is Boolean )
thus L is join-absorbing :: thesis: ( L is meet-absorbing & L is Boolean )

proof

let x, y be Element of L; :: according to LATTICES:def 9 :: thesis: x "/\" (x "\/" y) = x
thus x "/\" (x "\/" y) = x by STRUCT_0:def 10; :: thesis: verum

end;

A2: 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 M2( 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 :: thesis: L is Boolean

proof

let x, y be Element of L; :: according to LATTICES:def 8 :: thesis: (x "/\" y) "\/" y = y
thus (x "/\" y) "\/" y = y by STRUCT_0:def 10; :: thesis: verum

end;

A3: 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 M2( 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;

A4: 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 M2( 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
A5: ( 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 A5, LATTICES:def 18; :: thesis: verum

end;

L is distributive

proof

let a, b, c be Element of L; :: according to LATTICES:def 11 :: thesis: a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
thus a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c) by STRUCT_0:def 10; :: thesis: verum

end;

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