let i be Nat; :: thesis: for Dftn being Petri With_directed_path Petri_net
for dct being directed_path_like FinSequence of places_and_trans_of Dftn st dct . i in transitions_of dct & i in dom dct holds
( [(dct . (i - 1)),(dct . i)] in the S-T_Arcs of Dftn & [(dct . i),(dct . (i + 1))] in the T-S_Arcs of Dftn )
let Dftn be Petri With_directed_path Petri_net; :: thesis: for dct being directed_path_like FinSequence of places_and_trans_of Dftn st dct . i in transitions_of dct & i in dom dct holds
( [(dct . (i - 1)),(dct . i)] in the S-T_Arcs of Dftn & [(dct . i),(dct . (i + 1))] in the T-S_Arcs of Dftn )
let dct be directed_path_like FinSequence of places_and_trans_of Dftn; :: thesis: ( dct . i in transitions_of dct & i in dom dct implies ( [(dct . (i - 1)),(dct . i)] in the S-T_Arcs of Dftn & [(dct . i),(dct . (i + 1))] in the T-S_Arcs of Dftn ) )
assume H1: ( dct . i in transitions_of dct & i in dom dct ) ; :: thesis: ( [(dct . (i - 1)),(dct . i)] in the S-T_Arcs of Dftn & [(dct . i),(dct . (i + 1))] in the T-S_Arcs of Dftn )
L1: [(dct . ((len dct) - 1)),(dct . (len dct))] in the T-S_Arcs of Dftn by The;
reconsider im1 = i - 1 as Element of NAT by NAT_1:21, FINSEQ_3:25, H1;
consider t being transition of Dftn such that
H6: ( t = dct . i & t in rng dct ) by H1;
H4: ( 1 <= i & i <= len dct ) by FINSEQ_3:25, H1;

now :: thesis: not im1 mod 2 = 0

assume im1 mod 2 = 0 ; :: thesis: contradiction
then (im1 + 1) mod 2 = 1 by NAT_D:16;
hence contradiction by Thcc, H1; :: thesis: verum

end;

then H2: im1 mod 2 = 1 by NAT_D:12;
i <> len dct

proof

assume i = len dct ; :: thesis: contradiction
then dct . i in the carrier of Dftn by L1, ZFMISC_1:87;
hence contradiction by H6, NET_1:def 2, XBOOLE_0:3; :: thesis: verum

end;

then H3: im1 + 1 < len dct by XXREAL_0:1, H4;
hence [(dct . (i - 1)),(dct . i)] in the S-T_Arcs of Dftn by Def5, H2; :: thesis: [(dct . i),(dct . (i + 1))] in the T-S_Arcs of Dftn
[(dct . (im1 + 1)),(dct . (im1 + 2))] in the T-S_Arcs of Dftn by Def5, H2, H3;
hence [(dct . i),(dct . (i + 1))] in the T-S_Arcs of Dftn ; :: thesis: verum