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

for i, j being Nat st 1 <= i & i < j & j < len S & i,j aren't_adjacent holds

Segm (S,i) misses Segm (S,j)

let S be Segmentation of C; :: thesis: for i, j being Nat st 1 <= i & i < j & j < len S & i,j aren't_adjacent holds

Segm (S,i) misses Segm (S,j)

let i, j be Nat; :: thesis: ( 1 <= i & i < j & j < len S & i,j aren't_adjacent implies Segm (S,i) misses Segm (S,j) )

assume that

A1: 1 <= i and

A2: i < j and

A3: j < len S and

A4: i,j aren't_adjacent ; :: thesis: Segm (S,i) misses Segm (S,j)

i < len S by A2, A3, XXREAL_0:2;

then A5: Segm (S,i) = Segment ((S /. i),(S /. (i + 1)),C) by A1, Def4;

1 < j by A1, A2, XXREAL_0:2;

then Segm (S,j) = Segment ((S /. j),(S /. (j + 1)),C) by A3, Def4;

hence Segm (S,i) misses Segm (S,j) by A1, A2, A3, A4, A5, Def3; :: thesis: verum

for i, j being Nat st 1 <= i & i < j & j < len S & i,j aren't_adjacent holds

Segm (S,i) misses Segm (S,j)

let S be Segmentation of C; :: thesis: for i, j being Nat st 1 <= i & i < j & j < len S & i,j aren't_adjacent holds

Segm (S,i) misses Segm (S,j)

let i, j be Nat; :: thesis: ( 1 <= i & i < j & j < len S & i,j aren't_adjacent implies Segm (S,i) misses Segm (S,j) )

assume that

A1: 1 <= i and

A2: i < j and

A3: j < len S and

A4: i,j aren't_adjacent ; :: thesis: Segm (S,i) misses Segm (S,j)

i < len S by A2, A3, XXREAL_0:2;

then A5: Segm (S,i) = Segment ((S /. i),(S /. (i + 1)),C) by A1, Def4;

1 < j by A1, A2, XXREAL_0:2;

then Segm (S,j) = Segment ((S /. j),(S /. (j + 1)),C) by A3, Def4;

hence Segm (S,i) misses Segm (S,j) by A1, A2, A3, A4, A5, Def3; :: thesis: verum