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 ;
dist (x9,y9) < r by ;
then the distance of A . (x9,y9) < r ;
then the distance of M . (x,y) < r by ;
then dist (x,y) < r ;
then a in Ball (x,r) by ;
hence a in (Ball (x,r)) /\ the carrier of A by ; :: 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 ;
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 ;
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 ; :: 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 ; :: thesis: verum