let n be Element of NAT ; :: thesis: for X, Y, B being Subset of (TOP-REAL n) st X c= Y holds
( X (-) B c= Y (-) B & X (+) B c= Y (+) B )
let X, Y, B be Subset of (TOP-REAL n); :: 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 set ; :: 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 (TOP-REAL n) such that
A2: ( p = p1 & B + p1 c= X ) ;
( p = p1 & B + p1 c= Y ) by A1, A2, XBOOLE_1:1;
hence p in Y (-) B ; :: thesis: verum

end;

let p be set ; :: 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, p2 being Point of (TOP-REAL n) such that
A3: ( p = p1 + p2 & p1 in X & p2 in B ) ;
thus p in Y (+) B by A1, A3; :: thesis: verum