let P be set ; :: thesis: for N being Petri_net of P
for e1, e2, e being Element of N holds {<*e1*>,<*e2*>} concur {<*e*>} = {<*e1,e*>,<*e2,e*>,<*e,e1*>,<*e,e2*>}
let N be Petri_net of P; :: thesis: for e1, e2, e being Element of N holds {<*e1*>,<*e2*>} concur {<*e*>} = {<*e1,e*>,<*e2,e*>,<*e,e1*>,<*e,e2*>}
let e1, e2, e be Element of N; :: thesis: {<*e1*>,<*e2*>} concur {<*e*>} = {<*e1,e*>,<*e2,e*>,<*e,e1*>,<*e,e2*>}
{<*e1*>,<*e2*>} = {<*e1*>} \/ {<*e2*>} by ENUMSET1:1;
then A1: {<*e1*>,<*e2*>} concur {<*e*>} = ({<*e1*>} concur {<*e*>}) \/ ({<*e2*>} concur {<*e*>}) by Th48;
A2: {<*e1*>} concur {<*e*>} = {<*e1,e*>,<*e,e1*>} by Th49;
{<*e2*>} concur {<*e*>} = {<*e2,e*>,<*e,e2*>} by Th49;
hence {<*e1*>,<*e2*>} concur {<*e*>} = {<*e1,e*>,<*e,e1*>,<*e2,e*>,<*e,e2*>} by A1, A2, ENUMSET1:5
.= {<*e1,e*>,<*e2,e*>,<*e,e1*>,<*e,e2*>} by ENUMSET1:62 ;
:: thesis: verum