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