theorem :: PETRI:13

for PTN being Petri_net holds (PTN .:) .: = PT_net_Str(# the carrier of PTN, the carrier' of PTN, the S-T_Arcs of PTN, the T-S_Arcs of PTN #) ;