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 *

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

proof

hence
{ (C1 ^ C2) where C1, C2 is firing-sequence of N : ( C1 in R1 & C2 in R2 ) } is process of N
; :: thesis: verum
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;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