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)

proof

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;

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) )
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;

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

then consider fs, fs1 being firing-sequence of N such that
A5: x = fs ^ fs1 and
A6: fs in R and
A7: fs1 in R1 ;
fs1 in R1 \/ R2 by A7, XBOOLE_0:def 3;
hence x in R before (R1 \/ R2) by A5, A6; :: thesis: verum

end;

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

then consider fs, fs2 being firing-sequence of N such that
A8: x = fs ^ fs2 and
A9: fs in R and
A10: fs2 in R2 ;
fs2 in R1 \/ R2 by A10, XBOOLE_0:def 3;
hence x in R before (R1 \/ R2) by A8, A9; :: thesis: verum

end;

end;