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