theorem Th12: :: PETRI_DF:4

for fs being FinSequence of places_and_trans_of PetriNet st fs = <*0,1,0*> holds
fs is directed_path_like