let n be Element of NAT ; :: thesis: for X being Subset of (TOP-REAL n) holds X (-) {(0.REAL n)} = X
let X be Subset of (TOP-REAL n); :: thesis: X (-) {(0.REAL n)} = X
thus X (-) {(0.REAL n)} c= X :: according to XBOOLE_0:def 10 :: thesis: X c= X (-) {(0.REAL n)}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X (-) {(0.REAL n)} or x in X )
assume x in X (-) {(0.REAL n)} ; :: thesis: x in X
then consider y being Point of (TOP-REAL n) such that
A1: ( x = y & {(0.REAL n)} + y c= X ) ;
{x} c= X by A1, Th2;
hence x in X by ZFMISC_1:37; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in X (-) {(0.REAL n)} )
assume A2: x in X ; :: thesis: x in X (-) {(0.REAL n)}
then A3: {x} c= X by ZFMISC_1:37;
reconsider xx = x as Point of (TOP-REAL n) by A2;
{(0.REAL n)} + xx c= X by A3, Th2;
hence x in X (-) {(0.REAL n)} ; :: thesis: verum