deffunc H1( Nat) -> object = dist_min ((Segm (S,(len S))),(Segm (S,$1)));
deffunc H2( Nat, Nat) -> object = dist_min ((Segm (S,$1)),(Segm (S,$2)));
defpred S1[ Nat] means ( 1 < $1 & $1 < (len S) -' 1 );
defpred S2[ Nat] means $1 in dom S;
defpred S3[ Nat, Nat] means ( 1 <= $1 & $1 < $2 & $2 < len S & $1,$2 aren't_adjacent );
defpred S4[ Nat, Nat] means ( S2[$1] & S2[$2] );
set S1 = { H2(i,j) where i, j is Element of NAT : S3[i,j] } ;
set S2 = { H1(j) where j is Element of NAT : S1[j] } ;
set B = { H2(i,j) where i, j is Element of NAT : S4[i,j] } ;
set B9 = { H2(i,j) where i, j is Element of NAT : ( i in dom S & j in dom S ) } ;
set A = { H1(j) where j is Element of NAT : S2[j] } ;
set A9 = { H1(j) where j is Element of NAT : j in dom S } ;
A1: for j being Element of NAT st S1[j] holds
S2[j]
proof
let j be Element of NAT ; :: thesis: ( S1[j] implies S2[j] )
assume A2: 1 < j ; :: thesis: ( not j < (len S) -' 1 or S2[j] )
A3: (len S) -' 1 <= len S by NAT_D:35;
assume j < (len S) -' 1 ; :: thesis: S2[j]
then j < len S by A3, XXREAL_0:2;
hence S2[j] by A2, FINSEQ_3:25; :: thesis: verum
end;
A4: { H1(j) where j is Element of NAT : S1[j] } c= { H1(j) where j is Element of NAT : S2[j] } from FRAENKEL:sch 1(A1);
 A5: for i, j being Element of NAT st S3[i,j] holds
S4[i,j]
proof
let i, j be Element of NAT ; :: thesis: ( S3[i,j] implies S4[i,j] )
assume that
A6: 1 <= i and
A7: i < j and
A8: j < len S and
i,j aren't_adjacent ; :: thesis: S4[i,j]
i < len S by A7, A8, XXREAL_0:2;
hence i in dom S by A6, FINSEQ_3:25; :: thesis: S2[j]
1 < j by A6, A7, XXREAL_0:2;
hence S2[j] by A8, FINSEQ_3:25; :: thesis: verum
end;
A9: { H2(i,j) where i, j is Element of NAT : S3[i,j] } c= { H2(i,j) where i, j is Element of NAT : S4[i,j] } from FRAENKEL:sch 2(A5);
 A10: { H2(i,j) where i, j is Element of NAT : S3[i,j] } c= REAL
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H2(i,j) where i, j is Element of NAT : S3[i,j] } or x in REAL )
assume x in { H2(i,j) where i, j is Element of NAT : S3[i,j] } ; :: thesis: x in REAL
then ex i, j being Element of NAT st
( x = dist_min ((Segm (S,i)),(Segm (S,j))) & 1 <= i & i < j & j < len S & i,j aren't_adjacent ) ;
hence x in REAL by XREAL_0:def 1; :: thesis: verum
end;
A11: { H1(j) where j is Element of NAT : S1[j] } c= REAL
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H1(j) where j is Element of NAT : S1[j] } or x in REAL )
assume x in { H1(j) where j is Element of NAT : S1[j] } ; :: thesis: x in REAL
then ex j being Element of NAT st
( x = dist_min ((Segm (S,(len S))),(Segm (S,j))) & 1 < j & j < (len S) -' 1 ) ;
hence x in REAL by XREAL_0:def 1; :: thesis: verum
end;
A12: dom S is finite ;
A13: { H1(j) where j is Element of NAT : j in dom S } is finite from FRAENKEL:sch 21(A12);
 A14: { H2(i,j) where i, j is Element of NAT : ( i in dom S & j in dom S ) } is finite from FRAENKEL:sch 22(A12, A12);
 A15: 3 <> 1 + 1 ;
1 <> 3 + 1 ;
then A16: 1,3 aren't_adjacent by A15, GOBRD10:def 1;
A17: len S >= 7 + 1 by Def3;
then 3 < len S by XXREAL_0:2;
then A18: dist_min ((Segm (S,1)),(Segm (S,3))) in { H2(i,j) where i, j is Element of NAT : S3[i,j] } by A16;
2 + 1 < len S by A17, XXREAL_0:2;
then 2 < (len S) -' 1 by NAT_D:52;
then dist_min ((Segm (S,(len S))),(Segm (S,2))) in { H1(j) where j is Element of NAT : S1[j] } ;
then reconsider S1 = { H2(i,j) where i, j is Element of NAT : S3[i,j] } , S2 = { H1(j) where j is Element of NAT : S1[j] } as non empty finite Subset of REAL by A4, A9, A10, A11, A13, A14, A18;
reconsider mm = min ((min S1),(min S2)) as Element of REAL by XREAL_0:def 1;
take mm ; :: thesis: ex S1, S2 being non empty finite Subset of REAL st
( S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & i,j aren't_adjacent ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & mm = min ((min S1),(min S2)) )
take S1 ; :: thesis: ex S2 being non empty finite Subset of REAL st
( S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & i,j aren't_adjacent ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & mm = min ((min S1),(min S2)) )
take S2 ; :: thesis: ( S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & i,j aren't_adjacent ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & mm = min ((min S1),(min S2)) )
thus ( S1 = { (dist_min ((Segm (S,i)),(Segm (S,j)))) where i, j is Element of NAT : ( 1 <= i & i < j & j < len S & i,j aren't_adjacent ) } & S2 = { (dist_min ((Segm (S,(len S))),(Segm (S,k)))) where k is Element of NAT : ( 1 < k & k < (len S) -' 1 ) } & mm = min ((min S1),(min S2)) ) ; :: thesis: verum