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