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