let X be Subset of CQC-WFF ; :: thesis: for F, G being Element of CQC-WFF st F is closed & X \/ {F} |- G holds
X |- F => G
let F, G be Element of CQC-WFF ; :: thesis: ( F is closed & X \/ {F} |- G implies X |- F => G )
assume that
A1: F is closed and
A2: X \/ {F} |- G ; :: thesis: X |- F => G
G in Cn (X \/ {F}) by A2, CQC_THE1:def 9;
then consider f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] such that
A3: f is_a_proof_wrt X \/ {F} and
A4: Effect f = G by CQC_THE1:70;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len f implies for H being Element of CQC-WFF st H = (f . $1) `1 holds
X |- F => H );
A5: for n being Nat st ( for k being Nat st k < n holds
S₁[k] ) holds
S₁[n]

proof

let n be Nat; :: thesis: ( ( for k being Nat st k < n holds
S₁[k] ) implies S₁[n] )
assume A6: for k being Nat st k < n & 1 <= k & k <= len f holds
for H being Element of CQC-WFF st H = (f . k) `1 holds
X |- F => H ; :: thesis: S<sub>1</sub>[n]
assume A7: ( 1 <= n & n <= len f ) ; :: thesis: for H being Element of CQC-WFF st H = (f . n) `1 holds
X |- F => H
let H be Element of CQC-WFF ; :: thesis: ( H = (f . n) `1 implies X |- F => H )
assume A8: H = (f . n) `1 ; :: thesis: X |- F => H
n in NAT by ORDINAL1:def 13;
then A9: f,n is_a_correct_step_wrt X \/ {F} by A3, A7, CQC_THE1:def 5;

now

per cases ( (f . n) `2 = 0 or (f . n) `2 = 1 or (f . n) `2 = 2 or (f . n) `2 = 3 or (f . n) `2 = 4 or (f . n) `2 = 5 or (f . n) `2 = 6 or (f . n) `2 = 7 or (f . n) `2 = 8 or (f . n) `2 = 9 ) by A7, CQC_THE1:45;

suppose (f . n) `2 = 0 ; :: thesis: X |- F => H

then H in X \/ {F} by A8, A9, CQC_THE1:def 4;
then A10: ( H in X or H in {F} ) by XBOOLE_0:def 3;

now

per cases ( H in X or H = F ) by A10, TARSKI:def 1;

suppose A11: H in X ; :: thesis: X |- F => H

X c= Cn X by CQC_THE1:38;
then ( H in Cn X & H => (F => H) is valid ) by A11, LUKASI_1:45;
then ( X |- H & X |- H => (F => H) ) by CQC_THE1:98, CQC_THE1:def 9;
hence X |- F => H by CQC_THE1:92; :: thesis: verum

end;

suppose H = F ; :: thesis: X |- F => H

hence X |- F => H by CQC_THE1:98, LUKASI_1:44; :: thesis: verum

end;

end;

end;

hence X |- F => H ; :: thesis: verum

end;

suppose (f . n) `2 = 1 ; :: thesis: X |- F => H

then H = VERUM by A8, A9, CQC_THE1:def 4;
then F => H is valid by LUKASI_1:50;
hence X |- F => H by CQC_THE1:98; :: thesis: verum

end;

suppose (f . n) `2 = 2 ; :: thesis: X |- F => H

then ex p being Element of CQC-WFF st H = (('not' p) => p) => p by A8, A9, CQC_THE1:def 4;
then H is valid by CQC_THE1:100;
hence X |- F => H by CQC_THE1:98, LUKASI_1:78; :: thesis: verum

end;

suppose (f . n) `2 = 3 ; :: thesis: X |- F => H

then ex p, q being Element of CQC-WFF st H = p => (('not' p) => q) by A8, A9, CQC_THE1:def 4;
then H is valid by CQC_THE1:101;
hence X |- F => H by CQC_THE1:98, LUKASI_1:78; :: thesis: verum

end;

suppose (f . n) `2 = 4 ; :: thesis: X |- F => H

then ex p, q, r being Element of CQC-WFF st H = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) by A8, A9, CQC_THE1:def 4;
then H is valid by CQC_THE1:102;
hence X |- F => H by CQC_THE1:98, LUKASI_1:78; :: thesis: verum

end;

