theorem Th16: :: GROEB_2:16

for X being set
for L being non empty right_complementable add-associative right_zeroed doubleLoopStr
for a being Element of L holds - (a | (X,L)) = (- a) | (X,L)