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