let n be Element of NAT ; :: thesis: for B2, X, B1 being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B2 holds
(X (*) B1,B2) /\ X = {}
let B2, X, B1 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 = {}

now

given x being set such that A2: x in (X (*) B1,B2) /\ X ; :: thesis: contradiction
A3: x in X by A2, XBOOLE_0:def 4;
x in X (*) B1,B2 by A2, XBOOLE_0:def 4;
then x in (X ` ) (-) B2 by XBOOLE_0:def 4;
then consider y being Point of (TOP-REAL n) such that
A4: x = y and
A5: 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 A4, EUCLID:31;
hence contradiction by A3, A5, XBOOLE_0:def 5; :: thesis: verum

end;

hence (X (*) B1,B2) /\ X = {} by XBOOLE_0:def 1; :: thesis: verum