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

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