let X be Subset of CQC-WFF ; :: thesis: for f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] holds
( not f is_a_proof_wrt X or (f . 1) `2 = 0 or (f . 1) `2 = 1 or (f . 1) `2 = 2 or (f . 1) `2 = 3 or (f . 1) `2 = 4 or (f . 1) `2 = 5 or (f . 1) `2 = 6 )
let f be FinSequence of [:CQC-WFF ,Proof_Step_Kinds :]; :: thesis: ( not f is_a_proof_wrt X or (f . 1) `2 = 0 or (f . 1) `2 = 1 or (f . 1) `2 = 2 or (f . 1) `2 = 3 or (f . 1) `2 = 4 or (f . 1) `2 = 5 or (f . 1) `2 = 6 )
assume A1: f is_a_proof_wrt X ; :: thesis: ( (f . 1) `2 = 0 or (f . 1) `2 = 1 or (f . 1) `2 = 2 or (f . 1) `2 = 3 or (f . 1) `2 = 4 or (f . 1) `2 = 5 or (f . 1) `2 = 6 )
A2: 1 <= len f by A1, Th58;
A3: f,1 is_a_correct_step_wrt X by A1, A2, Def5;
assume A4: ( not (f . 1) `2 = 0 & not (f . 1) `2 = 1 & not (f . 1) `2 = 2 & not (f . 1) `2 = 3 & not (f . 1) `2 = 4 & not (f . 1) `2 = 5 & not (f . 1) `2 = 6 ) ; :: thesis: contradiction

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

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

A6: ex i, j being Element of NAT ex p, q being Element of CQC-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, A5, Def4;
thus contradiction by A6; :: thesis: verum

end;

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

A8: ex i being Element of NAT ex p, q being Element of CQC-WFF ex x being bound_QC-variable 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, A7, Def4;
thus contradiction by A8; :: thesis: verum

end;

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

A10: ex i being Element of NAT ex x, y being bound_QC-variable ex s being QC-formula st
( 1 <= i & i < 1 & s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x = (f . i) `1 & (f . 1) `1 = s . y ) by A3, A9, Def4;
thus contradiction by A10; :: thesis: verum

end;

end;