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 H1( Point of M, Point of M) -> object = dist ($1,$2);
set X = { H1(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 { H1(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 { H1(x,y) where x, y is Point of M : ( x in S & y in S ) } implies x is real )
assume x in { H1(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 = H1(y,z) & y in S & z in S ) ;
hence x is real ; :: thesis: verum
end;
A2: H1(q,q) in { H1(x,y) where x, y is Point of M : ( x in S & y in S ) } ;
A3: S is finite ;
{ H1(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 = { H1(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 = H1(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
H1(x,y) <= sX
let x, y be Point of M; :: thesis: ( x in S & y in S implies H1(x,y) <= sX )
assume ( x in S & y in S ) ; :: thesis: H1(x,y) <= sX
then H1(x,y) in X ;
hence H1(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