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

let k be Element of NAT ; :: thesis:
assume A9: S₁[k] ; :: thesis:
assume A10: ( 1 <= k + 1 & k + 1 <= len L ) ; :: thesis:
set j = k + 1;

A11: now

assume k = 0 ; :: thesis:
then A12: L . (k + 1) = q by A2, SUBSTUT2:def 6;
take q = q; :: thesis:
thus QuantNbr q <= QuantNbr q ; :: thesis:

A13: now

assume JH, valH |= Ex x,('not' r) ; :: thesis:
then consider y being bound_QC-variable such that
A14: JH, valH |= ('not' r) . x,y by Th10;
QuantNbr ('not' r) = 0 by A4, A5, CQC_SIM1:16;
then QuantNbr (('not' r) . x,y) = 0 by Th14;
then CX |- ('not' r) . x,y by A1, A14, Th8;
hence CX |- Ex x,('not' r) by A1, Th3; :: thesis:

end;

now

assume CX |- Ex x,('not' r) ; :: thesis:
then consider y being bound_QC-variable such that
A15: CX |- ('not' r) . x,y by A1, Th3;
QuantNbr ('not' r) = 0 by A4, A5, CQC_SIM1:16;
then QuantNbr (('not' r) . x,y) = 0 by Th14;
then JH, valH |= ('not' r) . x,y by A1, A15, Th8;
hence JH, valH |= Ex x,('not' r) by Th10; :: thesis:

end;

end;

now

assume k <> 0 ; :: thesis:
then ( 0 < k & k < k + 1 ) by NAT_1:3, NAT_1:13;
then A16: ( 0 + 1 <= k & k < len L ) by A10, NAT_1:13;
then consider G1, H1 being Element of QC-WFF such that
A17: ( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) by A2, SUBSTUT2:def 6;
consider p1 being Element of CQC-WFF such that
A18: ( p1 = L . k & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH |= p1 ) & ( JH, valH |= p1 implies CX |- p1 ) ) by A9, A16;
consider F3 being QC-formula such that
A19: ( F3 = L . (k + 1) & F3 is_subformula_of p ) by A2, A10, SUBSTUT2:27;
reconsider s = H1 as Element of CQC-WFF by A2, A10, A17, SUBSTUT2:28;
take s = s; :: thesis:

A20: now

assume s = 'not' p1 ; :: thesis:
then ( QuantNbr q <= QuantNbr s & s = L . (k + 1) & ( CX |- s implies JH, valH |= s ) & ( JH, valH |= s implies CX |- s ) ) by A1, A17, A18, Def1, CQC_SIM1:16, HENMODEL:def 3, VALUAT_1:28;
hence ex p1 being Element of CQC-WFF st
( p1 = L . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH |= p1 ) & ( JH, valH |= p1 implies CX |- p1 ) ) ; :: thesis:

end;

A21: QuantNbr s <= 1 by A1, A17, A19, SUBSTUT2:30;

A22: now

given F1 being QC-formula such that A23: s = p1 '&' F1 ; :: thesis:
reconsider F1 = F1 as Element of CQC-WFF by A23, CQC_LANG:19;
QuantNbr s = (QuantNbr p1) + (QuantNbr F1) by A23, CQC_SIM1:17;
then A24: QuantNbr p1 <= QuantNbr s by NAT_1:11;
then ( QuantNbr p1 <= 1 & 1 <= QuantNbr s ) by A5, A18, A21, XXREAL_0:2;
then ( QuantNbr p1 = 1 & QuantNbr s = 1 ) by A5, A18, A21, XXREAL_0:1;
then 1 - 1 = ((QuantNbr F1) + 1) - 1 by A23, CQC_SIM1:17;
then ( CX |- F1 iff JH, valH |= F1 ) by A1, Th8;
then ( QuantNbr q <= QuantNbr s & s = L . (k + 1) & ( CX |- s implies JH, valH |= s ) & ( JH, valH |= s implies CX |- s ) ) by A17, A18, A23, A24, Th6, VALUAT_1:29, XXREAL_0:2;
hence ex p1 being Element of CQC-WFF st
( p1 = L . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH |= p1 ) & ( JH, valH |= p1 implies CX |- p1 ) ) ; :: thesis:

end;

A25: now

given F1 being QC-formula such that A26: s = F1 '&' p1 ; :: thesis:
reconsider F1 = F1 as Element of CQC-WFF by A26, CQC_LANG:19;
A27: QuantNbr s = (QuantNbr p1) + (QuantNbr F1) by A26, CQC_SIM1:17;
then A28: QuantNbr p1 <= QuantNbr s by NAT_1:11;
then ( QuantNbr p1 <= 1 & 1 <= QuantNbr s ) by A5, A18, A21, XXREAL_0:2;
then ( QuantNbr p1 = 1 & QuantNbr s = 1 ) by A5, A18, A21, XXREAL_0:1;
then ( CX |- F1 iff JH, valH |= F1 ) by A1, A27, Th8;
then ( QuantNbr q <= QuantNbr s & s = L . (k + 1) & ( CX |- s implies JH, valH |= s ) & ( JH, valH |= s implies CX |- s ) ) by A17, A18, A26, A28, Th6, VALUAT_1:29, XXREAL_0:2;
hence ex p1 being Element of CQC-WFF st
( p1 = L . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH |= p1 ) & ( JH, valH |= p1 implies CX |- p1 ) ) ; :: thesis:

end;

now

given x being bound_QC-variable such that A29: s = All x,p1 ; :: thesis:
1 < (QuantNbr p1) + 1 by A5, A18, NAT_1:13;
hence contradiction by A21, A29, CQC_SIM1:18; :: thesis:

end;

hence ex p1 being Element of CQC-WFF st
( p1 = L . (k + 1) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH |= p1 ) & ( JH, valH |= p1 implies CX |- p1 ) ) by A17, A18, A20, A22, A25, QC_LANG2:def 20; :: thesis:

end;

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

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A7, A8);
then consider p1 being Element of CQC-WFF such that
A30: ( p1 = L . (len L) & QuantNbr q <= QuantNbr p1 & ( CX |- p1 implies JH, valH |= p1 ) & ( JH, valH |= p1 implies CX |- p1 ) ) by A6;
thus ( JH, valH |= p iff CX |- p ) by A2, A30, SUBSTUT2:def 6; :: thesis: