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 M3( the carrier of (CLatt L)) st b₁ is_a_complement_of b
take a = b ` ; :: thesis: a is_a_complement_of b
reconsider a9 = a, b9 = 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: a9 ` = a ` by Def11
.= b9 by Th3 ;
thus a "/\" b = a9 *' b9 by Def11
.= Bot L by A1, Th8
.= Bottom (CLatt L) by Th35 ; :: 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 a9 = a, b9 = b, c9 = c as Element of L by Def11;
A2: ( a "/\" b = a9 *' b9 & a "/\" c = a9 *' c9 ) by Def11;
b9 + c9 = b "\/" c by Def11;
hence a "/\" (b "\/" c) = a9 *' (b9 + c9) by Def11
.= (a9 *' b9) + (a9 *' c9) by Th30
.= (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