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