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 a9 = a, b9 = b, c9 = c as Element of L by Def11;
A1: b9 *' c9 = b "/\" c by Def11;
a9 *' b9 = a "/\" b by Def11;
hence (a "/\" b) "/\" c = (a9 *' b9) *' c9 by Def11
.= a9 *' (b9 *' c9) by Th16
.= 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 a9 = a, b9 = b as Element of L by Def11;
a9 + b9 = a "\/" b by Def11;
hence a "/\" (a "\/" b) = a9 *' (a9 + b9) by Def11
.= a by Th21 ;
:: thesis: verum
end;
let a, b be Element of (CLatt L); :: according to LATTICES:def 8 :: thesis: (a "/\" b) + b = b
reconsider a9 = a, b9 = b as Element of L by Def11;
a9 *' b9 = a "/\" b by Def11;
hence (a "/\" b) "\/" b = (a9 *' b9) + b9 by Def11
.= b by Th20 ;
:: thesis: verum