let n be Element of NAT ; :: thesis: for X, B1, B2 being Subset of (TOP-REAL n) st B2 = {} holds
X (*) (B1,B2) = X (-) B1
let X, B1, B2 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) /\ the carrier of (TOP-REAL n) by Th8;
hence X (*) (B1,B2) = X (-) B1 by XBOOLE_1:28; :: thesis: verum