theorem Th31: :: CALCUL_1:31

for Al being QC-alphabet
for PR being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:]
for n being Nat st 1 <= n & n <= len PR holds
not not (PR . n) `2 = 0 & ... & not (PR . n) `2 = 9