theorem :: MATHMORP:70

for n being Element of NAT
for X, B1, B2 being Subset of (TOP-REAL n) st 0. (TOP-REAL n) in B2 holds
(X (*) (B1,B2)) /\ X = {}