for Dftn being With_directed_path Petri_net
for dct being directed_path_like FinSequence of places_and_trans_of Dftn holds [(dct . ((len dct) - 1)),(dct . (len dct))] in the T-S_Arcs of Dftn