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:235, 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