let x, y be Element of (CLatt L); :: according to ROBBINS1:def 23 :: thesis: x "/\" y = ((x `) "\/" (y `)) `
reconsider x9 = x, y9 = y as Element of L by Def11;
( x9 ` = x ` & y9 ` = y ` ) by Def11;
then (x9 `) "\/" (y9 `) = (x `) "\/" (y `) by Def11;
then ((x `) "\/" (y `)) ` = x9 *' y9 by Def11;
hence x "/\" y = ((x `) "\/" (y `)) ` by Def11; :: thesis: verum