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 object ; :: 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;
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 object ; :: 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