consider x being Element of TrivComplLat;
take x ; :: according to ROBBINS1:def 13 :: thesis: x + x = x
thus x = x + x by STRUCT_0:def 10; :: thesis: verum