let C be Simple_closed_curve; 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; 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; ( 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
; 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; verum