theorem Th45: :: UPROOTS:48

for L being non empty right_complementable left-distributive well-unital add-associative right_zeroed doubleLoopStr
for x being Element of L holds Roots <%(- x),(1. L)%> = {x}