let r be Real; 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; 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; 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; 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; ( x = x9 implies Ball (x9,r) = (Ball (x,r)) /\ the carrier of A )
assume A1:
x = x9
; Ball (x9,r) = (Ball (x,r)) /\ the carrier of A
now for a being object st a in Ball (x9,r) holds
a in (Ball (x,r)) /\ the carrier of Alet a be
object ;
( a in Ball (x9,r) implies a in (Ball (x,r)) /\ the carrier of A )assume A2:
a in Ball (
x9,
r)
;
a in (Ball (x,r)) /\ the carrier of Athen 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;
verum end;
then A4:
Ball (x9,r) c= (Ball (x,r)) /\ the carrier of A
;
now for a being object st a in (Ball (x,r)) /\ the carrier of A holds
a in Ball (x9,r)let a be
object ;
( 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
;
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;
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; verum