theorem :: PETRI:17

for PTN being Petri_net
for S being Subset of the carrier of PTN holds
( S is Deadlock-like iff S .: is Trap-like )