:: deftheorem Def9 defines With_directed_path PETRI_DF:def 9 :
for IT being Petri_net holds
( IT is With_directed_path iff ex fs being FinSequence of places_and_trans_of IT st fs is directed_path_like );