let Al be QC-alphabet ; :: thesis:
let p be Element of CQC-WFF Al; :: thesis:
let X be Subset of (CQC-WFF Al); :: thesis:
assume p is_formal_provable_from X ; :: thesis:
then consider f being FinSequence of CQC-WFF Al such that
A1: rng (Ant f) c= X and
A2: Suc f = p and
A3: |- f ;
consider PR being FinSequence of [:(set_of_CQC-WFF-seq Al),Proof_Step_Kinds:] such that
A4: PR is a_proof and
A5: f = (PR . (len PR)) `1 by A3;
PR <> {} by A4;
then A6: 1 <= len PR by FINSEQ_1:20;
defpred S₁[ Nat] means ( $1 <= len PR implies for m being Nat st 1 <= m & m <= $1 holds
ex g being FinSequence of CQC-WFF Al st
( g = (PR . m) `1 & Ant g |= Suc g ) );
A7: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A8: S₁[k] ; :: thesis:
assume A9: k + 1 <= len PR ; :: thesis:
A10: k <= k + 1 by NAT_1:11;
let m be Nat; :: thesis:
assume that
A11: 1 <= m and
A12: m <= k + 1 ; :: thesis:
A13: m <= len PR by A9, A12, XXREAL_0:2;

A14: now :: thesis:

assume A15: m = k + 1 ; :: thesis:
take g = (PR . m) `1 ; :: thesis:
thus g = (PR . m) `1 ; :: thesis:
reconsider g = (PR . m) `1 as FinSequence of CQC-WFF Al by A11, A13, Lm3;
A16: PR,m is_a_correct_step by A4, A11, A13;

now :: thesis:

not not (PR . m) `2 = 0 & ... & not (PR . m) `2 = 9 by A11, A13, Th31;

per cases ) `2 = 0 or (PR . m) `2 = 1 or (PR . m) `2 = 2 or (PR . m) `2 = 3 or (PR . m) `2 = 4 or (PR . m) `2 = 5 or (PR . m) `2 = 6 or (PR . m) `2 = 7 or (PR . m) `2 = 8 or (PR . m) `2 = 9 ) ;

suppose (PR . m) `2 = 0 ; :: thesis:

then ex f being FinSequence of CQC-WFF Al st
( Suc f is_tail_of Ant f & (PR . m) `1 = f ) by A16, Def7;
hence Ant g |= Suc g by Th15; :: thesis:

end;

suppose (PR . m) `2 = 1 ; :: thesis:

then ex f being FinSequence of CQC-WFF Al st g = f ^ <*(VERUM Al)*> by A16, Def7;
hence Ant g |= Suc g by Th30; :: thesis:

end;

suppose (PR . m) `2 = 2 ; :: thesis:

then consider i being Nat, f, f1 being FinSequence of CQC-WFF Al such that
A17: 1 <= i and
A18: i < m and
A19: ( Ant f is_Subsequence_of Ant f1 & Suc f = Suc f1 & (PR . i) `1 = f & (PR . m) `1 = f1 ) by A16, Def7;
i <= k by A15, A18, NAT_1:13;
then ex h being FinSequence of CQC-WFF Al st
( h = (PR . i) `1 & Ant h |= Suc h ) by A8, A9, A10, A17, XXREAL_0:2;
hence Ant g |= Suc g by A19, Th16; :: thesis:

end;

