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