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