let n be Element of NAT ; :: thesis: for X, Y, B being Subset of (TOP-REAL n) st X c= Y holds
( X (O) B c= Y (O) B & X (o) B c= Y (o) B )
let X, Y, B be Subset of (TOP-REAL n); :: thesis: ( X c= Y implies ( X (O) B c= Y (O) B & X (o) B c= Y (o) B ) )
assume A1: X c= Y ; :: thesis: ( X (O) B c= Y (O) B & X (o) B c= Y (o) B )
thus X (O) B c= Y (O) B :: thesis: X (o) B c= Y (o) B

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X (O) B or x in Y (O) B )
assume x in X (O) B ; :: thesis: x in Y (O) B
then consider x2, b2 being Point of (TOP-REAL n) such that
A2: ( x = x2 + b2 & x2 in X (-) B & b2 in B ) ;
consider y being Point of (TOP-REAL n) such that
A3: ( x2 = y & B + y c= X ) by A2;
B + y c= Y by A1, A3, XBOOLE_1:1;
then x2 in { y1 where y1 is Point of (TOP-REAL n) : B + y1 c= Y } by A3;
hence x in Y (O) B by A2; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X (o) B or x in Y (o) B )
assume x in X (o) B ; :: thesis: x in Y (o) B
then consider x2 being Point of (TOP-REAL n) such that
A4: ( x = x2 & B + x2 c= X (+) B ) ;
X (+) B c= Y (+) B by A1, Th9;
then B + x2 c= Y (+) B by A4, XBOOLE_1:1;
hence x in Y (o) B by A4; :: thesis: verum