let X be Subset of MC-wff; :: thesis: for f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] st f is_a_proof_wrt_IPC X holds
not not (f . 1) `2 = 0 & ... & not (f . 1) `2 = 10
let f be FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:]; :: thesis: ( f is_a_proof_wrt_IPC X implies not not (f . 1) `2 = 0 & ... & not (f . 1) `2 = 10 )
assume A1: f is_a_proof_wrt_IPC X ; :: thesis: not not (f . 1) `2 = 0 & ... & not (f . 1) `2 = 10
then A2: 1 <= len f by Th5;
then A3: f,1 is_a_correct_step_wrt_IPC X by A1;
assume (f . 1) `2 <> 0 & ... & (f . 1) `2 <> 10 ; :: thesis: contradiction

per cases then (f . 1) `2 = 10 by A2, Th3;

suppose (f . 1) `2 = 10 ; :: thesis: contradiction

then ex i, j being Nat ex p, q being Element of MC-wff st
( 1 <= i & i < 1 & 1 <= j & j < i & p = (f . j) `1 & q = (f . 1) `1 & (f . i) `1 = p => q ) by A3, Def3;
hence contradiction ; :: thesis: verum

end;

end;