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 (-) (Y + p) = (X (-) Y) + (- p)
let X, Y be Subset of (TOP-REAL n); :: thesis: for p being Point of (TOP-REAL n) holds X (-) (Y + p) = (X (-) Y) + (- p)
let p be Point of (TOP-REAL n); :: thesis: X (-) (Y + p) = (X (-) Y) + (- p)
thus X (-) (Y + p) c= (X (-) Y) + (- p) :: according to XBOOLE_0:def 10 :: thesis: (X (-) Y) + (- p) c= X (-) (Y + p)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X (-) (Y + p) or x in (X (-) Y) + (- p) )
assume x in X (-) (Y + p) ; :: thesis: x in (X (-) Y) + (- p)
then consider y being Point of (TOP-REAL n) such that
A1: ( x = y & (Y + p) + y c= X ) ;
Y + (y + p) c= X by A1, Th16;
then y + p in { y1 where y1 is Point of (TOP-REAL n) : Y + y1 c= X } ;
then (y + p) + (- p) in { (y1 + (- p)) where y1 is Point of (TOP-REAL n) : y1 in X (-) Y } ;
then (y + p) - p in (X (-) Y) + (- p) by EUCLID:45;
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 (-) (Y + p) )
assume x in (X (-) Y) + (- p) ; :: thesis: x in X (-) (Y + p)
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;
x + p = (y - p) + p by A2, EUCLID:45;
then A3: x + p = y by EUCLID:52;
consider y2 being Point of (TOP-REAL n) such that
A4: ( y = y2 & Y + y2 c= X ) by A2;
(Y + p) + x c= X by A3, A4, Th16;
hence x in X (-) (Y + p) ; :: thesis: verum