let C be Simple_closed_curve; :: thesis: for S being Segmentation of C
for j being Element of NAT st 1 < j & j < (len S) -' 1 holds
Segm S,(len S) misses Segm S,j
let S be Segmentation of C; :: thesis: for j being Element of NAT st 1 < j & j < (len S) -' 1 holds
Segm S,(len S) misses Segm S,j
let j be Element of NAT ; :: thesis: ( 1 < j & j < (len S) -' 1 implies Segm S,(len S) misses Segm S,j )
assume that
A1: 1 < j and
A2: j < (len S) -' 1 ; :: thesis: Segm S,(len S) misses Segm S,j
A3: Segm S,(len S) = Segment (S /. (len S)),(S /. 1),C by Def4;
A4: j + 1 < len S by A2, NAT_D:53;
j < len S by A2, NAT_D:44;
then Segm S,j = Segment (S /. j),(S /. (j + 1)),C by A1, Def4;
hence Segm S,(len S) misses Segm S,j by A1, A3, A4, Def3; :: thesis: verum