let A be QC-alphabet ; :: thesis: for X being Subset of (CQC-WFF A)
for F, G being Element of CQC-WFF A st F is closed & X \/ {F} |- G holds
X |- F => G
let X be Subset of (CQC-WFF A); :: thesis: for F, G being Element of CQC-WFF A st F is closed & X \/ {F} |- G holds
X |- F => G
let F, G be Element of CQC-WFF A; :: 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;
then consider f being FinSequence of [:(CQC-WFF A),Proof_Step_Kinds:] such that
A3: f is_a_proof_wrt X \/ {F} and
A4: Effect f = G by CQC_THE1:36;
f <> {} by A3;
then A5: G = (f . (len f)) `1 by A4, CQC_THE1:def 6;
defpred S<sub>1</sub>[ Nat] means ( 1 <= $1 & $1 <= len f implies for H being Element of CQC-WFF A st H = (f . $1) `1 holds
X |- F => H );
A6: 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 A7: for k being Nat st k < n & 1 <= k & k <= len f holds
for H being Element of CQC-WFF A st H = (f . k) `1 holds
X |- F => H ; :: thesis: S<sub>1</sub>[n]
assume that
A8: 1 <= n and
A9: n <= len f ; :: thesis: for H being Element of CQC-WFF A st H = (f . n) `1 holds
X |- F => H
A10: f,n is_a_correct_step_wrt X \/ {F} by A3, A8, A9;
let H be Element of CQC-WFF A; :: thesis: ( H = (f . n) `1 implies X |- F => H )
assume A11: H = (f . n) `1 ; :: thesis: X |- F => H

now :: thesis: X |- F => H

not not (f . n) `2 = 0 & ... & not (f . n) `2 = 9 by A8, A9, CQC_THE1:23;

per cases then ( (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 ) ;

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

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

now :: thesis: X |- F => H

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

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

X c= Cn X by CQC_THE1:17;
then A14: X |- H by A13;
X |- H => (F => H) by CQC_THE1:59;
hence X |- F => H by A14, CQC_THE1:55; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

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

then H = VERUM A by A11, A10, CQC_THE1:def 4;
hence X |- F => H by CQC_THE1:59, LUKASI_1:46; :: thesis: verum

end;

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

then ex p being Element of CQC-WFF A st H = (('not' p) => p) => p by A11, A10, CQC_THE1:def 4;
then H is valid by CQC_THE1:61;
hence X |- F => H by CQC_THE1:59, LUKASI_1:61; :: thesis: verum

end;

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

then ex p, q being Element of CQC-WFF A st H = p => (('not' p) => q) by A11, A10, CQC_THE1:def 4;
then H is valid by CQC_THE1:62;
hence X |- F => H by CQC_THE1:59, LUKASI_1:61; :: thesis: verum

end;

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

then ex p, q, r being Element of CQC-WFF A st H = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) by A11, A10, CQC_THE1:def 4;
then H is valid by CQC_THE1:63;
hence X |- F => H by CQC_THE1:59, LUKASI_1:61; :: thesis: verum

end;

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

then ex p, q being Element of CQC-WFF A st H = (p '&' q) => (q '&' p) by A11, A10, CQC_THE1:def 4;
then H is valid by CQC_THE1:64;
hence X |- F => H by CQC_THE1:59, LUKASI_1:61; :: thesis: verum

end;

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

then ex p being Element of CQC-WFF A ex x being bound_QC-variable of A st H = (All (x,p)) => p by A11, A10, CQC_THE1:def 4;
then H is valid by CQC_THE1:66;
hence X |- F => H by CQC_THE1:59, LUKASI_1:61; :: thesis: verum

end;

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

then consider i, j being Nat, p, q being Element of CQC-WFF A such that
A15: 1 <= i and
A16: i < n and
A17: 1 <= j and
A18: j < i and
A19: p = (f . j) `1 and
A20: q = H and
A21: (f . i) `1 = p => q by A11, A10, CQC_THE1:def 4;
i <= len f by A9, A16, XXREAL_0:2;
then A22: X |- F => (p => q) by A7, A15, A16, A21;
X |- (F => (p => q)) => ((F => p) => (F => q)) by CQC_THE1:59;
then A23: X |- (F => p) => (F => q) by A22, CQC_THE1:55;
j < n by A16, A18, XXREAL_0:2;
then A24: j <= len f by A9, XXREAL_0:2;
j < n by A16, A18, XXREAL_0:2;
then X |- F => p by A7, A17, A19, A24;
hence X |- F => H by A20, A23, CQC_THE1:55; :: thesis: verum

end;

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

then consider i being Nat, p, q being Element of CQC-WFF A, x being bound_QC-variable of A such that
A25: 1 <= i and
A26: i < n and
A27: (f . i) `1 = p => q and
A28: not x in still_not-bound_in p and
A29: H = p => (All (x,q)) by A11, A10, CQC_THE1:def 4;
A30: X |- (All (x,(p => q))) => (p => (All (x,q))) by A28, Th74, CQC_THE1:59;
not x in still_not-bound_in F by A1, QC_LANG1:def 31;
then A31: X |- (All (x,(F => (p => q)))) => (F => (All (x,(p => q)))) by Th74, CQC_THE1:59;
i <= len f by A9, A26, XXREAL_0:2;
then X |- All (x,(F => (p => q))) by A7, A25, A26, A27, Th90;
then X |- F => (All (x,(p => q))) by A31, CQC_THE1:55;
hence X |- F => H by A29, A30, LUKASI_1:59; :: thesis: verum

end;

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

then consider i being Nat, x, y being bound_QC-variable of A, s being QC-formula of A such that
A32: 1 <= i and
A33: i < n and
A34: ( s . x in CQC-WFF A & s . y in CQC-WFF A ) and
A35: not x in still_not-bound_in s and
A36: s . x = (f . i) `1 and
A37: H = s . y by A11, A10, CQC_THE1:def 4;
reconsider s1 = s . x, s2 = s . y as Element of CQC-WFF A by A34;
A38: X |- (All (x,s1)) => s2 by A35, Th25, CQC_THE1:59;
not x in still_not-bound_in F by A1, QC_LANG1:def 31;
then A39: X |- (All (x,(F => s1))) => (F => (All (x,s1))) by Th74, CQC_THE1:59;
i <= len f by A9, A33, XXREAL_0:2;
then X |- All (x,(F => s1)) by A7, A32, A33, A36, Th90;
then X |- F => (All (x,s1)) by A39, CQC_THE1:55;
hence X |- F => H by A37, A38, LUKASI_1:59; :: thesis: verum

end;

end;

end;

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

end;

A40: for n being Nat holds S₁[n] from NAT_1:sch 4(A6);
1 <= len f by A3, CQC_THE1:25;
hence X |- F => G by A40, A5; :: thesis: verum