theorem :: MATHMORP:51

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