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