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