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