theorem Th5: :: RLTOPSP1:5

for X being non empty right_complementable add-associative right_zeroed addLoopStr
for M being Subset of X holds (0. X) + M = M