let n be Element of NAT ; :: thesis: for X, B being Subset of (TOP-REAL n) holds (X (O) B) (O) B = X (O) B
let X, B be Subset of (TOP-REAL n); :: thesis: (X (O) B) (O) B = X (O) B
thus (X (O) B) (O) B c= X (O) B by Th41; :: according to XBOOLE_0:def 10 :: thesis: X (O) B c= (X (O) B) (O) B
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X (O) B or x in (X (O) B) (O) B )
assume x in X (O) B ; :: thesis: x in (X (O) B) (O) B
then consider x1, b1 being Point of (TOP-REAL n) such that
A1: ( x = x1 + b1 & x1 in X (-) B & b1 in B ) ;
consider x2 being Point of (TOP-REAL n) such that
A2: ( x1 = x2 & B + x2 c= X ) by A1;
(B + x2) (O) B c= X (O) B by A2, Th45;
then (B (O) B) + x2 c= X (O) B by Th46;
then B + x2 c= X (O) B by Th42;
then x1 in { x4 where x4 is Point of (TOP-REAL n) : B + x4 c= X (O) B } by A2;
hence x in (X (O) B) (O) B by A1; :: thesis: verum