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

now

let a be set ; :: thesis: ( a in Ball x',r implies a in (Ball x,r) /\ the carrier of A )
assume A2: a in Ball x',r ; :: thesis: a in (Ball x,r) /\ the carrier of A
then reconsider y' = a as Point of ;
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 = y' as Point of by A3, Th12;
dist x',y' < r by A2, METRIC_1:12;
then the distance of A . x',y' < 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 x',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 x',r )
assume A5: a in (Ball x,r) /\ the carrier of A ; :: thesis: a in Ball x',r
then reconsider y' = a as Point of by XBOOLE_0:def 4;
reconsider y = y' as Point of 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 . x',y' < r by A1, Def1;
then A6: dist x',y' < r by METRIC_1:def 1;
not the carrier of A is empty by A5;
then not A is empty ;
hence a in Ball x',r by A6, METRIC_1:12; :: thesis: verum

end;

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