let Al be QC-alphabet ; :: thesis:
let CX be Consistent Subset of (CQC-WFF Al); :: thesis:
let JH be Henkin_interpretation of CX; :: thesis:
let p be Element of CQC-WFF Al; :: thesis:
assume that
A1: QuantNbr p = 1 and
A2: CX is negation_faithful and
A3: CX is with_examples ; :: thesis:
consider q being Element of CQC-WFF Al such that
A4: q is_subformula_of p and
A5: ex x being bound_QC-variable of Al ex r being Element of CQC-WFF Al st q = All (x,r) by A1, SUBSTUT2:32;
consider x being bound_QC-variable of Al, r being Element of CQC-WFF Al such that
A6: q = All (x,r) by A5;
A7: QuantNbr q <= 1 by A1, A4, SUBSTUT2:30;
A8: QuantNbr q = (QuantNbr r) + 1 by A6, CQC_SIM1:18;
then 1 <= QuantNbr q by NAT_1:11;
then A9: 1 = QuantNbr q by A7, XXREAL_0:1;
set L = the PATH of q,p;
A10: 1 <= len the PATH of q,p by A4, SUBSTUT2:def 5;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len the PATH of q,p implies ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . $1 & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) ) );
A11: S₁[ 0 ] ;
A12: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis:
assume A13: S₁[k] ; :: thesis:
assume that
A14: 1 <= k + 1 and
A15: k + 1 <= len the PATH of q,p ; :: thesis:
set j = k + 1;

end;

end;

then ( JH, valH Al |= 'not' (Ex (x,('not' r))) iff CX |- 'not' (Ex (x,('not' r))) ) by A2, A18, HENMODEL:def 2, VALUAT_1:17;
then ( JH, valH Al |= q iff CX |- q ) by A6, Th11, Th12;
hence ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) ) by A17; :: thesis:

end;

assume k <> 0 ; :: thesis:
then 0 < k by NAT_1:3;
then A21: 0 + 1 <= k by NAT_1:13;
k < len the PATH of q,p by A15, NAT_1:13;
then consider G1, H1 being Element of QC-WFF Al such that
A22: the PATH of q,p . k = G1 and
A23: the PATH of q,p . (k + 1) = H1 and
A24: G1 is_immediate_constituent_of H1 by A4, A21, SUBSTUT2:def 5;
consider p1 being Element of CQC-WFF Al such that
A25: p1 = the PATH of q,p . k and
A26: QuantNbr q <= QuantNbr p1 and
A27: ( CX |- p1 iff JH, valH Al |= p1 ) by A13, A15, A21, NAT_1:13;
A28: ex F3 being QC-formula of Al st
( F3 = the PATH of q,p . (k + 1) & F3 is_subformula_of p ) by A4, A14, A15, SUBSTUT2:27;
reconsider s = H1 as Element of CQC-WFF Al by A4, A14, A15, A23, SUBSTUT2:28;
take s = s; :: thesis:

end;

end;

end;

end;

hence ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) ) by A22, A24, A25, A29, A33, A41, QC_LANG2:def 19; :: thesis:

end;

hence ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) ) by A16; :: thesis:

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A11, A12);
then ex p1 being Element of CQC-WFF Al st
( p1 = the PATH of q,p . (len the PATH of q,p) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH Al |= p1 ) & ( JH, valH Al |= p1 implies CX |- p1 ) ) by A10;
hence ( JH, valH Al |= p iff CX |- p ) by A4, SUBSTUT2:def 5; :: thesis: