let A be Subset of M; :: thesis: ( A is finite implies A is bounded )
per cases ( A is empty or not A is empty ) ;
suppose A is empty ; :: thesis: ( A is finite implies A is bounded )
hence ( A is finite implies A is bounded ) ; :: thesis: verum
end;
suppose A1: not A is empty ; :: thesis: ( A is finite implies A is bounded )
assume A is finite ; :: thesis: 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 :: thesis: 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 ; :: thesis: ( 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 ) } ; :: thesis: 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 ; :: thesis: 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 ; :: according to TBSP_1:def 7 :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( not x in A or not y in A or dist (x,y) <= sX1 )
assume ( x in A & y in A ) ; :: thesis: dist (x,y) <= sX1
then H1(x,y) in X ;
then H1(x,y) <= sX by XXREAL_2:4;
hence dist (x,y) <= sX1 by XREAL_1:39; :: thesis: verum
end;
end;