:: deftheorem Def2 defines Petri NET_1:def 2 :
for N being PT_net_Str holds
( N is Petri iff ( the carrier of N misses the carrier' of N & Flow N c= [: the carrier of N, the carrier' of N:] \/ [: the carrier' of N, the carrier of N:] ) );