theorem Th9: :: MATHMORP:9

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