let C be Simple_closed_curve; 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; 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; ( 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
; (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; verum