:: deftheorem Def4 defines Segm JORDAN_A:def 4 :
for C being Simple_closed_curve
for i being Nat
for S being Segmentation of C holds
( ( 1 <= i & i < len S implies Segm (S,i) = Segment ((S /. i),(S /. (i + 1)),C) ) & ( ( not 1 <= i or not i < len S ) implies Segm (S,i) = Segment ((S /. (len S)),(S /. 1),C) ) );