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

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