let PTN be Petri_net; :: thesis: for S being Subset of the carrier of PTN holds
( S is Deadlock-like iff S .: is Trap-like )
let S be Subset of the carrier of PTN; :: thesis: ( S is Deadlock-like iff S .: is Trap-like )
A1: (S .: ) *' = *' S by Th15;
thus ( S is Deadlock-like implies S .: is Trap-like ) :: thesis: ( S .: is Trap-like implies S is Deadlock-like )

proof

assume *' S is Subset of (S *' ) ; :: according to PETRI:def 8 :: thesis: S .: is Trap-like
hence (S .: ) *' is Subset of (*' (S .: )) by A1, Th16; :: according to PETRI:def 10 :: thesis: verum

end;

assume (S .: ) *' is Subset of (*' (S .: )) ; :: according to PETRI:def 10 :: thesis: S is Deadlock-like
hence *' S is Subset of (S *' ) by A1, Th16; :: according to PETRI:def 8 :: thesis: verum