let C be Simple_closed_curve; :: thesis: for S being Segmentation of C holds (Segm (S,(len S))) /\ (Segm (S,1)) = {(S /. 1)}
let S be Segmentation of C; :: thesis: (Segm (S,(len S))) /\ (Segm (S,1)) = {(S /. 1)}
A1: Segm (S,(len S)) = Segment ((S /. (len S)),(S /. 1),C) by Def4;
len S >= 8 by Def3;
then 1 < len S by XXREAL_0:2;
then Segm (S,1) = Segment ((S /. 1),(S /. (1 + 1)),C) by Def4;
hence (Segm (S,(len S))) /\ (Segm (S,1)) = {(S /. 1)} by A1, Def3; :: thesis: verum