for Dftn being Petri decision_free_like With_directed_path Petri_net
for dct being directed_path_like FinSequence of places_and_trans_of Dftn
for t being transition of Dftn st dct is circular & ex p1 being place of Dftn st
( p1 in places_of dct & ( [p1,t] in the S-T_Arcs of Dftn or [t,p1] in the T-S_Arcs of Dftn ) ) holds
t in transitions_of dct