theorem :: PETRI:18

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