let CPNT1, CPNT2 be Colored_PT_net_Str ; :: thesis: for t1 being transition of CPNT1
for t2 being transition of CPNT2 st the Places of CPNT1 c= the Places of CPNT2 & the Transitions of CPNT1 c= the Transitions 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 Places of CPNT1 c= the Places of CPNT2 & the Transitions of CPNT1 c= the Transitions 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 Places of CPNT1 c= the Places of CPNT2 & the Transitions of CPNT1 c= the Transitions 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 AS1: ( the Places of CPNT1 c= the Places of CPNT2 & the Transitions of CPNT1 c= the Transitions 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 ) ; :: thesis: ( *' {t1} c= *' {t2} & {t1} *' c= {t2} *' )
thus *' {t1} c= *' {t2} :: thesis: {t1} *' c= {t2} *'

proof

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

end;

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