let X be Subset of CQC-WFF ; :: thesis:
let p be Element of CQC-WFF ; :: thesis:
assume A1: p in Cn X ; :: thesis:
consider f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] such that
A2: f is_a_proof_wrt X and
A3: Effect f = p by A1, Th70;
A4: f <> {} by A2, Def5;
A5: rng f c= [:CQC-WFF ,Proof_Step_Kinds :] by FINSEQ_1:def 4;
consider A being set such that
A6: A is finite and
A7: A c= CQC-WFF and
A8: rng f c= [:A,Proof_Step_Kinds :] by A5, FINSET_1:33;
reconsider Z = A as Subset of CQC-WFF by A7;
take Y = Z /\ X; :: thesis:
thus Y c= X by XBOOLE_1:17; :: thesis:
thus Y is finite by A6; :: thesis:
A9: for n being Element of NAT st 1 <= n & n <= len f holds
f,n is_a_correct_step_wrt Y

let n be Element of NAT ; :: thesis:
assume A10: ( 1 <= n & n <= len f ) ; :: thesis:
A11: f,n is_a_correct_step_wrt X by A2, A10, Def5;

per cases ) `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 A10, Th45;
:: according to CQC_THE1:def 4

case A12: (f . n) `2 = 0 ; :: thesis:

A13: (f . n) `1 in X by A11, A12, Def4;
A14: n in Seg (len f) by A10, FINSEQ_1:3;
A15: n in dom f by A14, FINSEQ_1:def 3;
A16: f . n in rng f by A15, FUNCT_1:def 5;
A17: (f . n) `1 in A by A8, A16, MCART_1:10;
thus (f . n) `1 in Y by A13, A17, XBOOLE_0:def 4; :: thesis:

end;

case A18: (f . n) `2 = 1 ; :: thesis:

thus (f . n) `1 = VERUM by A11, A18, Def4; :: thesis:

end;

case A19: (f . n) `2 = 2 ; :: thesis:

thus ex p being Element of CQC-WFF st (f . n) `1 = (('not' p) => p) => p by A11, A19, Def4; :: thesis:

end;

case A20: (f . n) `2 = 3 ; :: thesis:

thus ex p, q being Element of CQC-WFF st (f . n) `1 = p => (('not' p) => q) by A11, A20, Def4; :: thesis:

end;

case A21: (f . n) `2 = 4 ; :: thesis:

thus ex p, q, r being Element of CQC-WFF st (f . n) `1 = (p => q) => (('not' (q '&' r)) => ('not' (p '&' r))) by A11, A21, Def4; :: thesis:

end;

case A22: (f . n) `2 = 5 ; :: thesis:

thus ex p, q being Element of CQC-WFF st (f . n) `1 = (p '&' q) => (q '&' p) by A11, A22, Def4; :: thesis:

end;

case A23: (f . n) `2 = 6 ; :: thesis:

thus ex p being Element of CQC-WFF ex x being bound_QC-variable st (f . n) `1 = (All x,p) => p by A11, A23, Def4; :: thesis:

end;

case A24: (f . n) `2 = 7 ; :: thesis:

thus ex i, j being Element of NAT ex p, q being Element of CQC-WFF st
( 1 <= i & i < n & 1 <= j & j < i & p = (f . j) `1 & q = (f . n) `1 & (f . i) `1 = p => q ) by A11, A24, Def4; :: thesis:

end;

case A25: (f . n) `2 = 8 ; :: thesis:

thus ex i being Element of NAT ex p, q being Element of CQC-WFF ex x being bound_QC-variable st
( 1 <= i & i < n & (f . i) `1 = p => q & not x in still_not-bound_in p & (f . n) `1 = p => (All x,q) ) by A11, A25, Def4; :: thesis:

end;

case A26: (f . n) `2 = 9 ; :: thesis:

thus ex i being Element of NAT ex x, y being bound_QC-variable ex s being QC-formula st
( 1 <= i & i < n & s . x in CQC-WFF & s . y in CQC-WFF & not x in still_not-bound_in s & s . x = (f . i) `1 & s . y = (f . n) `1 ) by A11, A26, Def4; :: thesis:

end;

end;

end;

A27: f is_a_proof_wrt Y by A4, A9, Def5;
A28: p in { q where q is Element of CQC-WFF : ex f being FinSequence of [:CQC-WFF ,Proof_Step_Kinds :] st
( f is_a_proof_wrt Y & Effect f = q ) } by A3, A27;
thus p in Cn Y by A28, Th69; :: thesis: