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 set ; :: 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 & fs in R & fs1 in R1 \/ R2 ) ;
( fs1 in R1 or fs1 in R2 ) by A1, 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;
hence x in (R before R1) \/ (R before R2) by XBOOLE_0:def 3; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (R before R1) \/ (R before R2) or x in R before (R1 \/ R2) )
assume A2: 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 A2, 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
A3: ( x = fs ^ fs1 & fs in R & fs1 in R1 ) ;
fs1 in R1 \/ R2 by A3, XBOOLE_0:def 3;
hence x in R before (R1 \/ R2) by A3; :: 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
A4: ( x = fs ^ fs2 & fs in R & fs2 in R2 ) ;
fs2 in R1 \/ R2 by A4, XBOOLE_0:def 3;
hence x in R before (R1 \/ R2) by A4; :: thesis: verum

end;

end;