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) and
A3: q1 in Y ;
reconsider p = p as Point of (TOP-REAL n) by A2;
p = (q1 + y) - x by A2, EUCLID:49;
then A4: p + x = q1 + y by EUCLID:52;
q1 + y in { (q + y) where q is Point of (TOP-REAL n) : q in Y } by A3;
then p + x in X + x by A1, A4;
then consider p1 being Point of (TOP-REAL n) such that
A5: p + x = p1 + x and
A6: p1 in X ;
(p + x) - x = p1 by A5, EUCLID:52;
hence p in X by A6, EUCLID:52; :: thesis: verum

end;

assume A7: 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
A8: p = q1 + y and
A9: q1 in Y ;
reconsider p = p as Point of (TOP-REAL n) by A8;
( p - x = q1 + (y - x) & q1 + (y - x) in { (q + (y - x)) where q is Point of (TOP-REAL n) : q in Y } ) by A8, A9, EUCLID:49;
then (p - x) + x in { (q + x) where q is Point of (TOP-REAL n) : q in X } by A7;
hence p in X + x by EUCLID:52; :: thesis: verum