let P be set ; :: thesis: for N being Petri_net of P
for e1, e2 being Element of N holds {<*e1*>} concur {<*e2*>} = {<*e1,e2*>,<*e2,e1*>}

let N be Petri_net of P; :: thesis: for e1, e2 being Element of N holds {<*e1*>} concur {<*e2*>} = {<*e1,e2*>,<*e2,e1*>}
let e1, e2 be Element of N; :: thesis: {<*e1*>} concur {<*e2*>} = {<*e1,e2*>,<*e2,e1*>}
set C1 = <*e1*>;
set C2 = <*e2*>;
set R1 = {<*e1*>};
set R2 = {<*e2*>};
thus {<*e1*>} concur {<*e2*>} c= {<*e1,e2*>,<*e2,e1*>} :: according to XBOOLE_0:def 10 :: thesis: {<*e1,e2*>,<*e2,e1*>} c= {<*e1*>} concur {<*e2*>}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {<*e1*>} concur {<*e2*>} or x in {<*e1,e2*>,<*e2,e1*>} )
assume x in {<*e1*>} concur {<*e2*>} ; :: thesis: x in {<*e1,e2*>,<*e2,e1*>}
then consider C being firing-sequence of N such that
A1: x = C and
A2: ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in {<*e1*>} & Seq q2 in {<*e2*>} ) ;
consider q1, q2 being FinSubsequence such that
A3: C = q1 \/ q2 and
A4: q1 misses q2 and
A5: Seq q1 in {<*e1*>} and
A6: Seq q2 in {<*e2*>} by A2;
A7: Seq q1 = <*e1*> by ;
A8: Seq q2 = <*e2*> by ;
consider i being Element of NAT such that
A9: q1 = {[i,e1]} by ;
consider j being Element of NAT such that
A10: q2 = {[j,e2]} by ;
A11: [i,e1] in q1 by ;
A12: [j,e2] in q2 by ;
A13: C = {[i,e1],[j,e2]} by ;
then ( ( i = 1 & j = 1 & e1 = e2 ) or ( i = 1 & j = 2 ) or ( i = 2 & j = 1 ) ) by FINSEQ_1:98;
then ( C = <*e1,e2*> or C = <*e2,e1*> ) by ;
hence x in {<*e1,e2*>,<*e2,e1*>} by ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {<*e1,e2*>,<*e2,e1*>} or x in {<*e1*>} concur {<*e2*>} )
assume A14: x in {<*e1,e2*>,<*e2,e1*>} ; :: thesis: x in {<*e1*>} concur {<*e2*>}
per cases ( x = <*e1,e2*> or x = <*e2,e1*> ) by ;
end;