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 ;
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 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 ;
hence i in dom S by ; :: thesis: S2[j]
1 < j by ;
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 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:
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:
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 A14: { H2(i,j) where i, j is Element of NAT : ( i in dom S & j in dom S ) } is finite from A15: 3 <> 1 + 1 ;
1 <> 3 + 1 ;
then A16: 1,3 aren't_adjacent by ;
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 ;
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