let Al be QC-alphabet ; :: thesis: for X being Subset of (CQC-WFF Al)

for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X holds

not not (f . 1) `2 = 0 & ... & not (f . 1) `2 = 6

let X be Subset of (CQC-WFF Al); :: thesis: for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X holds

not not (f . 1) `2 = 0 & ... & not (f . 1) `2 = 6

let f be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:]; :: thesis: ( f is_a_proof_wrt X implies not not (f . 1) `2 = 0 & ... & not (f . 1) `2 = 6 )

assume A1: f is_a_proof_wrt X ; :: thesis: not not (f . 1) `2 = 0 & ... & not (f . 1) `2 = 6

then A2: 1 <= len f by Th21;

then A3: f,1 is_a_correct_step_wrt X by A1;

assume A4: (f . 1) `2 <> 0 & ... & (f . 1) `2 <> 6 ; :: thesis: contradiction

not not (f . 1) `2 = 0 & ... & not (f . 1) `2 = 9 by A2, Th19;

for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X holds

not not (f . 1) `2 = 0 & ... & not (f . 1) `2 = 6

let X be Subset of (CQC-WFF Al); :: thesis: for f being FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:] st f is_a_proof_wrt X holds

not not (f . 1) `2 = 0 & ... & not (f . 1) `2 = 6

let f be FinSequence of [:(CQC-WFF Al),Proof_Step_Kinds:]; :: thesis: ( f is_a_proof_wrt X implies not not (f . 1) `2 = 0 & ... & not (f . 1) `2 = 6 )

assume A1: f is_a_proof_wrt X ; :: thesis: not not (f . 1) `2 = 0 & ... & not (f . 1) `2 = 6

then A2: 1 <= len f by Th21;

then A3: f,1 is_a_correct_step_wrt X by A1;

assume A4: (f . 1) `2 <> 0 & ... & (f . 1) `2 <> 6 ; :: thesis: contradiction

not not (f . 1) `2 = 0 & ... & not (f . 1) `2 = 9 by A2, Th19;

per cases then
( (f . 1) `2 = 7 or (f . 1) `2 = 8 or (f . 1) `2 = 9 )
by A4;

end;

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

then
ex i, j being Nat ex p, q being Element of CQC-WFF Al st

( 1 <= i & i < 1 & 1 <= j & j < i & p = (f . j) `1 & q = (f . 1) `1 & (f . i) `1 = p => q ) by A3, Def4;

hence contradiction ; :: thesis: verum

end;( 1 <= i & i < 1 & 1 <= j & j < i & p = (f . j) `1 & q = (f . 1) `1 & (f . i) `1 = p => q ) by A3, Def4;

hence contradiction ; :: thesis: verum

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

then
ex i being Nat ex p, q being Element of CQC-WFF Al ex x being bound_QC-variable of Al st

( 1 <= i & i < 1 & (f . i) `1 = p => q & not x in still_not-bound_in p & (f . 1) `1 = p => (All (x,q)) ) by A3, Def4;

hence contradiction ; :: thesis: verum

end;( 1 <= i & i < 1 & (f . i) `1 = p => q & not x in still_not-bound_in p & (f . 1) `1 = p => (All (x,q)) ) by A3, Def4;

hence contradiction ; :: thesis: verum

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

then
ex i being Nat ex x, y being bound_QC-variable of Al ex s being QC-formula of Al st

( 1 <= i & i < 1 & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (f . i) `1 & (f . 1) `1 = s . y ) by A3, Def4;

hence contradiction ; :: thesis: verum

end;( 1 <= i & i < 1 & s . x in CQC-WFF Al & s . y in CQC-WFF Al & not x in still_not-bound_in s & s . x = (f . i) `1 & (f . 1) `1 = s . y ) by A3, Def4;

hence contradiction ; :: thesis: verum