let CPNT1, CPNT2 be Colored_Petri_net; :: thesis: 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} *' )
let t1 be transition of CPNT1; :: thesis: 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} *' )
let t2 be transition of CPNT2; :: thesis: ( 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 implies ( *' {t1} c= *' {t2} & {t1} *' c= {t2} *' ) )
assume that
A1: the carrier of CPNT1 c= the carrier of CPNT2 and
A2: the S-T_Arcs of CPNT1 c= the S-T_Arcs of CPNT2 and
A3: the T-S_Arcs of CPNT1 c= the T-S_Arcs of CPNT2 and
A4: t1 = t2 ; :: thesis: ( *' {t1} c= *' {t2} & {t1} *' c= {t2} *' )
thus *' {t1} c= *' {t2} :: thesis: {t1} *' c= {t2} *'

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in *' {t1} or x in *' {t2} )
assume A5: x in *' {t1} ; :: thesis: x in *' {t2}
then A6: x is place of CPNT2 by A1;
ex s being place of CPNT1 st
( x = s & ex f being S-T_arc of CPNT1 ex w being transition of CPNT1 st
( w in {t1} & f = [s,w] ) ) by A5;
then consider f being S-T_arc of CPNT1, w being transition of CPNT1 such that
A7: w in {t2} and
A8: f = [x,w] by A4;
f is S-T_arc of CPNT2 by A2;
hence x in *' {t2} by A7, A8, A6; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {t1} *' or x in {t2} *' )
assume A9: x in {t1} *' ; :: thesis: x in {t2} *'
then A10: x is place of CPNT2 by A1;
ex s being place of CPNT1 st
( x = s & ex f being T-S_arc of CPNT1 ex w being transition of CPNT1 st
( w in {t1} & f = [w,s] ) ) by A9;
then consider f being T-S_arc of CPNT1, w being transition of CPNT1 such that
A11: w in {t2} and
A12: f = [w,x] by A4;
f is T-S_arc of CPNT2 by A3;
hence x in {t2} *' by A11, A12, A10; :: thesis: verum