suppose (f . n) `2 = 5 ; :: thesis: X |- F => H

then ex p, q being Element of CQC-WFF st H = (p '&' q) => (q '&' p) by A8, A9, CQC_THE1:def 4;
then H is valid by CQC_THE1:103;
hence X |- F => H by CQC_THE1:98, LUKASI_1:78; :: thesis: verum

end;

suppose (f . n) `2 = 6 ; :: thesis: X |- F => H

then ex p being Element of CQC-WFF ex x being bound_QC-variable st H = (All x,p) => p by A8, A9, CQC_THE1:def 4;
then H is valid by CQC_THE1:105;
hence X |- F => H by CQC_THE1:98, LUKASI_1:78; :: thesis: verum

end;

suppose (f . n) `2 = 7 ; :: thesis: X |- F => H

then consider i, j being Element of NAT , p, q being Element of CQC-WFF such that
A12: ( 1 <= i & i < n & 1 <= j & j < i ) and
A13: ( p = (f . j) `1 & q = H & (f . i) `1 = p => q ) by A8, A9, CQC_THE1:def 4;
( j < n & i <= n & j <= n ) by A12, XXREAL_0:2;
then ( i < n & 1 <= i & i <= len f & j < n & 1 <= j & j <= len f ) by A7, A12, XXREAL_0:2;
then A14: ( X |- F => (p => q) & X |- F => p ) by A6, A13;
X |- (F => (p => q)) => ((F => p) => (F => q)) by CQC_THE1:98, LUKASI_1:54;
then X |- (F => p) => (F => q) by A14, CQC_THE1:92;
hence X |- F => H by A13, A14, CQC_THE1:92; :: thesis: verum

end;

suppose (f . n) `2 = 8 ; :: thesis: X |- F => H

then consider i being Element of NAT , p, q being Element of CQC-WFF , x being bound_QC-variable such that
A15: ( 1 <= i & i < n ) and
A16: (f . i) `1 = p => q and
A17: ( not x in still_not-bound_in p & H = p => (All x,q) ) by A8, A9, CQC_THE1:def 4;
A18: not x in still_not-bound_in F by A1, QC_LANG1:def 30;
i <= len f by A7, A15, XXREAL_0:2;
then A19: X |- All x,(F => (p => q)) by A6, A15, A16, Th94;
(All x,(F => (p => q))) => (F => (All x,(p => q))) is valid by A18, Th78;
then X |- (All x,(F => (p => q))) => (F => (All x,(p => q))) by CQC_THE1:98;
then A20: X |- F => (All x,(p => q)) by A19, CQC_THE1:92;
X |- (All x,(p => q)) => (p => (All x,q)) by A17, Th95;
hence X |- F => H by A17, A20, LUKASI_1:76; :: thesis: verum

end;

suppose (f . n) `2 = 9 ; :: thesis: X |- F => H

then consider i being Element of NAT , x, y being bound_QC-variable, s being QC-formula such that
A21: ( 1 <= i & i < n ) and
A22: ( s . x in CQC-WFF & s . y in CQC-WFF ) and
A23: ( not x in still_not-bound_in s & s . x = (f . i) `1 & H = s . y ) by A8, A9, CQC_THE1:def 4;
reconsider s1 = s . x, s2 = s . y as Element of CQC-WFF by A22;
i <= len f by A7, A21, XXREAL_0:2;
then A24: X |- All x,(F => s1) by A6, A21, A23, Th94;
not x in still_not-bound_in F by A1, QC_LANG1:def 30;
then X |- (All x,(F => s1)) => (F => (All x,s1)) by Th95;
then A25: X |- F => (All x,s1) by A24, CQC_THE1:92;
X |- (All x,s1) => s2 by A23, Th28, CQC_THE1:98;
hence X |- F => H by A23, A25, LUKASI_1:76; :: thesis: verum

end;

end;

end;

hence X |- F => H ; :: thesis: verum

end;

A26: for n being Nat holds S₁[n] from NAT_1:sch 4(A5);
A27: ( 1 <= len f & len f <= len f ) by A3, CQC_THE1:58;
f <> {} by A3, CQC_THE1:def 5;
then G = (f . (len f)) `1 by A4, CQC_THE1:def 6;
hence X |- F => G by A26, A27; :: thesis: verum