let P be set ; :: thesis: for N being Petri_net of P
for C1, C2, C being firing-sequence of N holds {C1,C2} before {C} = {(C1 ^ C),(C2 ^ C)}
let N be Petri_net of P; :: thesis: for C1, C2, C being firing-sequence of N holds {C1,C2} before {C} = {(C1 ^ C),(C2 ^ C)}
let C1, C2, C 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 Th43
.= {(C1 ^ C)} \/ ({C2} before {C}) by Th45
.= {(C1 ^ C)} \/ {(C2 ^ C)} by Th45
.= {(C1 ^ C),(C2 ^ C)} by ENUMSET1:1 ; :: thesis: verum