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 Th28;

hence Segm (S,(len S)) meets Segm (S,1) ; :: thesis: verum

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 Th28;

hence Segm (S,(len S)) meets Segm (S,1) ; :: thesis: verum