:: deftheorem Def6 defines transition PNPROC_1:def 6 :
for P, b₂ being set holds
( b₂ is transition of P iff ex m1, m2 being marking of P st b₂ = [m1,m2] );