let T be non empty right_complementable Abelian add-associative right_zeroed RLSStruct ; :: thesis: for X, Y, B being Subset of T st X c= Y holds
( X (-) B c= Y (-) B & X (+) B c= Y (+) B )
let X, Y, B be Subset of T; :: thesis: ( X c= Y implies ( X (-) B c= Y (-) B & X (+) B c= Y (+) B ) )
assume A1: X c= Y ; :: thesis: ( X (-) B c= Y (-) B & X (+) B c= Y (+) B )
thus X (-) B c= Y (-) B :: thesis: X (+) B c= Y (+) B

proof

let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in X (-) B or p in Y (-) B )
assume p in X (-) B ; :: thesis: p in Y (-) B
then consider p1 being Point of T such that
A2: p = p1 and
A3: B + p1 c= X ;
B + p1 c= Y by A1, A3;
hence p in Y (-) B by A2; :: thesis: verum

end;

let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in X (+) B or p in Y (+) B )
assume p in X (+) B ; :: thesis: p in Y (+) B
then ex p1, p2 being Point of T st
( p = p1 + p2 & p1 in X & p2 in B ) ;
hence p in Y (+) B by A1; :: thesis: verum