let P be set ; :: thesis: for N being Petri_net of P
for R being process of N holds (NeutralProcess N) concur R = R
let N be Petri_net of P; :: thesis: for R being process of N holds (NeutralProcess N) concur R = R
let R be process of N; :: thesis: (NeutralProcess N) concur R = R
thus (NeutralProcess N) concur R c= R :: according to XBOOLE_0:def 10 :: thesis: R c= (NeutralProcess N) concur R
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (NeutralProcess N) concur R or x in R )
assume x in (NeutralProcess N) concur R ; :: thesis: x in R
then consider C being firing-sequence of N such that
A1: x = C and
A2: ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in {(<*> N)} & Seq q2 in R ) ;
consider q1, q2 being FinSubsequence such that
A3: C = q1 \/ q2 and
q1 misses q2 and
A4: Seq q1 in {(<*> N)} and
A5: Seq q2 in R by A2;
Seq q1 = {} by A4, TARSKI:def 1;
then q1 = {} by FINSEQ_1:97;
hence x in R by A1, A3, A5, FINSEQ_3:116; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in R or x in (NeutralProcess N) concur R )
assume A6: x in R ; :: thesis: x in (NeutralProcess N) concur R
then reconsider C = x as firing-sequence of N ;
reconsider q1 = <*> N, q2 = C as FinSubsequence ;
A7: Seq q2 = C by FINSEQ_3:116;
A8: {} \/ q2 = C ;
A9: Seq q1 = q1 by FINSEQ_3:116;
A10: q1 in {(<*> N)} by TARSKI:def 1;
q1 misses q2 ;
hence x in (NeutralProcess N) concur R by A6, A7, A8, A9, A10; :: thesis: verum