theorem Th27: :: MATHMORP:27

for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for B, C being Subset of T
for y being Point of T holds (B \/ C) + y = (B + y) \/ (C + y)