set X = { 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 ) } ;

{ 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 ) } c= N *

( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) } is process of N ; :: thesis: verum

( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) } ;

{ 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 ) } c= N *

proof

hence
{ 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 { 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 ) } or x in N * )

assume 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 R1 & Seq q2 in R2 ) } ; :: thesis: x in N *

then ex C being firing-sequence of N st

( x = C & ex q1, q2 being FinSubsequence st

( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) ) ;

hence x in N * ; :: thesis: verum

end;( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) } or x in N * )

assume 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 R1 & Seq q2 in R2 ) } ; :: thesis: x in N *

then ex C being firing-sequence of N st

( x = C & ex q1, q2 being FinSubsequence st

( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) ) ;

hence x in N * ; :: thesis: verum

( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) } is process of N ; :: thesis: verum