let P be set ; :: thesis: for N being Petri_net of P
for R1, P1, R2, P2 being process of N st R1 c= P1 & R2 c= P2 holds
R1 before R2 c= P1 before P2
let N be Petri_net of P; :: thesis: for R1, P1, R2, P2 being process of N st R1 c= P1 & R2 c= P2 holds
R1 before R2 c= P1 before P2
let R1, P1, R2, P2 be process of N; :: thesis: ( R1 c= P1 & R2 c= P2 implies R1 before R2 c= P1 before P2 )
assume A1: ( R1 c= P1 & R2 c= P2 ) ; :: thesis: R1 before R2 c= P1 before P2
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in R1 before R2 or x in P1 before P2 )
assume x in R1 before R2 ; :: thesis: x in P1 before P2
then consider C1, C2 being firing-sequence of N such that
A2: ( x = C1 ^ C2 & C1 in R1 & C2 in R2 ) ;
thus x in P1 before P2 by A1, A2; :: thesis: verum