let P be set ; :: thesis: for N being Petri_net of P
for R being process of N holds R before (NeutralProcess N) = R
let N be Petri_net of P; :: thesis: for R being process of N holds R before (NeutralProcess N) = R
let R be process of N; :: thesis: R before (NeutralProcess N) = R
thus R before (NeutralProcess N) c= R :: according to XBOOLE_0:def 10 :: thesis: R c= R before (NeutralProcess N)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in R before (NeutralProcess N) or x in R )
assume x in R before (NeutralProcess N) ; :: thesis: x in R
then consider C1, C being firing-sequence of N such that
A1: x = C1 ^ C and
A2: C1 in R and
A3: C in NeutralProcess N ;
C = <*> N by A3, TARSKI:def 1;
hence x in R by A1, A2, FINSEQ_1:34; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in R or x in R before (NeutralProcess N) )
assume A4: x in R ; :: thesis: x in R before (NeutralProcess N)
then reconsider C = x as Element of N * ;
A5: <*> N in NeutralProcess N by TARSKI:def 1;
x = C ^ (<*> N) by FINSEQ_1:34;
hence x in R before (NeutralProcess N) by A4, A5; :: thesis: verum