let n be Element of NAT ; :: thesis: for X, B1, B2 being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B2 holds
X (@) (B1,B2) = X
let X, B1, B2 be Subset of (TOP-REAL n); :: thesis: ( 0. (TOP-REAL n) in B2 implies X (@) (B1,B2) = X )
assume A1: 0. (TOP-REAL n) in B2 ; :: thesis: X (@) (B1,B2) = X
thus X (@) (B1,B2) c= X by XBOOLE_0:def 5; :: according to XBOOLE_0:def 10 :: thesis: X c= X (@) (B1,B2)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in X (@) (B1,B2) )
assume A2: x in X ; :: thesis: x in X (@) (B1,B2)
not x in X (*) (B1,B2)

proof

assume x in X (*) (B1,B2) ; :: thesis: contradiction
then x in (X `) (-) B2 by XBOOLE_0:def 4;
then consider y being Point of (TOP-REAL n) such that
A3: x = y and
A4: B2 + y c= X ` ;
(0. (TOP-REAL n)) + y in { (z + y) where z is Point of (TOP-REAL n) : z in B2 } by A1;
then x in B2 + y by A3;
hence contradiction by A2, A4, XBOOLE_0:def 5; :: thesis: verum

end;

hence x in X (@) (B1,B2) by A2, XBOOLE_0:def 5; :: thesis: verum