theorem Th3: :: INTPRO_2:2

for f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:]
for n being Nat st 1 <= n & n <= len f holds
not not (f . n) `2 = 0 & ... & not (f . n) `2 = 10