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

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