for i being 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 places_of dct & 1 < i & i < len dct holds
( [(dct . (i - 2)),(dct . (i - 1))] in the S-T_Arcs of Dftn & [(dct . (i - 1)),(dct . i)] in the T-S_Arcs of Dftn & [(dct . i),(dct . (i + 1))] in the S-T_Arcs of Dftn & [(dct . (i + 1)),(dct . (i + 2))] in the T-S_Arcs of Dftn & 3 <= i )