let Dftn be With_directed_path Petri_net; :: thesis: for dct being directed_path_like FinSequence of places_and_trans_of Dftn holds [(dct . 1),(dct . 2)] in the S-T_Arcs of Dftn
let dct be directed_path_like FinSequence of places_and_trans_of Dftn; :: thesis: [(dct . 1),(dct . 2)] in the S-T_Arcs of Dftn
A3: 1 mod 2 = 1 by NAT_D:14;
len dct >= 3 by Def5;
then 1 + 1 < len dct by XXREAL_0:2;
hence [(dct . 1),(dct . 2)] in the S-T_Arcs of Dftn by Def5, A3; :: thesis: verum