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

proof

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

end;

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