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 that
A1: 1 <= i and
A2: i < j and
A3: j < len S and
A4: i,j are_adjacent1 ; :: thesis: Segm (S,i) meets Segm (S,j)
(Segm (S,i)) /\ (Segm (S,j)) = {(S /. (i + 1))} by A1, A2, A3, A4, Th27;
hence Segm (S,i) meets Segm (S,j) by XBOOLE_0:def 7; :: thesis: verum