let r be real number ; :: thesis: for M being MetrSpace
for A being SubSpace of M
for x being Point of M
for x' being Point of A 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 M
for x' being Point of A 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 M
for x' being Point of A st x = x' holds
Ball x',r = (Ball x,r) /\ the carrier of A
let x be Point of M; :: thesis: for x' being Point of A st x = x' holds
Ball x',r = (Ball x,r) /\ the carrier of A
let x' be Point of A; :: 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 A3: a in the carrier of A ;
reconsider y' = a as Point of A by A2;
A4: not A is empty by A2;
A5: not M is empty

proof

the carrier of A c= the carrier of M by Def1;
hence not the carrier of M is empty by A3; :: according to STRUCT_0:def 1 :: thesis: verum

end;

then reconsider y = y' as Point of M by A4, 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 A5, METRIC_1:12;
hence a in (Ball x,r) /\ the carrier of A by A2, XBOOLE_0:def 4; :: thesis: verum

end;

then A6: 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 A7: a in (Ball x,r) /\ the carrier of A ; :: thesis: a in Ball x',r
then A8: ( a in Ball x,r & a in the carrier of A ) by XBOOLE_0:def 4;
A9: not A is empty

proof

thus not the carrier of A is empty by A7; :: according to STRUCT_0:def 1 :: thesis: verum

end;

A10: not M is empty by A7;
reconsider y' = a as Point of A by A7, XBOOLE_0:def 4;
reconsider y = y' as Point of M by A9, A10, Th12;
dist x,y < r by A8, 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 dist x',y' < r by METRIC_1:def 1;
hence a in Ball x',r by A9, 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 A6, XBOOLE_0:def 10; :: thesis: verum