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

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