let n be Element of NAT ; :: thesis: for B, B1, X being Subset of (TOP-REAL n) st B = B (O) B1 holds
X (O) B c= X (O) B1
let B, B1, X be Subset of (TOP-REAL n); :: thesis: ( B = B (O) B1 implies X (O) B c= X (O) B1 )
assume A1: B = B (O) B1 ; :: thesis: X (O) B c= X (O) B1
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X (O) B or x in X (O) B1 )
assume x in X (O) B ; :: thesis: x in X (O) B1
then consider x1, b1 being Point of (TOP-REAL n) such that
A2: ( x = x1 + b1 & x1 in X (-) B & b1 in B ) ;
consider x2 being Point of (TOP-REAL n) such that
A3: ( x1 = x2 & B + x2 c= X ) by A2;
consider x3, b2 being Point of (TOP-REAL n) such that
A4: ( b1 = x3 + b2 & x3 in B (-) B1 & b2 in B1 ) by A1, A2;
consider x4 being Point of (TOP-REAL n) such that
A5: ( x3 = x4 & B1 + x4 c= B ) by A4;
(B1 + x4) + x2 c= B + x2 by A5, Th3;
then (B1 + x3) + x1 c= X by A3, A5, XBOOLE_1:1;
then B1 + (x3 + x1) c= X by Th16;
then x1 + x3 in X (-) B1 ;
then (x1 + x3) + b2 in (X (-) B1) (+) B1 by A4;
hence x in X (O) B1 by A2, A4, EUCLID:30; :: thesis: verum