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