let C be Simple_closed_curve; :: thesis: for S being Segmentation of C
for i, j being Element of NAT st 1 <= i & i < j & j < len S & not i,j are_adjacent1 holds
Segm S,i misses Segm S,j
let S be Segmentation of C; :: thesis: for i, j being Element of NAT st 1 <= i & i < j & j < len S & not i,j are_adjacent1 holds
Segm S,i misses Segm S,j
let i, j be Element of NAT ; :: thesis: ( 1 <= i & i < j & j < len S & not i,j are_adjacent1 implies Segm S,i misses Segm S,j )
assume that
A1: 1 <= i and
A2: i < j and
A3: j < len S and
A4: not i,j are_adjacent1 ; :: 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