theorem Th13: :: GROEB_3:13

for X being set
for L being non empty right_complementable add-associative right_zeroed addLoopStr holds - (0_ (X,L)) = 0_ (X,L)