let C be Simple_closed_curve; :: thesis: for S being Segmentation of C
for i, j being Element of NAT st 1 <= i & i < j & j < len S & i,j are_adjacent1 holds
Segm S,i meets Segm S,j
let S be Segmentation of C; :: thesis: for i, j being Element of NAT st 1 <= i & i < j & j < len S & i,j are_adjacent1 holds
Segm S,i meets Segm S,j
let i, j be Element of NAT ; :: thesis: ( 1 <= i & i < j & j < len S & i,j are_adjacent1 implies Segm S,i meets Segm S,j )
assume ( 1 <= i & i < j & j < len S & i,j are_adjacent1 ) ; :: thesis: Segm S,i meets Segm S,j
then (Segm S,i) /\ (Segm S,j) = {(S /. (i + 1))} by Th27;
hence Segm S,i meets Segm S,j by XBOOLE_0:def 7; :: thesis: verum