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

( 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

( 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 { C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st
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;( 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

( 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