let P be set ; :: thesis: for N being Petri_net of P
for R1, R2, R being process of N holds (R1 \/ R2) concur R = (R1 concur R) \/ (R2 concur R)
let N be Petri_net of P; :: thesis: for R1, R2, R being process of N holds (R1 \/ R2) concur R = (R1 concur R) \/ (R2 concur R)
let R1, R2, R be process of N; :: thesis: (R1 \/ R2) concur R = (R1 concur R) \/ (R2 concur R)
thus (R1 \/ R2) concur R c= (R1 concur R) \/ (R2 concur R) :: according to XBOOLE_0:def 10 :: thesis: (R1 concur R) \/ (R2 concur R) c= (R1 \/ R2) concur R

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (R1 \/ R2) concur R or x in (R1 concur R) \/ (R2 concur R) )
assume x in (R1 \/ R2) concur R ; :: thesis: x in (R1 concur R) \/ (R2 concur R)
then consider C being firing-sequence of N such that
A1: ( x = C & ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 \/ R2 & Seq q2 in R ) ) ;
consider q1, q2 being FinSubsequence such that
A2: ( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 \/ R2 & Seq q2 in R ) by A1;
( Seq q1 in R1 or Seq q1 in R2 ) by A2, XBOOLE_0:def 3;
then ( x in { C1 where C1 is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C1 = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R ) } or x in { C2 where C2 is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C2 = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R ) } ) by A1, A2;
hence x in (R1 concur R) \/ (R2 concur R) by XBOOLE_0:def 3; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (R1 concur R) \/ (R2 concur R) or x in (R1 \/ R2) concur R )
assume A3: x in (R1 concur R) \/ (R2 concur R) ; :: thesis: x in (R1 \/ R2) concur R

per cases ( x in R1 concur R or x in R2 concur R ) by A3, XBOOLE_0:def 3;

suppose x in R1 concur R ; :: thesis: x in (R1 \/ R2) concur R

then consider C being firing-sequence of N such that
A4: ( x = C & ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R ) ) ;
consider q1, q2 being FinSubsequence such that
A5: ( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R ) by A4;
Seq q1 in R1 \/ R2 by A5, XBOOLE_0:def 3;
hence x in (R1 \/ R2) concur R by A4, A5; :: thesis: verum

end;

suppose x in R2 concur R ; :: thesis: x in (R1 \/ R2) concur R

then consider C being firing-sequence of N such that
A6: ( x = C & ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R ) ) ;
consider q1, q2 being FinSubsequence such that
A7: ( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R ) by A6;
Seq q1 in R1 \/ R2 by A7, XBOOLE_0:def 3;
hence x in (R1 \/ R2) concur R by A6, A7; :: thesis: verum

end;

end;