suppose (PR . m) `2 = 3 ; :: thesis:

then consider i, j being Nat, f, f1 being FinSequence of CQC-WFF Al such that
A20: 1 <= i and
A21: i < m and
A22: 1 <= j and
A23: j < i and
A24: ( len f > 1 & len f1 > 1 & Ant (Ant f) = Ant (Ant f1) & 'not' (Suc (Ant f)) = Suc (Ant f1) & Suc f = Suc f1 & f = (PR . j) `1 & f1 = (PR . i) `1 ) and
A25: (Ant (Ant f)) ^ <*(Suc f)*> = (PR . m) `1 by A16, Def7;
A26: ( Ant g = Ant (Ant f) & Suc g = Suc f ) by A25, Th5;
A27: i <= k by A15, A21, NAT_1:13;
then j <= k by A23, XXREAL_0:2;
then A28: ex h1 being FinSequence of CQC-WFF Al st
( h1 = (PR . j) `1 & Ant h1 |= Suc h1 ) by A8, A9, A10, A22, XXREAL_0:2;
ex h being FinSequence of CQC-WFF Al st
( h = (PR . i) `1 & Ant h |= Suc h ) by A8, A9, A10, A20, A27, XXREAL_0:2;
hence Ant g |= Suc g by A24, A28, A26, Th18; :: thesis:

end;

suppose (PR . m) `2 = 4 ; :: thesis:

then consider i, j being Nat, f, f1 being FinSequence of CQC-WFF Al, p being Element of CQC-WFF Al such that
A29: 1 <= i and
A30: i < m and
A31: 1 <= j and
A32: j < i and
A33: ( len f > 1 & Ant f = Ant f1 & Suc (Ant f) = 'not' p & 'not' (Suc f) = Suc f1 & f = (PR . j) `1 & f1 = (PR . i) `1 ) and
A34: (Ant (Ant f)) ^ <*p*> = (PR . m) `1 by A16, Def7;
A35: ( Ant g = Ant (Ant f) & Suc g = p ) by A34, Th5;
A36: i <= k by A15, A30, NAT_1:13;
then j <= k by A32, XXREAL_0:2;
then A37: ex h1 being FinSequence of CQC-WFF Al st
( h1 = (PR . j) `1 & Ant h1 |= Suc h1 ) by A8, A9, A10, A31, XXREAL_0:2;
ex h being FinSequence of CQC-WFF Al st
( h = (PR . i) `1 & Ant h |= Suc h ) by A8, A9, A10, A29, A36, XXREAL_0:2;
hence Ant g |= Suc g by A33, A37, A35, Th19; :: thesis:

end;

suppose (PR . m) `2 = 5 ; :: thesis:

then consider i, j being Nat, f, f1 being FinSequence of CQC-WFF Al such that
A38: 1 <= i and
A39: i < m and
A40: 1 <= j and
A41: j < i and
A42: ( Ant f = Ant f1 & f = (PR . j) `1 & f1 = (PR . i) `1 ) and
A43: (Ant f) ^ <*((Suc f) '&' (Suc f1))*> = (PR . m) `1 by A16, Def7;
A44: ( Ant g = Ant f & Suc g = (Suc f) '&' (Suc f1) ) by A43, Th5;
A45: i <= k by A15, A39, NAT_1:13;
then j <= k by A41, XXREAL_0:2;
then A46: ex h1 being FinSequence of CQC-WFF Al st
( h1 = (PR . j) `1 & Ant h1 |= Suc h1 ) by A8, A9, A10, A40, XXREAL_0:2;
ex h being FinSequence of CQC-WFF Al st
( h = (PR . i) `1 & Ant h |= Suc h ) by A8, A9, A10, A38, A45, XXREAL_0:2;
hence Ant g |= Suc g by A42, A46, A44, Th20; :: thesis:

end;

suppose (PR . m) `2 = 6 ; :: thesis:

then consider i being Nat, f being FinSequence of CQC-WFF Al, p, q being Element of CQC-WFF Al such that
A47: 1 <= i and
A48: i < m and
A49: ( p '&' q = Suc f & f = (PR . i) `1 ) and
A50: (Ant f) ^ <*p*> = (PR . m) `1 by A16, Def7;
i <= k by A15, A48, NAT_1:13;
then A51: ex h being FinSequence of CQC-WFF Al st
( h = (PR . i) `1 & Ant h |= Suc h ) by A8, A9, A10, A47, XXREAL_0:2;
( Ant g = Ant f & Suc g = p ) by A50, Th5;
hence Ant g |= Suc g by A49, A51, Th21; :: thesis:

