let L be non empty LattStr ; :: thesis: ( L is trivial implies ( L is join-absorbing & L is meet-absorbing & L is Boolean ) )
assume A1: L is trivial ; :: 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 A1, 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 A1, STRUCT_0:def 10; :: thesis: verum

end;

A2: L is bounded

proof

A3: L is lower-bounded

proof

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

end;

L is upper-bounded

proof

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

end;

hence L is bounded by A3; :: thesis: verum

end;

A4: L is complemented

proof

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
consider a being Element of L;
take a ; :: thesis: a is_a_complement_of b
( a "\/" b = Top L & b "\/" a = Top L & a "/\" b = Bottom L & b "/\" a = Bottom L ) by A1, STRUCT_0:def 10;
hence a is_a_complement_of b by 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 A1, STRUCT_0:def 10; :: thesis: verum

end;

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