let P be set ; :: thesis: for N being Petri_net of P
for C, C1, C2 being firing-sequence of N holds {C} before {C1,C2} = {(C ^ C1),(C ^ C2)}
let N be Petri_net of P; :: thesis: for C, C1, C2 being firing-sequence of N holds {C} before {C1,C2} = {(C ^ C1),(C ^ C2)}
let C, C1, C2 be firing-sequence of N; :: thesis: {C} before {C1,C2} = {(C ^ C1),(C ^ C2)}
thus {C} before {C1,C2} = {C} before ({C1} \/ {C2}) by ENUMSET1:1
.= ({C} before {C1}) \/ ({C} before {C2}) by Th30
.= {(C ^ C1)} \/ ({C} before {C2}) by Th31
.= {(C ^ C1)} \/ {(C ^ C2)} by Th31
.= {(C ^ C1),(C ^ C2)} by ENUMSET1:1 ; :: thesis: verum