let P be set ; :: thesis: for N being Petri_net of P
for C1, C2 being firing-sequence of N holds {C1} before {C2} = {(C1 ^ C2)}
let N be Petri_net of P; :: thesis: for C1, C2 being firing-sequence of N holds {C1} before {C2} = {(C1 ^ C2)}
let C1, C2 be firing-sequence of N; :: thesis: {C1} before {C2} = {(C1 ^ C2)}
thus {C1} before {C2} c= {(C1 ^ C2)} :: according to XBOOLE_0:def 10 :: thesis: {(C1 ^ C2)} c= {C1} before {C2}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {C1} before {C2} or x in {(C1 ^ C2)} )
assume x in {C1} before {C2} ; :: thesis: x in {(C1 ^ C2)}
then consider fs1, fs2 being firing-sequence of N such that
A1: x = fs1 ^ fs2 and
A2: fs1 in {C1} and
A3: fs2 in {C2} ;
A4: fs1 = C1 by A2, TARSKI:def 1;
fs2 = C2 by A3, TARSKI:def 1;
hence x in {(C1 ^ C2)} by A1, A4, TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {(C1 ^ C2)} or x in {C1} before {C2} )
assume x in {(C1 ^ C2)} ; :: thesis: x in {C1} before {C2}
then A5: x = C1 ^ C2 by TARSKI:def 1;
A6: C1 in {C1} by TARSKI:def 1;
C2 in {C2} by TARSKI:def 1;
hence x in {C1} before {C2} by A5, A6; :: thesis: verum