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