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

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

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

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

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

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

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

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

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

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

proof

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

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

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

A1: x = fs ^ fs1 and

A2: fs in R and

A3: fs1 in R1 \/ R2 ;

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

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

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

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

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

A1: x = fs ^ fs1 and

A2: fs in R and

A3: fs1 in R1 \/ R2 ;

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

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

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

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

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

end;