let C be Simple_closed_curve; :: thesis: for S being Segmentation of C holds (Segm S,(len S)) /\ (Segm S,((len S) -' 1)) = {(S /. (len S))}
let S be Segmentation of C; :: thesis: (Segm S,(len S)) /\ (Segm S,((len S) -' 1)) = {(S /. (len S))}
A1: Segm S,(len S) = Segment (S /. (len S)),(S /. 1),C by Def4;
A2: len S >= 8 by Def3;
then len S >= 1 + 1 by XXREAL_0:2;
then A3: 1 <= (len S) -' 1 by NAT_D:55;
A4: ((len S) -' 1) + 1 = len S by A2, XREAL_1:237, XXREAL_0:2;
then (len S) -' 1 < len S by NAT_1:13;
then Segm S,((len S) -' 1) = Segment (S /. ((len S) -' 1)),(S /. (len S)),C by A3, A4, Def4;
hence (Segm S,(len S)) /\ (Segm S,((len S) -' 1)) = {(S /. (len S))} by A1, Def3; :: thesis: verum