set X = { (C1 ^ C2) where C1, C2 is firing-sequence of N : ( C1 in R1 & C2 in R2 ) } ;
{ (C1 ^ C2) where C1, C2 is firing-sequence of N : ( C1 in R1 & C2 in R2 ) } c= N *

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (C1 ^ C2) where C1, C2 is firing-sequence of N : ( C1 in R1 & C2 in R2 ) } or x in N * )
assume x in { (C1 ^ C2) where C1, C2 is firing-sequence of N : ( C1 in R1 & C2 in R2 ) } ; :: thesis: x in N *
then ex C1, C2 being firing-sequence of N st
( x = C1 ^ C2 & C1 in R1 & C2 in R2 ) ;
hence x in N * ; :: thesis: verum

end;

hence { (C1 ^ C2) where C1, C2 is firing-sequence of N : ( C1 in R1 & C2 in R2 ) } is process of N ; :: thesis: verum