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