deffunc H₁( Nat) -> Element of REAL = In ((diameter (Segm (S,$1))),REAL);
defpred S₁[ set ] means $1 in dom S;
set S1 = { H₁(i) where i is Element of NAT : S₁[i] } ;
set S2 = { H₁(i) where i is Element of NAT : i in dom S } ;
A1: dom S is finite ;
A2: { H₁(i) where i is Element of NAT : i in dom S } is finite from FRAENKEL:sch 21(A1);
A3: { H₁(i) where i is Element of NAT : S₁[i] } is Subset of REAL from DOMAIN_1:sch 8();
1 in dom S by FINSEQ_5:6;
then H₁(1) in { H₁(i) where i is Element of NAT : S₁[i] } ;
then reconsider S1 = { H₁(i) where i is Element of NAT : S₁[i] } as non empty finite Subset of REAL by A2, A3;
reconsider mS1 = max S1 as Real ;
take mS1 ; :: thesis: ex S1 being non empty finite Subset of REAL st
( S1 = { (diameter (Segm (S,i))) where i is Element of NAT : i in dom S } & mS1 = max S1 )
take S1 ; :: thesis: ( S1 = { (diameter (Segm (S,i))) where i is Element of NAT : i in dom S } & mS1 = max S1 )
deffunc H₂( Nat) -> Real = diameter (Segm (S,$1));
A4: for i being Element of NAT holds H₁(i) = H₂(i) ;
{ H₁(i) where i is Element of NAT : S₁[i] } = { H₂(j) where j is Element of NAT : S₁[j] } from FRAENKEL:sch 5(A4);
hence ( S1 = { (diameter (Segm (S,i))) where i is Element of NAT : i in dom S } & mS1 = max S1 ) ; :: thesis: verum