theorem Th12: :: FVALUAT1:12

for K being non empty right_complementable distributive left_unital add-associative right_zeroed doubleLoopStr holds (- (1. K)) * (- (1. K)) = 1. K