end;

suppose (PR . m) `2 = 7 ; :: thesis:

then consider i being Nat, f being FinSequence of CQC-WFF Al, p, q being Element of CQC-WFF Al such that
A52: 1 <= i and
A53: i < m and
A54: ( p '&' q = Suc f & f = (PR . i) `1 ) and
A55: (Ant f) ^ <*q*> = (PR . m) `1 by A16, Def7;
i <= k by A15, A53, NAT_1:13;
then A56: ex h being FinSequence of CQC-WFF Al st
( h = (PR . i) `1 & Ant h |= Suc h ) by A8, A9, A10, A52, XXREAL_0:2;
( Ant g = Ant f & Suc g = q ) by A55, Th5;
hence Ant g |= Suc g by A54, A56, Th22; :: thesis:

end;

suppose (PR . m) `2 = 8 ; :: thesis:

then consider i being Nat, f being FinSequence of CQC-WFF Al, p being Element of CQC-WFF Al, x, y being bound_QC-variable of Al such that
A57: 1 <= i and
A58: i < m and
A59: ( Suc f = All (x,p) & f = (PR . i) `1 ) and
A60: (Ant f) ^ <*(p . (x,y))*> = (PR . m) `1 by A16, Def7;
i <= k by A15, A58, NAT_1:13;
then A61: ex h being FinSequence of CQC-WFF Al st
( h = (PR . i) `1 & Ant h |= Suc h ) by A8, A9, A10, A57, XXREAL_0:2;
( Ant g = Ant f & Suc g = p . (x,y) ) by A60, Th5;
hence Ant g |= Suc g by A59, A61, Th25; :: thesis:

end;

suppose (PR . m) `2 = 9 ; :: thesis:

then consider i being Nat, f being FinSequence of CQC-WFF Al, p being Element of CQC-WFF Al, x, y being bound_QC-variable of Al such that
A62: 1 <= i and
A63: i < m and
A64: ( Suc f = p . (x,y) & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) & f = (PR . i) `1 ) and
A65: (Ant f) ^ <*(All (x,p))*> = (PR . m) `1 by A16, Def7;
i <= k by A15, A63, NAT_1:13;
then A66: ex h being FinSequence of CQC-WFF Al st
( h = (PR . i) `1 & Ant h |= Suc h ) by A8, A9, A10, A62, XXREAL_0:2;
( Ant g = Ant f & Suc g = All (x,p) ) by A65, Th5;
hence Ant g |= Suc g by A64, A66, Th29; :: thesis:

end;

hence ex g being FinSequence of CQC-WFF Al st
( g = (PR . m) `1 & Ant g |= Suc g ) ; :: thesis:

end;

( m <= k implies ex g being FinSequence of CQC-WFF Al st
( g = (PR . m) `1 & Ant g |= Suc g ) ) by A8, A9, A11, A10, XXREAL_0:2;
hence ex g being FinSequence of CQC-WFF Al st
( g = (PR . m) `1 & Ant g |= Suc g ) by A12, A14, NAT_1:8; :: thesis:

end;

A67: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A67, A7);
then consider g being FinSequence of CQC-WFF Al such that
A68: g = (PR . (len PR)) `1 and
A69: Ant g |= Suc g by A6;
let A be non empty set ; :: according to CALCUL_1:def 12 :: thesis:
let J be interpretation of Al,A; :: thesis:
let v be Element of Valuations_in (Al,A); :: thesis:
assume J,v |= X ; :: thesis:
then for p being Element of CQC-WFF Al st p in rng (Ant f) holds
J,v |= p by A1;
then J,v |= rng (Ant f) ;
then J,v |= Ant g by A5, A68;
hence J,v |= p by A2, A5, A68, A69; :: thesis: