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

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A2: x in X (&) (B1,B2) ; :: thesis:

end;

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

end;