theorem Th7: :: PETRI_2:7

for CPNT1, CPNT2 being Colored_Petri_net
for t1 being transition of CPNT1
for t2 being transition of CPNT2 st the carrier of CPNT1 c= the carrier of CPNT2 & the S-T_Arcs of CPNT1 c= the S-T_Arcs of CPNT2 & the T-S_Arcs of CPNT1 c= the T-S_Arcs of CPNT2 & t1 = t2 holds
( *' {t1} c= *' {t2} & {t1} *' c= {t2} *' )