theorem Th9: :: RUSUB_5:9

for V being non empty right_complementable Abelian add-associative right_zeroed addLoopStr
for M, N being Subset of V
for v being Element of V holds
( M = N + {v} iff M - {v} = N )