theorem Th15: :: MATHMORP:15

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, Y being Subset of T
for p being Point of T holds (X + p) (+) Y = (X (+) Y) + p