let M be non empty Reflexive MetrStruct ; :: thesis: for S being non empty finite Subset of M ex p, q being Point of M st
( p in S & q in S & dist (p,q) = diameter S )
let S be non empty finite Subset of M; :: thesis: ex p, q being Point of M st
( p in S & q in S & dist (p,q) = diameter S )
set q = the Element of S;
reconsider q = the Element of S as Point of M ;
deffunc H₁( Point of M, Point of M) -> object = dist ($1,$2);
set X = { H₁(x,y) where x, y is Point of M : ( x in S & y in S ) } ;

A1: now :: thesis: for x being object st x in { H₁(x,y) where x, y is Point of M : ( x in S & y in S ) } holds
x is real

let x be object ; :: thesis: ( x in { H₁(x,y) where x, y is Point of M : ( x in S & y in S ) } implies x is real )
assume x in { H₁(x,y) where x, y is Point of M : ( x in S & y in S ) } ; :: thesis: x is real
then ex y, z being Point of M st
( x = H₁(y,z) & y in S & z in S ) ;
hence x is real ; :: thesis: verum

end;

A2: H₁(q,q) in { H₁(x,y) where x, y is Point of M : ( x in S & y in S ) } ;
A3: S is finite ;
{ H₁(x,y) where x, y is Point of M : ( x in S & y in S ) } is finite from FRAENKEL:sch 22(A3, A3);
then reconsider X = { H₁(x,y) where x, y is Point of M : ( x in S & y in S ) } as non empty finite real-membered set by A1, A2, MEMBERED:def 3;
reconsider sX = sup X as Real ;
sX in X by XXREAL_2:def 6;
then consider p, q being Point of M such that
A4: ( sX = H₁(p,q) & p in S & q in S ) ;

now :: thesis: for x, y being Point of M st x in S & y in S holds
H₁(x,y) <= sX

let x, y be Point of M; :: thesis: ( x in S & y in S implies H₁(x,y) <= sX )
assume ( x in S & y in S ) ; :: thesis: H₁(x,y) <= sX
then H₁(x,y) in X ;
hence H₁(x,y) <= sX by XXREAL_2:4; :: thesis: verum

end;

then A5: diameter S <= sX by TBSP_1:def 8;
sX <= diameter S by A4, TBSP_1:def 8;
hence ex p, q being Point of M st
( p in S & q in S & dist (p,q) = diameter S ) by A4, A5, XXREAL_0:1; :: thesis: verum