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