let b be Element of (CLatt L); :: according to LATTICES:def 19 :: thesis:
take a = b ` ; :: thesis:
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:
thus b + a = Top (CLatt L) by Def8; :: thesis:
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:
hence b "/\" a = Bottom (CLatt L) ; :: thesis:

end;

let a, b, c be Element of (CLatt L); :: thesis:
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:

end;