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

for R, R1, R2 being process of N holds (R1 \/ R2) before R = (R1 before R) \/ (R2 before R)

let N be Petri_net of P; :: thesis: for R, R1, R2 being process of N holds (R1 \/ R2) before R = (R1 before R) \/ (R2 before R)

let R, R1, R2 be process of N; :: thesis: (R1 \/ R2) before R = (R1 before R) \/ (R2 before R)

thus (R1 \/ R2) before R c= (R1 before R) \/ (R2 before R) :: according to XBOOLE_0:def 10 :: thesis: (R1 before R) \/ (R2 before R) c= (R1 \/ R2) before R

assume A4: x in (R1 before R) \/ (R2 before R) ; :: thesis: x in (R1 \/ R2) before R

for R, R1, R2 being process of N holds (R1 \/ R2) before R = (R1 before R) \/ (R2 before R)

let N be Petri_net of P; :: thesis: for R, R1, R2 being process of N holds (R1 \/ R2) before R = (R1 before R) \/ (R2 before R)

let R, R1, R2 be process of N; :: thesis: (R1 \/ R2) before R = (R1 before R) \/ (R2 before R)

thus (R1 \/ R2) before R c= (R1 before R) \/ (R2 before R) :: according to XBOOLE_0:def 10 :: thesis: (R1 before R) \/ (R2 before R) c= (R1 \/ R2) before R

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (R1 before R) \/ (R2 before R) or x in (R1 \/ R2) before R )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (R1 \/ R2) before R or x in (R1 before R) \/ (R2 before R) )

assume x in (R1 \/ R2) before R ; :: thesis: x in (R1 before R) \/ (R2 before R)

then consider fs1, fs being firing-sequence of N such that

A1: x = fs1 ^ fs and

A2: fs1 in R1 \/ R2 and

A3: fs in R ;

( fs1 in R1 or fs1 in R2 ) by A2, XBOOLE_0:def 3;

then ( x in { (a1 ^ a) where a1, a is firing-sequence of N : ( a1 in R1 & a in R ) } or x in { (b2 ^ b) where b2, b is firing-sequence of N : ( b2 in R2 & b in R ) } ) by A1, A3;

hence x in (R1 before R) \/ (R2 before R) by XBOOLE_0:def 3; :: thesis: verum

end;assume x in (R1 \/ R2) before R ; :: thesis: x in (R1 before R) \/ (R2 before R)

then consider fs1, fs being firing-sequence of N such that

A1: x = fs1 ^ fs and

A2: fs1 in R1 \/ R2 and

A3: fs in R ;

( fs1 in R1 or fs1 in R2 ) by A2, XBOOLE_0:def 3;

then ( x in { (a1 ^ a) where a1, a is firing-sequence of N : ( a1 in R1 & a in R ) } or x in { (b2 ^ b) where b2, b is firing-sequence of N : ( b2 in R2 & b in R ) } ) by A1, A3;

hence x in (R1 before R) \/ (R2 before R) by XBOOLE_0:def 3; :: thesis: verum

assume A4: x in (R1 before R) \/ (R2 before R) ; :: thesis: x in (R1 \/ R2) before R

per cases
( x in R1 before R or x in R2 before R )
by A4, XBOOLE_0:def 3;

end;