let A be Subset of M; ( A is finite implies A is bounded )
per cases
( A is empty or not A is empty )
;
suppose A1:
not
A is
empty
;
( A is finite implies A is bounded )assume
A is
finite
;
A is bounded then reconsider a =
A as non
empty finite Subset of
M by A1;
deffunc H1(
Point of
M,
Point of
M)
-> object =
dist (
M,
c2);
consider q being
object such that A2:
q in a
by XBOOLE_0:def 1;
set X =
{ H1(x,y) where x, y is Point of M : ( x in a & y in a ) } ;
reconsider q =
q as
Point of
M by A2;
A3:
H1(
q,
q)
in { H1(x,y) where x, y is Point of M : ( x in a & y in a ) }
by A2;
A4:
now for x being object st x in { H1(x,y) where x, y is Point of M : ( x in a & y in a ) } holds
x is real let x be
object ;
( x in { H1(x,y) where x, y is Point of M : ( x in a & y in a ) } implies x is real )assume
x in { H1(x,y) where x, y is Point of M : ( x in a & y in a ) }
;
x is real then
ex
y,
z being
Point of
M st
(
x = H1(
y,
z) &
y in a &
z in a )
;
hence
x is
real
;
verum end; A5:
a is
finite
;
{ H1(x,y) where x, y is Point of M : ( x in a & y in a ) } is
finite
from FRAENKEL:sch 22(A5, A5);
then reconsider X =
{ H1(x,y) where x, y is Point of M : ( x in a & y in a ) } as non
empty finite real-membered set by A3, A4, MEMBERED:def 3;
reconsider sX =
sup X as
Real ;
reconsider sX1 =
sX + 1 as
Real ;
take
sX1
;
TBSP_1:def 7 ( not sX1 <= 0 & ( for b1, b2 being Element of the carrier of M holds
( not b1 in A or not b2 in A or dist (b1,b2) <= sX1 ) ) )
(
H1(
q,
q)
= 0 &
H1(
q,
q)
<= sX )
by A3, METRIC_1:1, XXREAL_2:4;
hence
0 < sX1
;
for b1, b2 being Element of the carrier of M holds
( not b1 in A or not b2 in A or dist (b1,b2) <= sX1 )let x,
y be
Point of
M;
( not x in A or not y in A or dist (x,y) <= sX1 )assume
(
x in A &
y in A )
;
dist (x,y) <= sX1then
H1(
x,
y)
in X
;
then
H1(
x,
y)
<= sX
by XXREAL_2:4;
hence
dist (
x,
y)
<= sX1
by XREAL_1:39;
verum end; end;