let n be Element of NAT ; :: thesis: for B2, X, B1 being Subset of (TOP-REAL n) st B2 = {} holds
X (*) B1,B2 = X (-) B1
let B2, X, B1 be Subset of (TOP-REAL n); :: thesis: ( B2 = {} implies X (*) B1,B2 = X (-) B1 )
assume B2 = {} ; :: thesis: X (*) B1,B2 = X (-) B1
then X (*) B1,B2 = (X (-) B1) /\ (REAL n) by Th8;
then X (*) B1,B2 = (X (-) B1) /\ the carrier of (TOP-REAL n) by EUCLID:25;
hence X (*) B1,B2 = X (-) B1 by XBOOLE_1:28; :: thesis: verum