let r be real number ; :: thesis: for M being MetrSpace
for A being SubSpace of M
for x being Point of M
for x9 being Point of A st x = x9 holds
Ball x9,r = (Ball x,r) /\ the carrier of A
let M be MetrSpace; :: thesis: for A being SubSpace of M
for x being Point of M
for x9 being Point of A st x = x9 holds
Ball x9,r = (Ball x,r) /\ the carrier of A
let A be SubSpace of M; :: thesis: for x being Point of M
for x9 being Point of A st x = x9 holds
Ball x9,r = (Ball x,r) /\ the carrier of A
let x be Point of M; :: thesis: for x9 being Point of A st x = x9 holds
Ball x9,r = (Ball x,r) /\ the carrier of A
let x9 be Point of A; :: thesis: ( x = x9 implies Ball x9,r = (Ball x,r) /\ the carrier of A )
assume A1: x = x9 ; :: thesis: Ball x9,r = (Ball x,r) /\ the carrier of A

now

let a be set ; :: thesis: ( a in Ball x9,r implies a in (Ball x,r) /\ the carrier of A )
assume A2: a in Ball x9,r ; :: thesis: a in (Ball x,r) /\ the carrier of A
then reconsider y9 = a as Point of A ;
the carrier of A c= the carrier of M by Def1;
then A3: not M is empty by A2;
not A is empty by A2;
then reconsider y = y9 as Point of M by A3, Th12;
dist x9,y9 < r by A2, METRIC_1:12;
then the distance of A . x9,y9 < r by METRIC_1:def 1;
then the distance of M . x,y < r by A1, Def1;
then dist x,y < r by METRIC_1:def 1;
then a in Ball x,r by A3, METRIC_1:12;
hence a in (Ball x,r) /\ the carrier of A by A2, XBOOLE_0:def 4; :: thesis: verum

end;

then A4: Ball x9,r c= (Ball x,r) /\ the carrier of A by TARSKI:def 3;

now

let a be set ; :: thesis: ( a in (Ball x,r) /\ the carrier of A implies a in Ball x9,r )
assume A5: a in (Ball x,r) /\ the carrier of A ; :: thesis: a in Ball x9,r
then reconsider y9 = a as Point of A by XBOOLE_0:def 4;
reconsider y = y9 as Point of M by A5;
a in Ball x,r by A5, XBOOLE_0:def 4;
then dist x,y < r by METRIC_1:12;
then the distance of M . x,y < r by METRIC_1:def 1;
then the distance of A . x9,y9 < r by A1, Def1;
then A6: dist x9,y9 < r by METRIC_1:def 1;
not the carrier of A is empty by A5;
then not A is empty ;
hence a in Ball x9,r by A6, METRIC_1:12; :: thesis: verum

end;

then (Ball x,r) /\ the carrier of A c= Ball x9,r by TARSKI:def 3;
hence Ball x9,r = (Ball x,r) /\ the carrier of A by A4, XBOOLE_0:def 10; :: thesis: verum