let n be Element of NAT ; :: thesis: for X, B being Subset of (TOP-REAL n) holds
( (X (O) B) (-) B c= X (-) B & (X (O) B) (+) B c= X (+) B )
let X, B be Subset of (TOP-REAL n); :: thesis: ( (X (O) B) (-) B c= X (-) B & (X (O) B) (+) B c= X (+) B )
X (O) B c= X by Th41;
hence ( (X (O) B) (-) B c= X (-) B & (X (O) B) (+) B c= X (+) B ) by Th9; :: thesis: verum