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