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 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 A5, TARSKI:def 1;
A8: Seq q2 = <*e2*> by A6, TARSKI:def 1;
consider i being Element of NAT such that
A9: q1 = {[i,e1]} by A7, Th4;
consider j being Element of NAT such that
A10: q2 = {[j,e2]} by A8, Th4;
A11: [i,e1] in q1 by A9, TARSKI:def 1;
A12: [j,e2] in q2 by A10, TARSKI:def 1;
A13: C = {[i,e1],[j,e2]} by A3, A9, A10, ENUMSET1:1;
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 A4, A11, A12, A13, 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 A14: x in {<*e1,e2*>,<*e2,e1*>} ; :: thesis: x in {<*e1*>} concur {<*e2*>}

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

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

then A16: x = {[1,e1],[2,e2]} by Th6
.= {[1,e1]} \/ {[2,e2]} by ENUMSET1:1 ;
reconsider q1 = {[1,e1]}, q2 = {[2,e2]} as FinSubsequence by Th1;
[1,e1] <> [2,e2] by ZFMISC_1:27;
then not [1,e1] in q2 by TARSKI:def 1;
then A17: q1 misses q2 by ZFMISC_1:50;
A18: Seq q1 = <*e1*> by Th3;
A19: Seq q2 = <*e2*> by Th3;
A20: <*e1*> in {<*e1*>} by TARSKI:def 1;
<*e2*> in {<*e2*>} by TARSKI:def 1;
hence x in {<*e1*>} concur {<*e2*>} by A15, A16, A17, A18, A19, A20; :: thesis: verum

end;

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

then A22: x = {[1,e2],[2,e1]} by Th6
.= {[1,e2]} \/ {[2,e1]} by ENUMSET1:1 ;
reconsider q1 = {[2,e1]}, q2 = {[1,e2]} as FinSubsequence by Th1;
[1,e2] <> [2,e1] by ZFMISC_1:27;
then not [2,e1] in q2 by TARSKI:def 1;
then A23: q1 misses q2 by ZFMISC_1:50;
A24: Seq q1 = <*e1*> by Th3;
A25: Seq q2 = <*e2*> by Th3;
A26: <*e1*> in {<*e1*>} by TARSKI:def 1;
<*e2*> in {<*e2*>} by TARSKI:def 1;
hence x in {<*e1*>} concur {<*e2*>} by A21, A22, A23, A24, A25, A26; :: thesis: verum

end;

end;