let r be Real; :: 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 :: thesis: for a being object st a in Ball (x9,r) holds
a in (Ball (x,r)) /\ the carrier of A

let a be object ; :: 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, Th8;
dist (x9,y9) < r by A2, METRIC_1:11;
then the distance of A . (x9,y9) < r ;
then the distance of M . (x,y) < r by A1, Def1;
then dist (x,y) < r ;
then a in Ball (x,r) by A3, METRIC_1:11;
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 ;

now :: thesis: for a being object st a in (Ball (x,r)) /\ the carrier of A holds
a in Ball (x9,r)

let a be object ; :: 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:11;
then the distance of M . (x,y) < r ;
then the distance of A . (x9,y9) < r by A1, Def1;
then A6: dist (x9,y9) < r ;
not the carrier of A is empty by A5;
then not A is empty ;
hence a in Ball (x9,r) by A6, METRIC_1:11; :: thesis: verum

end;

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