let n be Element of NAT ; :: thesis: for Y, X being Subset of (TOP-REAL n)
for y, x being Point of (TOP-REAL n) holds
( Y + y c= X + x iff Y + (y - x) c= X )
let Y, X be Subset of (TOP-REAL n); :: thesis: for y, x being Point of (TOP-REAL n) holds
( Y + y c= X + x iff Y + (y - x) c= X )
let y, x be Point of (TOP-REAL n); :: thesis: ( Y + y c= X + x iff Y + (y - x) c= X )
thus ( Y + y c= X + x implies Y + (y - x) c= X ) :: thesis: ( Y + (y - x) c= X implies Y + y c= X + x )

proof

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

end;

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