let C be Simple_closed_curve; :: thesis: for i being Nat
for S being Segmentation of C st i in dom S holds
Segm (S,i) c= C
let i be Nat; :: thesis: for S being Segmentation of C st i in dom S holds
Segm (S,i) c= C
let S be Segmentation of C; :: thesis: ( i in dom S implies Segm (S,i) c= C )
assume i in dom S ; :: thesis: Segm (S,i) c= C
then A1: 1 <= i by FINSEQ_3:25;
( i < len S or i >= len S ) ;
then ( Segm (S,i) = Segment ((S /. i),(S /. (i + 1)),C) or Segm (S,i) = Segment ((S /. (len S)),(S /. 1),C) ) by A1, Def4;
hence Segm (S,i) c= C by JORDAN16:6; :: thesis: verum