let R, R1, R2 be process of N; :: thesis: ( R = { C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) } implies R = { C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R1 ) } )
assume A1: R = { C1 where C1 is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C1 = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) } ; :: thesis: R = { C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R1 ) }
thus R c= { C2 where C2 is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C2 = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R1 ) } :: according to XBOOLE_0:def 10 :: thesis: { C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R1 ) } c= R

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in R or x in { C2 where C2 is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C2 = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R1 ) } )
assume x in R ; :: thesis: x in { C2 where C2 is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C2 = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R1 ) }
then A2: ex C1 being firing-sequence of N st
( x = C1 & ex q1, q2 being FinSubsequence st
( C1 = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) ) by A1;
set X = { C2 where C2 is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C2 = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R1 ) } ;
thus x in { C2 where C2 is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C2 = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R1 ) } by A2; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R1 ) } or x in R )
assume x in { C2 where C2 is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C2 = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R1 ) } ; :: thesis: x in R
then ex C2 being firing-sequence of N st
( x = C2 & ex q1, q2 being FinSubsequence st
( C2 = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R1 ) ) ;
hence x in R by A1; :: thesis: verum