let P be set ; :: thesis: for N being Petri_net of P
for R1, P1, R2, 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, P1, R2, P2 being process of N st R1 c= P1 & R2 c= P2 holds
R1 concur R2 c= P1 concur P2
let R1, P1, R2, 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 set ; :: 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