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

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