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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (X + p) (-) Y or x in (X (-) Y) + p )
assume x in (X + p) (-) Y ; :: thesis: x in (X (-) Y) + p
then consider y being Point of (TOP-REAL n) such that
A1: ( x = y & Y + y c= X + p ) ;
Y + (y - p) c= X by A1, Th13;
then y - p in { y1 where y1 is Point of (TOP-REAL n) : Y + y1 c= X } ;
then (y - p) + p in { (q + p) where q is Point of (TOP-REAL n) : q in X (-) Y } ;
hence x in (X (-) Y) + p by A1, EUCLID:52; :: thesis: verum

end;

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