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 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 such that
A4: q is_subformula_of p and
A5: 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
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;
consider L being PATH of q,p;
A10: 1 <= len L by A4, 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 ) ) );
A11: S₁[ 0 ] ;
A12: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

let k be Element of NAT ; :: thesis:
assume A13: S₁[k] ; :: thesis:
assume that
A14: 1 <= k + 1 and
A15: k + 1 <= len L ; :: thesis:
set j = k + 1;

A16: now

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

A18: now

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

end;

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

end;

then ( JH, valH |= 'not' (Ex x,('not' r)) iff CX |- 'not' (Ex x,('not' r)) ) by A2, A18, Def1, HENMODEL:def 3, VALUAT_1:28;
then ( JH, valH |= q iff CX |- q ) by A6, Th11, Th12;
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; :: thesis:

end;

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

A29: now

assume A30: s = 'not' p1 ; :: thesis:
then A31: QuantNbr q <= QuantNbr s by A26, CQC_SIM1:16;
( CX |- s iff JH, valH |= s ) by A2, A27, A30, Def1, 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 ) ) by A23, A31; :: thesis:

end;

A32: QuantNbr s <= 1 by A1, A23, A28, SUBSTUT2:30;

A33: now

given F1 being QC-formula such that A34: s = p1 '&' F1 ; :: thesis:
reconsider F1 = F1 as Element of CQC-WFF by A34, CQC_LANG:19;
QuantNbr s = (QuantNbr p1) + (QuantNbr F1) by A34, CQC_SIM1:17;
then A35: QuantNbr p1 <= QuantNbr s by NAT_1:11;
then A36: QuantNbr p1 <= 1 by A32, XXREAL_0:2;
A37: 1 <= QuantNbr s by A9, A26, A35, XXREAL_0:2;
A38: QuantNbr p1 = 1 by A9, A26, A36, XXREAL_0:1;
QuantNbr s = 1 by A32, A37, XXREAL_0:1;
then 1 - 1 = ((QuantNbr F1) + 1) - 1 by A34, A38, CQC_SIM1:17;
then A39: ( CX |- F1 iff JH, valH |= F1 ) by A2, A3, Th8;
A40: QuantNbr q <= QuantNbr s by A26, A35, XXREAL_0:2;
( CX |- s iff JH, valH |= s ) by A27, A34, A39, Th6, VALUAT_1:29;
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 A23, A40; :: thesis:

end;

A41: now

given F1 being QC-formula such that A42: s = F1 '&' p1 ; :: thesis:
reconsider F1 = F1 as Element of CQC-WFF by A42, CQC_LANG:19;
A43: QuantNbr s = (QuantNbr p1) + (QuantNbr F1) by A42, CQC_SIM1:17;
then A44: QuantNbr p1 <= QuantNbr s by NAT_1:11;
then A45: QuantNbr p1 <= 1 by A32, XXREAL_0:2;
A46: 1 <= QuantNbr s by A9, A26, A44, XXREAL_0:2;
A47: QuantNbr p1 = 1 by A9, A26, A45, XXREAL_0:1;
QuantNbr s = 1 by A32, A46, XXREAL_0:1;
then A48: ( CX |- F1 iff JH, valH |= F1 ) by A2, A3, A43, A47, Th8;
A49: QuantNbr q <= QuantNbr s by A26, A44, XXREAL_0:2;
( CX |- s iff JH, valH |= s ) by A27, A42, A48, Th6, VALUAT_1:29;
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 A23, A49; :: thesis:

end;

given x being bound_QC-variable such that A50: s = All x,p1 ; :: thesis:
1 < (QuantNbr p1) + 1 by A9, A26, NAT_1:13;
hence contradiction by A32, A50, 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 A22, A24, A25, A29, A33, A41, 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 A16; :: thesis:

end;

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