theorem Th21: :: UPROOTS:24

for L being non empty right_complementable distributive add-associative right_zeroed doubleLoopStr
for p being Polynomial of L
for pc being Element of (Polynom-Ring L) st p = pc holds
- p = - pc