let C be Simple_closed_curve; :: thesis: for S being Segmentation of C
for i, j being Nat st 1 <= i & i < j & j < len S & i,j are_adjacent holds
(Segm (S,i)) /\ (Segm (S,j)) = {(S /. (i + 1))}
let S be Segmentation of C; :: thesis: for i, j being Nat st 1 <= i & i < j & j < len S & i,j are_adjacent holds
(Segm (S,i)) /\ (Segm (S,j)) = {(S /. (i + 1))}
let i, j be Nat; :: thesis: ( 1 <= i & i < j & j < len S & i,j are_adjacent 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_adjacent ; :: 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