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