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 set ; :: 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 & fs1 in {C1} & fs2 in {C2} ) ;
( fs1 = C1 & fs2 = C2 ) by A1, TARSKI:def 1;
hence x in {(C1 ^ C2)} by A1, TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: 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 ( x = C1 ^ C2 & C1 in {C1} & C2 in {C2} ) by TARSKI:def 1;
hence x in {C1} before {C2} ; :: thesis: verum