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