theorem Th19: :: CQC_THE1:23

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