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

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