let x, y, z, u be Element of TrivOrtLat ; :: according to ROBBINS2:def 1 :: thesis: (((((x + y) ` ) + z) ` ) + ((x + (((z ` ) + ((z + u) ` )) ` )) ` )) ` = z
thus (((((x + y) ` ) + z) ` ) + ((x + (((z ` ) + ((z + u) ` )) ` )) ` )) ` = z by STRUCT_0:def 10; :: thesis: verum