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 set ; :: 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 & 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
A2: ( C = q1 \/ q2 & q1 misses q2 & Seq q1 in {<*e1*>} & Seq q2 in {<*e2*>} ) by A1;
A3: ( Seq q1 = <*e1*> & Seq q2 = <*e2*> ) by A2, TARSKI:def 1;
then consider i being Element of NAT such that
A4: q1 = {[i,e1]} by Th4;
consider j being Element of NAT such that
A5: q2 = {[j,e2]} by A3, Th4;
A6: ( [i,e1] in q1 & [j,e2] in q2 ) by A4, A5, TARSKI:def 1;
A7: C = {[i,e1],[j,e2]} by A2, A4, A5, ENUMSET1:41;
then ( ( i = 1 & j = 1 & e1 = e2 ) or ( i = 1 & j = 2 ) or ( i = 2 & j = 1 ) ) by Th5;
then ( C = <*e1,e2*> or C = <*e2,e1*> ) by A2, A6, A7, Th6, XBOOLE_0:3;
hence x in {<*e1,e2*>,<*e2,e1*>} by A1, TARSKI:def 2; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {<*e1,e2*>,<*e2,e1*>} or x in {<*e1*>} concur {<*e2*>} )
assume A8: x in {<*e1,e2*>,<*e2,e1*>} ; :: thesis: x in {<*e1*>} concur {<*e2*>}

per cases ( x = <*e1,e2*> or x = <*e2,e1*> ) by A8, TARSKI:def 2;

suppose A9: x = <*e1,e2*> ; :: thesis: x in {<*e1*>} concur {<*e2*>}

then A10: x = {[1,e1],[2,e2]} by Th6
.= {[1,e1]} \/ {[2,e2]} by ENUMSET1:41 ;
reconsider q1 = {[1,e1]}, q2 = {[2,e2]} as FinSubsequence by Th1;
[1,e1] <> [2,e2] by ZFMISC_1:33;
then not [1,e1] in q2 by TARSKI:def 1;
then A11: q1 misses q2 by ZFMISC_1:56;
A12: ( Seq q1 = <*e1*> & Seq q2 = <*e2*> ) by Th3;
( <*e1*> in {<*e1*>} & <*e2*> in {<*e2*>} ) by TARSKI:def 1;
hence x in {<*e1*>} concur {<*e2*>} by A9, A10, A11, A12; :: thesis: verum

end;

suppose A13: x = <*e2,e1*> ; :: thesis: x in {<*e1*>} concur {<*e2*>}

then A14: x = {[1,e2],[2,e1]} by Th6
.= {[1,e2]} \/ {[2,e1]} by ENUMSET1:41 ;
reconsider q1 = {[2,e1]}, q2 = {[1,e2]} as FinSubsequence by Th1;
[1,e2] <> [2,e1] by ZFMISC_1:33;
then not [2,e1] in q2 by TARSKI:def 1;
then A15: q1 misses q2 by ZFMISC_1:56;
A16: ( Seq q1 = <*e1*> & Seq q2 = <*e2*> ) by Th3;
( <*e1*> in {<*e1*>} & <*e2*> in {<*e2*>} ) by TARSKI:def 1;
hence x in {<*e1*>} concur {<*e2*>} by A13, A14, A15, A16; :: thesis: verum

end;

end;