let P be set ; :: thesis: for N being Petri_net of P
for e, e1, e2 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 e, e1, e2 being Element of N holds {<*e1*>,<*e2*>} concur {<*e*>} = {<*e1,e*>,<*e2,e*>,<*e,e1*>,<*e,e2*>}
let e, e1, e2 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 Th34;
A2: {<*e1*>} concur {<*e*>} = {<*e1,e*>,<*e,e1*>} by Th35;
{<*e2*>} concur {<*e*>} = {<*e2,e*>,<*e,e2*>} by Th35;
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