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