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

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

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

then A4:
Ball (x9,r) c= (Ball (x,r)) /\ the carrier of A
;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;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

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

a in Ball (x9,r)

then
(Ball (x,r)) /\ the carrier of A c= Ball (x9,r)
;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;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

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