:: deftheorem Def7 defines With_directed_circuit PETRI_DF:def 10 :
for PTN being Petri_net holds
( PTN is With_directed_circuit iff ex fs being FinSequence of places_and_trans_of PTN st
( fs is directed_path_like & fs is circular & fs is almost-one-to-one ) );