let n be Element of NAT ; :: thesis: for X being Subset of (TOP-REAL n) holds X (O) X = X
let X be Subset of (TOP-REAL n); :: thesis: X (O) X = X
thus X (O) X c= X by Th41; :: according to XBOOLE_0:def 10 :: thesis: X c= X (O) X
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in X (O) X )
assume A1: x in X ; :: thesis: x in X (O) X
then reconsider x1 = x as Point of (TOP-REAL n) ;
X + (0. (TOP-REAL n)) c= X by Th21;
then 0. (TOP-REAL n) in X (-) X ;
then x1 + (0. (TOP-REAL n)) in (X (-) X) (+) X by A1;
hence x in X (O) X by EUCLID:31; :: thesis: verum