deffunc H₁( Element of NAT ) -> Real = diameter (Segm S,$1);
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 diameter (Segm S,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 Element of REAL by XREAL_0:def 1;
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 )
thus ( S1 = { (diameter (Segm S,i)) where i is Element of NAT : i in dom S } & mS1 = max S1 ) ; :: thesis: verum