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

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