let C be Simple_closed_curve; :: thesis: for S being Segmentation of C

for j being 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 Nat st 1 < j & j < (len S) -' 1 holds

Segm (S,(len S)) misses Segm (S,j)

let j be 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

for j being 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 Nat st 1 < j & j < (len S) -' 1 holds

Segm (S,(len S)) misses Segm (S,j)

let j be 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