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*>}

assume A14: x in {<*e1,e2*>,<*e2,e1*>} ; :: thesis: x in {<*e1*>} concur {<*e2*>}

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,e2*>,<*e2,e1*>} or x in {<*e1*>} concur {<*e2*>} )
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 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, FINSEQ_3:159;

consider j being Element of NAT such that

A10: q2 = {[j,e2]} by A8, FINSEQ_3:159;

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 FINSEQ_1:98;

then ( C = <*e1,e2*> or C = <*e2,e1*> ) by A4, A11, A12, A13, FINSEQ_1:99, XBOOLE_0:3;

hence x in {<*e1,e2*>,<*e2,e1*>} by A1, TARSKI:def 2; :: thesis: verum

end;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, FINSEQ_3:159;

consider j being Element of NAT such that

A10: q2 = {[j,e2]} by A8, FINSEQ_3:159;

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 FINSEQ_1:98;

then ( C = <*e1,e2*> or C = <*e2,e1*> ) by A4, A11, A12, A13, FINSEQ_1:99, XBOOLE_0:3;

hence x in {<*e1,e2*>,<*e2,e1*>} by A1, TARSKI:def 2; :: thesis: verum

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;

end;

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

then A16: x =
{[1,e1],[2,e2]}
by FINSEQ_1:99

.= {[1,e1]} \/ {[2,e2]} by ENUMSET1:1 ;

reconsider q1 = {[1,e1]}, q2 = {[2,e2]} as FinSubsequence by FINSEQ_1:96;

[1,e1] <> [2,e2] by XTUPLE_0:1;

then not [1,e1] in q2 by TARSKI:def 1;

then A17: q1 misses q2 by ZFMISC_1:50;

A18: Seq q1 = <*e1*> by FINSEQ_3:157;

A19: Seq q2 = <*e2*> by FINSEQ_3:157;

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;.= {[1,e1]} \/ {[2,e2]} by ENUMSET1:1 ;

reconsider q1 = {[1,e1]}, q2 = {[2,e2]} as FinSubsequence by FINSEQ_1:96;

[1,e1] <> [2,e2] by XTUPLE_0:1;

then not [1,e1] in q2 by TARSKI:def 1;

then A17: q1 misses q2 by ZFMISC_1:50;

A18: Seq q1 = <*e1*> by FINSEQ_3:157;

A19: Seq q2 = <*e2*> by FINSEQ_3:157;

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

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

then A22: x =
{[1,e2],[2,e1]}
by FINSEQ_1:99

.= {[1,e2]} \/ {[2,e1]} by ENUMSET1:1 ;

reconsider q1 = {[2,e1]}, q2 = {[1,e2]} as FinSubsequence by FINSEQ_1:96;

[1,e2] <> [2,e1] by XTUPLE_0:1;

then not [2,e1] in q2 by TARSKI:def 1;

then A23: q1 misses q2 by ZFMISC_1:50;

A24: Seq q1 = <*e1*> by FINSEQ_3:157;

A25: Seq q2 = <*e2*> by FINSEQ_3:157;

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;.= {[1,e2]} \/ {[2,e1]} by ENUMSET1:1 ;

reconsider q1 = {[2,e1]}, q2 = {[1,e2]} as FinSubsequence by FINSEQ_1:96;

[1,e2] <> [2,e1] by XTUPLE_0:1;

then not [2,e1] in q2 by TARSKI:def 1;

then A23: q1 misses q2 by ZFMISC_1:50;

A24: Seq q1 = <*e1*> by FINSEQ_3:157;

A25: Seq q2 = <*e2*> by FINSEQ_3:157;

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