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 H₁( Point of M, Point of M) -> object = dist (M,c₂);
consider q being object such that
A2: q in a by XBOOLE_0:def 1;
set X = { H₁(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: H₁(q,q) in { H₁(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 { H₁(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 { H₁(x,y) where x, y is Point of M : ( x in a & y in a ) } implies x is real )
assume x in { H₁(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 = H₁(y,z) & y in a & z in a ) ;
hence x is real ; :: thesis: verum

end;

A5: a is finite ;
{ H₁(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 = { H₁(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 b₁, b₂ being Element of the carrier of M holds
( not b₁ in A or not b₂ in A or dist (b₁,b₂) <= sX1 ) ) )
( H₁(q,q) = 0 & H₁(q,q) <= sX ) by A3, METRIC_1:1, XXREAL_2:4;
hence 0 < sX1 ; :: thesis: for b₁, b₂ being Element of the carrier of M holds
( not b₁ in A or not b₂ in A or dist (b₁,b₂) <= 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 H₁(x,y) in X ;
then H₁(x,y) <= sX by XXREAL_2:4;
hence dist (x,y) <= sX1 by XREAL_1:39; :: thesis: verum

end;

end;