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

proof

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

end;

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