let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for X, B being Subset of T holds
( X (-) B c= (X (o) B) (-) B & X (+) B c= (X (o) B) (+) B )
let X, B be Subset of T; :: thesis: ( X (-) B c= (X (o) B) (-) B & X (+) B c= (X (o) B) (+) B )
X c= X (o) B by Th41;
hence ( X (-) B c= (X (o) B) (-) B & X (+) B c= (X (o) B) (+) B ) by Th9; :: thesis: verum