:: deftheorem defines With_Deadlocks PETRI:def 9 :
for IT being Petri_net holds
( IT is With_Deadlocks iff ex S being Subset of the carrier of IT st S is Deadlock-like );