theorem Th1: :: MOD_3:1
for R being non empty non degenerated right_complementable add-associative right_zeroed doubleLoopStr holds 0. R <> - (1. R)