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 Th30;
hence Segm (S,(len S)) meets Segm (S,((len S) -' 1)) ; :: thesis: verum