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