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