let n be Element of NAT ; :: thesis: for C, B, X being Subset of (TOP-REAL n) st C c= B holds
X (O) B c= (X (-) C) (+) B
let C, B, X be Subset of (TOP-REAL n); :: thesis: ( C c= B implies X (O) B c= (X (-) C) (+) B )
assume A1: C c= B ; :: thesis: X (O) B c= (X (-) C) (+) B
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X (O) B or x in (X (-) C) (+) B )
assume x in X (O) B ; :: thesis: x in (X (-) C) (+) B
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;
C + x2 c= B + x2 by A1, Th3;
then C + x2 c= X by A3, XBOOLE_1:1;
then x1 in X (-) C by A3;
hence x in (X (-) C) (+) B by A2; :: thesis: verum