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

proof

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

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in X + (- x) or y in X (-) {x} )
assume y in X + (- x) ; :: thesis: y in X (-) {x}
then consider p being Point of (TOP-REAL n) such that
A2: ( y = p + (- x) & p in X ) ;
reconsider y = y as Point of (TOP-REAL n) by A2;
y = p - x by A2, EUCLID:45;
then A3: y + x = p by EUCLID:52;
{x} + y c= X

proof

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

end;

hence y in X (-) {x} ; :: thesis: verum