:: deftheorem defines places_of PETRI_DF:def 3 :
for PTN being Petri_net
for fs being FinSequence of places_and_trans_of PTN holds places_of fs = { p where p is place of PTN : p in rng fs } ;