let n be Element of NAT ; :: thesis: for B2, X, B1 being Subset of (TOP-REAL n) st 0.REAL n in B2 holds
X (@) B1,B2 = X
let B2, X, B1 be Subset of (TOP-REAL n); :: thesis: ( 0.REAL n in B2 implies X (@) B1,B2 = X )
assume A1: 0.REAL n in B2 ; :: thesis: X (@) B1,B2 = X
thus X (@) B1,B2 c= X :: according to XBOOLE_0:def 10 :: thesis: X c= X (@) B1,B2

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X (@) B1,B2 or x in X )
assume x in X (@) B1,B2 ; :: thesis: x in X
hence x in X by XBOOLE_0:def 5; :: thesis: verum

end;

let x be set ; :: 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 (-) B1 & x in (X ` ) (-) B2 ) by XBOOLE_0:def 4;
then consider y being Point of (TOP-REAL n) such that
A3: ( x = y & B2 + y c= X ` ) ;
(0.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, EUCLID:31;
hence contradiction by A2, A3, XBOOLE_0:def 5; :: thesis: verum

end;

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