deffunc H_{1}( Nat) -> object = dist_min ((Segm (S,(len S))),(Segm (S,$1)));

deffunc H_{2}( Nat, Nat) -> object = dist_min ((Segm (S,$1)),(Segm (S,$2)));

defpred S_{1}[ Nat] means ( 1 < $1 & $1 < (len S) -' 1 );

defpred S_{2}[ Nat] means $1 in dom S;

defpred S_{3}[ Nat, Nat] means ( 1 <= $1 & $1 < $2 & $2 < len S & $1,$2 aren't_adjacent );

defpred S_{4}[ Nat, Nat] means ( S_{2}[$1] & S_{2}[$2] );

set S1 = { H_{2}(i,j) where i, j is Element of NAT : S_{3}[i,j] } ;

set S2 = { H_{1}(j) where j is Element of NAT : S_{1}[j] } ;

set B = { H_{2}(i,j) where i, j is Element of NAT : S_{4}[i,j] } ;

set B9 = { H_{2}(i,j) where i, j is Element of NAT : ( i in dom S & j in dom S ) } ;

set A = { H_{1}(j) where j is Element of NAT : S_{2}[j] } ;

set A9 = { H_{1}(j) where j is Element of NAT : j in dom S } ;

A1: for j being Element of NAT st S_{1}[j] holds

S_{2}[j]
_{1}(j) where j is Element of NAT : S_{1}[j] } c= { H_{1}(j) where j is Element of NAT : S_{2}[j] }
from FRAENKEL:sch 1(A1);

A5: for i, j being Element of NAT st S_{3}[i,j] holds

S_{4}[i,j]
_{2}(i,j) where i, j is Element of NAT : S_{3}[i,j] } c= { H_{2}(i,j) where i, j is Element of NAT : S_{4}[i,j] }
from FRAENKEL:sch 2(A5);

A10: { H_{2}(i,j) where i, j is Element of NAT : S_{3}[i,j] } c= REAL
_{1}(j) where j is Element of NAT : S_{1}[j] } c= REAL

A13: { H_{1}(j) where j is Element of NAT : j in dom S } is finite
from FRAENKEL:sch 21(A12);

A14: { H_{2}(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 { H_{2}(i,j) where i, j is Element of NAT : S_{3}[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 { H_{1}(j) where j is Element of NAT : S_{1}[j] }
;

then reconsider S1 = { H_{2}(i,j) where i, j is Element of NAT : S_{3}[i,j] } , S2 = { H_{1}(j) where j is Element of NAT : S_{1}[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

deffunc H

defpred S

defpred S

defpred S

defpred S

set S1 = { H

set S2 = { H

set B = { H

set B9 = { H

set A = { H

set A9 = { H

A1: for j being Element of NAT st S

S

proof

A4:
{ H
let j be Element of NAT ; :: thesis: ( S_{1}[j] implies S_{2}[j] )

assume A2: 1 < j ; :: thesis: ( not j < (len S) -' 1 or S_{2}[j] )

A3: (len S) -' 1 <= len S by NAT_D:35;

assume j < (len S) -' 1 ; :: thesis: S_{2}[j]

then j < len S by A3, XXREAL_0:2;

hence S_{2}[j]
by A2, FINSEQ_3:25; :: thesis: verum

end;assume A2: 1 < j ; :: thesis: ( not j < (len S) -' 1 or S

A3: (len S) -' 1 <= len S by NAT_D:35;

assume j < (len S) -' 1 ; :: thesis: S

then j < len S by A3, XXREAL_0:2;

hence S

A5: for i, j being Element of NAT st S

S

proof

A9:
{ H
let i, j be Element of NAT ; :: thesis: ( S_{3}[i,j] implies S_{4}[i,j] )

assume that

A6: 1 <= i and

A7: i < j and

A8: j < len S and

i,j aren't_adjacent ; :: thesis: S_{4}[i,j]

i < len S by A7, A8, XXREAL_0:2;

hence i in dom S by A6, FINSEQ_3:25; :: thesis: S_{2}[j]

1 < j by A6, A7, XXREAL_0:2;

hence S_{2}[j]
by A8, FINSEQ_3:25; :: thesis: verum

end;assume that

A6: 1 <= i and

A7: i < j and

A8: j < len S and

i,j aren't_adjacent ; :: thesis: S

i < len S by A7, A8, XXREAL_0:2;

hence i in dom S by A6, FINSEQ_3:25; :: thesis: S

1 < j by A6, A7, XXREAL_0:2;

hence S

A10: { H

proof

A11:
{ H
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H_{2}(i,j) where i, j is Element of NAT : S_{3}[i,j] } or x in REAL )

assume x in { H_{2}(i,j) where i, j is Element of NAT : S_{3}[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;assume x in { H

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

proof

A12:
dom S is finite
;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H_{1}(j) where j is Element of NAT : S_{1}[j] } or x in REAL )

assume x in { H_{1}(j) where j is Element of NAT : S_{1}[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;assume x in { H

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

A13: { H

A14: { H

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 { H

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 { H

then reconsider S1 = { H

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