set L = TrivOrtLat ;
thus for x, y being Element of TrivOrtLat holds x + y = y + x by STRUCT_0:def 10; :: according to LATTICES:def 4 :: thesis: ( TrivOrtLat is join-associative & TrivOrtLat is Huntington & TrivOrtLat is Robbins )
thus for x, y, z being Element of TrivOrtLat holds (x + y) + z = x + (y + z) by STRUCT_0:def 10; :: according to LATTICES:def 5 :: thesis: ( TrivOrtLat is Huntington & TrivOrtLat is Robbins )
thus for x, y being Element of TrivOrtLat holds (((x `) + (y `)) `) + (((x `) + y) `) = x by STRUCT_0:def 10; :: according to ROBBINS1:def 6 :: thesis: TrivOrtLat is Robbins
let x, y be Element of TrivOrtLat; :: according to ROBBINS1:def 5 :: thesis: (((x + y) `) + ((x + (y `)) `)) ` = x
thus (((x + y) `) + ((x + (y `)) `)) ` = x by STRUCT_0:def 10; :: thesis: verum