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 )
then A2: ( 1 <= 1 & 1 <= len f ) by Th58;
then A3: f,1 is_a_correct_step_wrt X by A1, 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 (f . 1) `2 = 7 ; :: thesis: contradiction

then 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, Def4;
hence contradiction ; :: thesis: verum

end;

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

then 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, Def4;
hence contradiction ; :: thesis: verum

end;

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

then 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, Def4;
hence contradiction ; :: thesis: verum

end;

end;