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

assume A4: x in R ; :: thesis: x in (NeutralProcess N) before R

then reconsider C = x as Element of N * ;

A5: <*> N in NeutralProcess N by TARSKI:def 1;

x = (<*> N) ^ C by FINSEQ_1:34;

hence x in (NeutralProcess N) before R by A4, A5; :: thesis: verum

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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in R or x in (NeutralProcess N) before R )
let x be object ; :: 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 and

A2: C1 in NeutralProcess N and

A3: C in R ;

C1 = <*> N by A2, TARSKI:def 1;

hence x in R by A1, A3, FINSEQ_1:34; :: thesis: verum

end;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 and

A2: C1 in NeutralProcess N and

A3: C in R ;

C1 = <*> N by A2, TARSKI:def 1;

hence x in R by A1, A3, FINSEQ_1:34; :: thesis: verum

assume A4: x in R ; :: thesis: x in (NeutralProcess N) before R

then reconsider C = x as Element of N * ;

A5: <*> N in NeutralProcess N by TARSKI:def 1;

x = (<*> N) ^ C by FINSEQ_1:34;

hence x in (NeutralProcess N) before R by A4, A5; :: thesis: verum