let n be Element of NAT ; :: thesis: for B, C, X being Subset of (TOP-REAL n) st B c= C holds
X (o) B c= (X (+) C) (-) B
let B, C, X be Subset of (TOP-REAL n); :: thesis: ( B c= C implies X (o) B c= (X (+) C) (-) B )
assume A1: B c= C ; :: 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 x2 being Point of (TOP-REAL n) such that
A2: ( x = x2 & B + x2 c= X (+) B ) ;
X (+) B c= X (+) C by A1, Th10;
then B + x2 c= X (+) C by A2, XBOOLE_1:1;
hence x in (X (+) C) (-) B by A2; :: thesis: verum