hereby :: according to LATTICES:def 7 :: thesis: ( CLatt L is join-absorbing & CLatt L is meet-absorbing )

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

end;

hereby :: according to LATTICES:def 9 :: thesis: CLatt L is meet-absorbing

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

end;

let a, b be Element of (CLatt L); :: according to LATTICES:def 8 :: thesis: (a "/\" b) + b = b
reconsider a' = a, b' = b as Element of L by Def11;
a' *' b' = a "/\" b by Def11;
hence (a "/\" b) "\/" b = (a' *' b') + b' by Def11
.= b by Th21 ;
:: thesis: verum