thus CLatt L is complemented :: thesis: ( CLatt L is distributive & CLatt L is bounded )

proof

let b be Element of (CLatt L); :: according to LATTICES:def 19 :: thesis: ex b₁ being M2(the carrier of (CLatt L)) st b₁ is_a_complement_of b
take a = b ` ; :: thesis: a is_a_complement_of b
reconsider a' = a, b' = b as Element of L by Def11;
thus a + b = Top (CLatt L) by Def8; :: according to LATTICES:def 18 :: thesis: ( b + a = Top (CLatt L) & a "/\" b = Bottom (CLatt L) & b "/\" a = Bottom (CLatt L) )
thus b + a = Top (CLatt L) by Def8; :: thesis: ( a "/\" b = Bottom (CLatt L) & b "/\" a = Bottom (CLatt L) )
A1: a' ` = a ` by Def11
.= b' by Th3 ;
thus a "/\" b = a' *' b' by Def11
.= Bot L by A1, Th9
.= Bottom (CLatt L) by Th36 ; :: thesis: b "/\" a = Bottom (CLatt L)
hence b "/\" a = Bottom (CLatt L) ; :: thesis: verum

end;

hereby :: according to LATTICES:def 11 :: thesis: CLatt L is bounded

let a, b, c be Element of (CLatt L); :: thesis: a "/\" (b "\/" c) = (a "/\" b) "\/" (a "/\" c)
reconsider a' = a, b' = b, c' = c as Element of L by Def11;
A2: ( b' + c' = b "\/" c & a "/\" b = a' *' b' & a "/\" c = a' *' c' ) by Def11;
hence a "/\" (b "\/" c) = a' *' (b' + c') by Def11
.= (a' *' b') + (a' *' c') by Th31
.= (a "/\" b) "\/" (a "/\" c) by A2, Def11 ;
:: thesis: verum

end;

thus CLatt L is lower-bounded ; :: according to LATTICES:def 15 :: thesis: CLatt L is upper-bounded
thus CLatt L is upper-bounded ; :: thesis: verum