let x, y be Element of TrivOrtLat ; :: according to ROBBINS1:def 23 :: thesis: x "/\" y = ((x ` ) "\/" (y ` )) `
thus x "/\" y = ((x ` ) "\/" (y ` )) ` by STRUCT_0:def 10; :: thesis: verum