let C be Simple_closed_curve; :: thesis: for i being Element of NAT
for S being Segmentation of C st i in dom S holds
Segm S,i c= C
let i be Element of 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:27;
( 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:10; :: thesis: verum