theorem Th4: :: MATHMORP:4

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for x being Point of T
for X being Subset of T st X = {} holds
X + x = {}