let P be set ; :: thesis: for N being Petri_net of P
for R1, R2, R3 being process of N holds (R1 before R2) before R3 = R1 before (R2 before R3)
let N be Petri_net of P; :: thesis: for R1, R2, R3 being process of N holds (R1 before R2) before R3 = R1 before (R2 before R3)
let R1, R2, R3 be process of N; :: thesis: (R1 before R2) before R3 = R1 before (R2 before R3)
thus (R1 before R2) before R3 c= R1 before (R2 before R3) :: according to XBOOLE_0:def 10 :: thesis: R1 before (R2 before R3) c= (R1 before R2) before R3

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (R1 before R2) before R3 or x in R1 before (R2 before R3) )
assume x in (R1 before R2) before R3 ; :: thesis: x in R1 before (R2 before R3)
then consider C1, C2 being firing-sequence of N such that
A1: ( x = C1 ^ C2 & C1 in R1 before R2 & C2 in R3 ) ;
consider fs1, fs2 being firing-sequence of N such that
A2: ( C1 = fs1 ^ fs2 & fs1 in R1 & fs2 in R2 ) by A1;
A3: x = fs1 ^ (fs2 ^ C2) by A1, A2, FINSEQ_1:45;
consider C3 being firing-sequence of N such that
A4: ( C3 = fs2 ^ C2 & fs2 in R2 & C2 in R3 ) by A1, A2;
C3 in R2 before R3 by A4;
hence x in R1 before (R2 before R3) by A2, A3, A4; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in R1 before (R2 before R3) or x in (R1 before R2) before R3 )
assume x in R1 before (R2 before R3) ; :: thesis: x in (R1 before R2) before R3
then consider C1, C2 being firing-sequence of N such that
A5: ( x = C1 ^ C2 & C1 in R1 & C2 in R2 before R3 ) ;
consider fs1, fs2 being firing-sequence of N such that
A6: ( C2 = fs1 ^ fs2 & fs1 in R2 & fs2 in R3 ) by A5;
A7: x = (C1 ^ fs1) ^ fs2 by A5, A6, FINSEQ_1:45;
consider C being firing-sequence of N such that
A8: ( C = C1 ^ fs1 & C1 in R1 & fs1 in R2 ) by A5, A6;
C in R1 before R2 by A8;
hence x in (R1 before R2) before R3 by A6, A7, A8; :: thesis: verum