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 object ; :: 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 and
A2: C1 in R1 before R2 and
A3: C2 in R3 ;
consider fs1, fs2 being firing-sequence of N such that
A4: C1 = fs1 ^ fs2 and
A5: fs1 in R1 and
A6: fs2 in R2 by A2;
A7: x = fs1 ^ (fs2 ^ C2) by A1, A4, FINSEQ_1:32;
consider C3 being firing-sequence of N such that
A8: C3 = fs2 ^ C2 and
A9: fs2 in R2 and
A10: C2 in R3 by A3, A6;
C3 in R2 before R3 by A8, A9, A10;
hence x in R1 before (R2 before R3) by A5, A7, A8; :: thesis: verum

end;

let x be object ; :: 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
A11: x = C1 ^ C2 and
A12: C1 in R1 and
A13: C2 in R2 before R3 ;
consider fs1, fs2 being firing-sequence of N such that
A14: C2 = fs1 ^ fs2 and
A15: fs1 in R2 and
A16: fs2 in R3 by A13;
A17: x = (C1 ^ fs1) ^ fs2 by A11, A14, FINSEQ_1:32;
consider C being firing-sequence of N such that
A18: C = C1 ^ fs1 and
A19: C1 in R1 and
A20: fs1 in R2 by A12, A15;
C in R1 before R2 by A18, A19, A20;
hence x in (R1 before R2) before R3 by A16, A17, A18; :: thesis: verum