let P be set ; :: thesis: for N being Petri_net of P

for R1, R2, P1, P2 being process of N st R1 c= P1 & R2 c= P2 holds

R1 concur R2 c= P1 concur P2

let N be Petri_net of P; :: thesis: for R1, R2, P1, P2 being process of N st R1 c= P1 & R2 c= P2 holds

R1 concur R2 c= P1 concur P2

let R1, R2, P1, P2 be process of N; :: thesis: ( R1 c= P1 & R2 c= P2 implies R1 concur R2 c= P1 concur P2 )

assume that

A1: R1 c= P1 and

A2: R2 c= P2 ; :: thesis: R1 concur R2 c= P1 concur P2

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in R1 concur R2 or x in P1 concur P2 )

assume x in R1 concur R2 ; :: thesis: x in P1 concur P2

then ex C being firing-sequence of N st

( x = C & ex q1, q2 being FinSubsequence st

( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) ) ;

hence x in P1 concur P2 by A1, A2; :: thesis: verum

for R1, R2, P1, P2 being process of N st R1 c= P1 & R2 c= P2 holds

R1 concur R2 c= P1 concur P2

let N be Petri_net of P; :: thesis: for R1, R2, P1, P2 being process of N st R1 c= P1 & R2 c= P2 holds

R1 concur R2 c= P1 concur P2

let R1, R2, P1, P2 be process of N; :: thesis: ( R1 c= P1 & R2 c= P2 implies R1 concur R2 c= P1 concur P2 )

assume that

A1: R1 c= P1 and

A2: R2 c= P2 ; :: thesis: R1 concur R2 c= P1 concur P2

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in R1 concur R2 or x in P1 concur P2 )

assume x in R1 concur R2 ; :: thesis: x in P1 concur P2

then ex C being firing-sequence of N st

( x = C & ex q1, q2 being FinSubsequence st

( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) ) ;

hence x in P1 concur P2 by A1, A2; :: thesis: verum