:: deftheorem defines Trap-like PETRI:def 10 :
for PTN being Petri_net
for IT being Subset of the carrier of PTN holds
( IT is Trap-like iff IT *' is Subset of (*' IT) );