theorem :: MATHMORP:44
for T being non empty right_complementable Abelian add-associative right_zeroed RLSStruct
for X, B being Subset of T holds
( X (-) B c= (X (o) B) (-) B & X (+) B c= (X (o) B) (+) B )