let i be Nat; :: thesis:
let Dftn be Petri With_directed_path Petri_net; :: thesis:
let dct be directed_path_like FinSequence of places_and_trans_of Dftn; :: thesis:
assume H1: ( dct . i in places_of dct & 1 < i & i < len dct ) ; :: thesis:
then P1: i in dom dct by FINSEQ_3:25;
then H4: i mod 2 = 1 by Thc, H1;
L1: [(dct . ((len dct) - 1)),(dct . (len dct))] in the T-S_Arcs of Dftn by The;
L2: [(dct . 1),(dct . 2)] in the S-T_Arcs of Dftn by Thd;
consider p being place of Dftn such that
H6: ( p = dct . i & p in rng dct ) by H1;
H8: 1 + 1 <= i by H1, NAT_1:13;
then reconsider im2 = i - 2 as Element of NAT by NAT_1:21;

end;

then H2: im2 mod 2 = 1 by NAT_D:12;
P2: i - 1 < len dct by H1, XREAL_1:147;
then [(dct . im2),(dct . (im2 + 1))] in the S-T_Arcs of Dftn by Def5, H2;
hence [(dct . (i - 2)),(dct . (i - 1))] in the S-T_Arcs of Dftn ; :: thesis:
[(dct . (im2 + 1)),(dct . (im2 + 2))] in the T-S_Arcs of Dftn by Def5, H2, P2;
hence [(dct . (i - 1)),(dct . i)] in the T-S_Arcs of Dftn ; :: thesis:
H9: i + 1 <= len dct by NAT_1:13, H1;
i + 1 <> len dct

end;

then H5: i + 1 < len dct by XXREAL_0:1, H9;
hence [(dct . i),(dct . (i + 1))] in the S-T_Arcs of Dftn by Def5, H4; :: thesis:
thus [(dct . (i + 1)),(dct . (i + 2))] in the T-S_Arcs of Dftn by Def5, H5, H4; :: thesis:
2 <> i

end;