let n be Nat; :: thesis:
let p, q be Point of (TOP-REAL n); :: thesis:
let r be Real; :: thesis:
set TR = TOP-REAL n;
set T = transl (p,(TOP-REAL n));

end;

let x be Point of (TOP-REAL n); :: thesis:
thus (x + p) - (q + p) = ((x + p) - p) - q by RLVECT_1:27
.= (x + (p - p)) - q by RLVECT_1:28
.= (x + (0. (TOP-REAL n))) - q by RLVECT_1:def 10
.= x - q by RLVECT_1:def 4 ; :: thesis:

end;

thus (transl (p,(TOP-REAL n))) .: (Ball (q,r)) c= Ball ((q + p),r) :: according to XBOOLE_0:def 10 :: thesis:

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in (transl (p,(TOP-REAL n))) .: (Ball (q,r)) ; :: thesis:
then consider x being object such that
A5: x in dom (transl (p,(TOP-REAL n))) and
A6: x in Ball (q,r) and
A7: (transl (p,(TOP-REAL n))) . x = y by FUNCT_1:def 6;
reconsider x = x as Point of (TOP-REAL n) by A5;
A8: y = x + p by A7, RLTOPSP1:def 10;
A9: (x + p) - (q + p) = x - q by A3;
|.(x - q).| < r by A6, TOPREAL9:7;
hence y in Ball ((q + p),r) by A9, A8; :: thesis:

end;

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A10: y in Ball ((q + p),r) ; :: thesis:
then reconsider y = y as Point of (TOP-REAL n) ;
A11: (y - p) - q = y - (p + q) by RLVECT_1:27;
|.(y - (q + p)).| < r by A10, TOPREAL9:7;
then A12: y - p in Ball (q,r) by A11;
(transl (p,(TOP-REAL n))) . (y - p) = y by A2;
hence y in (transl (p,(TOP-REAL n))) .: (Ball (q,r)) by A12, A4, FUNCT_1:def 6; :: thesis:

end;

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in (transl (p,(TOP-REAL n))) .: (cl_Ball (q,r)) ; :: thesis:
then consider x being object such that
A13: x in dom (transl (p,(TOP-REAL n))) and
A14: x in cl_Ball (q,r) and
A15: (transl (p,(TOP-REAL n))) . x = y by FUNCT_1:def 6;
reconsider x = x as Point of (TOP-REAL n) by A13;
A16: y = x + p by A15, RLTOPSP1:def 10;
A17: (x + p) - (q + p) = x - q by A3;
|.(x - q).| <= r by A14, TOPREAL9:8;
hence y in cl_Ball ((q + p),r) by A17, A16; :: thesis:

end;

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A18: y in cl_Ball ((q + p),r) ; :: thesis:
then reconsider y = y as Point of (TOP-REAL n) ;
A19: (y - p) - q = y - (p + q) by RLVECT_1:27;
|.(y - (q + p)).| <= r by A18, TOPREAL9:8;
then A20: y - p in cl_Ball (q,r) by A19;
(transl (p,(TOP-REAL n))) . (y - p) = y by A2;
hence y in (transl (p,(TOP-REAL n))) .: (cl_Ball (q,r)) by A20, A4, FUNCT_1:def 6; :: thesis:

end;

thus (transl (p,(TOP-REAL n))) .: (Sphere (q,r)) c= Sphere ((q + p),r) :: according to XBOOLE_0:def 10 :: thesis:

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in (transl (p,(TOP-REAL n))) .: (Sphere (q,r)) ; :: thesis:
then consider x being object such that
A21: x in dom (transl (p,(TOP-REAL n))) and
A22: x in Sphere (q,r) and
A23: (transl (p,(TOP-REAL n))) . x = y by FUNCT_1:def 6;
reconsider x = x as Point of (TOP-REAL n) by A21;
A24: y = x + p by A23, RLTOPSP1:def 10;
A25: (x + p) - (q + p) = x - q by A3;
|.(x - q).| = r by A22, TOPREAL9:9;
hence y in Sphere ((q + p),r) by A25, A24; :: thesis:

end;

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A26: y in Sphere ((q + p),r) ; :: thesis:
then reconsider y = y as Point of (TOP-REAL n) ;
A27: (y - p) - q = y - (p + q) by RLVECT_1:27;
|.(y - (q + p)).| = r by A26, TOPREAL9:9;
then A28: y - p in Sphere (q,r) by A27;
(transl (p,(TOP-REAL n))) . (y - p) = y by A2;
hence y in (transl (p,(TOP-REAL n))) .: (Sphere (q,r)) by A28, A4, FUNCT_1:def 6; :: thesis: