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