theorem Th30: :: JORDAN_A:30

for C being Simple_closed_curve
for S being Segmentation of C holds (Segm (S,(len S))) /\ (Segm (S,((len S) -' 1))) = {(S /. (len S))}