theorem :: RUSUB_5:10

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 st v in N holds
M + {v} c= M + N