let X be Subset of MC-wff; :: thesis: for F, G being Element of MC-wff st X \/ {F} |-_IPC G holds
X |-_IPC F => G
let F, G be Element of MC-wff ; :: thesis: ( X \/ {F} |-_IPC G implies X |-_IPC F => G )
assume X \/ {F} |-_IPC G ; :: thesis: X |-_IPC F => G
then G in CnIPC (X \/ {F}) ;
then consider f being FinSequence of [:MC-wff,Proof_Step_Kinds_IPC:] such that
A3: f is_a_proof_wrt_IPC X \/ {F} and
A4: Effect_IPC f = G by Th16;
f <> {} by A3;
then A5: G = (f . (len f)) `1 by A4, Def5;
defpred S<sub>1</sub>[ Nat] means ( 1 <= $1 & $1 <= len f implies for H being Element of MC-wff st H = (f . $1) `1 holds
X |-_IPC 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 MC-wff st H = (f . k) `1 holds
X |-_IPC F => H ; :: thesis: S<sub>1</sub>[n]
assume that
A8: 1 <= n and
A9: n <= len f ; :: thesis: for H being Element of MC-wff st H = (f . n) `1 holds
X |-_IPC F => H
A10: f,n is_a_correct_step_wrt_IPC X \/ {F} by A3, A8, A9;
let H be Element of MC-wff ; :: thesis: ( H = (f . n) `1 implies X |-_IPC F => H )
assume A11: H = (f . n) `1 ; :: thesis: X |-_IPC F => H

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

not not (f . n) `2 = 0 & ... & not (f . n) `2 = 10 by A8, A9, Th3;

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 or (f . n) `2 = 10 ) ;

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

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

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

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

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

X c= CnIPC X by INTPRO_1:12;
then A14: X |-_IPC H by A13;
X |-_IPC H => (F => H) by INTPRO_1:1;
hence X |-_IPC F => H by A14, INTPRO_1:10; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

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

then ex p, q being Element of MC-wff st H = p => (q => p) by A11, A10, Def3;
then H is valid_IPC by Th39;
hence X |-_IPC F => H by Th51, Th52; :: thesis: verum

end;

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

then ex p, q, r being Element of MC-wff st H = (p => (q => r)) => ((p => q) => (p => r)) by A11, A10, Def3;
then H is valid_IPC by Th40;
hence X |-_IPC F => H by Th51, Th52; :: thesis: verum

end;

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

then ex p, q being Element of MC-wff st H = (p '&' q) => p by A11, A10, Def3;
then H is valid_IPC by Th41;
hence X |-_IPC F => H by Th51, Th52; :: thesis: verum

end;

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

then ex p, q being Element of MC-wff st H = (p '&' q) => q by A11, A10, Def3;
then H is valid_IPC by Th42;
hence X |-_IPC F => H by Th51, Th52; :: thesis: verum

end;

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

then ex p, q being Element of MC-wff st H = p => (q => (p '&' q)) by A11, A10, Def3;
then H is valid_IPC by Th43;
hence X |-_IPC F => H by Th51, Th52; :: thesis: verum

end;

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

then ex p, q being Element of MC-wff st H = p => (p 'or' q) by A11, A10, Def3;
then H is valid_IPC by Th44;
hence X |-_IPC F => H by Th51, Th52; :: thesis: verum

end;

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

then ex p, q being Element of MC-wff st H = q => (p 'or' q) by A11, A10, Def3;
then H is valid_IPC by Th45;
hence X |-_IPC F => H by Th51, Th52; :: thesis: verum

end;

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

then ex p, q, r being Element of MC-wff st H = (p => r) => ((q => r) => ((p 'or' q) => r)) by A11, A10, Def3;
then H is valid_IPC by Th46;
hence X |-_IPC F => H by Th51, Th52; :: thesis: verum

end;

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

then ex p being Element of MC-wff st H = FALSUM => p by A11, A10, Def3;
then H is valid_IPC by Th47;
hence X |-_IPC F => H by Th51, Th52; :: thesis: verum

end;

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

then consider i, j being Nat, p, q being Element of MC-wff 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, Def3;
i <= len f by A9, A16, XXREAL_0:2;
then A22: X |-_IPC F => (p => q) by A7, A15, A16, A21;
X |-_IPC (F => (p => q)) => ((F => p) => (F => q)) by INTPRO_1:2;
then A23: X |-_IPC (F => p) => (F => q) by A22, INTPRO_1:10;
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 |-_IPC F => p by A7, A17, A19, A24;
hence X |-_IPC F => H by A20, A23, INTPRO_1:10; :: thesis: verum

end;

end;

end;

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

end;

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