let M be non empty Reflexive MetrStruct ; 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; 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 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 ;
( 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 ) }
;
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
;
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 for x, y being Point of M st x in S & y in S holds
H1(x,y) <= sXlet x,
y be
Point of
M;
( x in S & y in S implies H1(x,y) <= sX )assume
(
x in S &
y in S )
;
H1(x,y) <= sXthen
H1(
x,
y)
in X
;
hence
H1(
x,
y)
<= sX
by XXREAL_2:4;
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; verum