let PTN be Petri_net; :: thesis: for S being Subset of the carrier of PTN holds
( S is Trap-like iff S .: is Deadlock-like )
let S be Subset of the carrier of PTN; :: thesis: ( S is Trap-like iff S .: is Deadlock-like )
A1: (S .:) *' = *' S by Th15;
thus ( S is Trap-like implies S .: is Deadlock-like ) by A1, Th16; :: thesis: ( S .: is Deadlock-like implies S is Trap-like )
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