theorem Th28: :: MATHMORP:28

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)