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) /\ (Segm S,j) = {(S /. (i + 1))}
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) /\ (Segm S,j) = {(S /. (i + 1))}
let i, j be Element of NAT ; :: thesis: ( 1 <= i & i < j & j < len S & i,j are_adjacent1 implies (Segm S,i) /\ (Segm S,j) = {(S /. (i + 1))} )
assume that
A1: 1 <= i and
A2: i < j and
A3: j < len S and
A4: i,j are_adjacent1 ; :: thesis: (Segm S,i) /\ (Segm S,j) = {(S /. (i + 1))}
i < len S by A2, A3, XXREAL_0:2;
then A5: Segm S,i = Segment (S /. i),(S /. (i + 1)),C by A1, Def4;
1 < j by A1, A2, XXREAL_0:2;
then A6: Segm S,j = Segment (S /. j),(S /. (j + 1)),C by A3, Def4;
j + 1 > i by A2, NAT_1:13;
then j = i + 1 by A4, GOBRD10:def 1;
then j + 1 = i + (1 + 1) ;
hence (Segm S,i) /\ (Segm S,j) = {(S /. (i + 1))} by A1, A3, A5, A6, Def3; :: thesis: verum