let n be Element of NAT ; :: thesis: for B1, X, B2 being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B1 holds
X (*) B1,B2 c= X
let B1, X, B2 be Subset of (TOP-REAL n); :: thesis: ( 0. (TOP-REAL n) in B1 implies X (*) B1,B2 c= X )
assume A1: 0. (TOP-REAL n) in B1 ; :: thesis: X (*) B1,B2 c= X
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
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
A2: ( x = y & 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 A2, EUCLID:31;
hence x in X by A2; :: thesis: verum