let i be Nat; 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; 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; ( 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 )
; ( [(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;
then H2:
im1 mod 2 = 1
by NAT_D:12;
i <> len dct
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; [(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
; verum