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

proof

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

end;

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