let C be Simple_closed_curve; :: thesis: for S being Segmentation of C holds Segm S,(len S) meets Segm S,1
let S be Segmentation of C; :: thesis: Segm S,(len S) meets Segm S,1
(Segm S,(len S)) /\ (Segm S,1) = {(S /. 1)} by Th29;
hence Segm S,(len S) meets Segm S,1 by XBOOLE_0:def 7; :: thesis: verum