let P be set ; :: thesis: for N being Petri_net of P

for R1, R2, P1, 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, R2, P1, P2 being process of N st R1 c= P1 & R2 c= P2 holds

R1 before R2 c= P1 before P2

let R1, R2, P1, P2 be process of N; :: thesis: ( R1 c= P1 & R2 c= P2 implies R1 before R2 c= P1 before P2 )

assume that

A1: R1 c= P1 and

A2: R2 c= P2 ; :: thesis: R1 before R2 c= P1 before P2

let x be object ; :: 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 ex C1, C2 being firing-sequence of N st

( x = C1 ^ C2 & C1 in R1 & C2 in R2 ) ;

hence x in P1 before P2 by A1, A2; :: thesis: verum

for R1, R2, P1, 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, R2, P1, P2 being process of N st R1 c= P1 & R2 c= P2 holds

R1 before R2 c= P1 before P2

let R1, R2, P1, P2 be process of N; :: thesis: ( R1 c= P1 & R2 c= P2 implies R1 before R2 c= P1 before P2 )

assume that

A1: R1 c= P1 and

A2: R2 c= P2 ; :: thesis: R1 before R2 c= P1 before P2

let x be object ; :: 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 ex C1, C2 being firing-sequence of N st

( x = C1 ^ C2 & C1 in R1 & C2 in R2 ) ;

hence x in P1 before P2 by A1, A2; :: thesis: verum