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