let Al be QC-alphabet ; :: thesis: for i, n being Nat
for p, q being Element of CQC-WFF Al
for L being PATH of q,p st QuantNbr p <= n & q is_subformula_of p & 1 <= i & i <= len L holds
ex r being Element of CQC-WFF Al st
( r = L . i & QuantNbr r <= n )
let i, n be Nat; :: thesis: for p, q being Element of CQC-WFF Al
for L being PATH of q,p st QuantNbr p <= n & q is_subformula_of p & 1 <= i & i <= len L holds
ex r being Element of CQC-WFF Al st
( r = L . i & QuantNbr r <= n )
let p, q be Element of CQC-WFF Al; :: thesis: for L being PATH of q,p st QuantNbr p <= n & q is_subformula_of p & 1 <= i & i <= len L holds
ex r being Element of CQC-WFF Al st
( r = L . i & QuantNbr r <= n )
let L be PATH of q,p; :: thesis: ( QuantNbr p <= n & q is_subformula_of p & 1 <= i & i <= len L implies ex r being Element of CQC-WFF Al st
( r = L . i & QuantNbr r <= n ) )
set m = len L;
assume that
A1: QuantNbr p <= n and
A2: q is_subformula_of p and
A3: 1 <= i and
A4: i <= len L ; :: thesis: ex r being Element of CQC-WFF Al st
( r = L . i & QuantNbr r <= n )
i + (- i) <= (len L) + (- i) by A4, XREAL_1:6;
then reconsider l = (len L) - i as Element of NAT by INT_1:3;
(len L) + 1 <= (len L) + i by A3, XREAL_1:6;
then ((len L) + 1) + (- 1) <= ((len L) + i) + (- 1) by XREAL_1:6;
then A5: (len L) + (- i) <= (((len L) - 1) + i) + (- i) by XREAL_1:6;
defpred S₁[ Nat] means ( $1 <= (len L) - 1 implies ex r being Element of CQC-WFF Al st
( r = L . ((len L) - $1) & QuantNbr r <= n ) );
A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: S₁[k] ; :: thesis: S₁[k + 1]
assume A8: k + 1 <= (len L) - 1 ; :: thesis: ex r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )
then (k + 1) + 1 <= ((len L) - 1) + 1 by XREAL_1:6;
then A9: (2 + k) + (- k) <= (len L) + (- k) by XREAL_1:6;
then reconsider j = (len L) - k as Element of NAT by INT_1:3;
A10: (1 + 1) + (- 1) <= j + (- 1) by A9, XREAL_1:6;
then reconsider j1 = j - 1 as Element of NAT by INT_1:3;
len L <= (len L) + k by NAT_1:11;
then (len L) + (- k) <= ((len L) + k) + (- k) by XREAL_1:6;
then A11: j - 1 < len L by XREAL_1:146, XXREAL_0:2;
j1 + 1 = j ;
then consider G1, H1 being Element of QC-WFF Al such that
A12: L . j1 = G1 and
A13: ( L . j = H1 & G1 is_immediate_constituent_of H1 ) by A2, A10, A11, Def5;
reconsider r = G1 as Element of CQC-WFF Al by A2, A10, A11, A12, Th28;
k < k + 1 by NAT_1:13;
then consider q being Element of CQC-WFF Al such that
A14: q = L . j and
A15: QuantNbr q <= n by A7, A8, XXREAL_0:2;

A16: now :: thesis: ( ex x being bound_QC-variable of Al st q = All (x,G1) implies ex r, r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) )

given x being bound_QC-variable of Al such that A17: q = All (x,G1) ; :: thesis: ex r, r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )
take r = r; :: thesis: ex r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )
(QuantNbr r) + 1 <= n by A15, A17, CQC_SIM1:18;
then QuantNbr r <= n by NAT_1:13;
hence ex r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) by A12; :: thesis: verum

end;

A18: now :: thesis: ( ex F being Element of QC-WFF Al st q = F '&' G1 implies ex r, r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) )

given F being Element of QC-WFF Al such that A19: q = F '&' G1 ; :: thesis: ex r, r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )
reconsider F = F as Element of CQC-WFF Al by A19, CQC_LANG:9;
take r = r; :: thesis: ex r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )
n <= n + (QuantNbr F) by NAT_1:11;
then A20: n + (- (QuantNbr F)) <= (n + (QuantNbr F)) + (- (QuantNbr F)) by XREAL_1:6;
(QuantNbr r) + (QuantNbr F) <= n by A15, A19, CQC_SIM1:17;
then ((QuantNbr r) + (QuantNbr F)) + (- (QuantNbr F)) <= n + (- (QuantNbr F)) by XREAL_1:6;
hence ex r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) by A12, A20, XXREAL_0:2; :: thesis: verum

end;

A21: now :: thesis: ( ex F being Element of QC-WFF Al st q = G1 '&' F implies ex r, r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) )

given F being Element of QC-WFF Al such that A22: q = G1 '&' F ; :: thesis: ex r, r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )
reconsider F = F as Element of CQC-WFF Al by A22, CQC_LANG:9;
take r = r; :: thesis: ex r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )
n <= n + (QuantNbr F) by NAT_1:11;
then A23: n + (- (QuantNbr F)) <= (n + (QuantNbr F)) + (- (QuantNbr F)) by XREAL_1:6;
(QuantNbr r) + (QuantNbr F) <= n by A15, A22, CQC_SIM1:17;
then ((QuantNbr r) + (QuantNbr F)) + (- (QuantNbr F)) <= n + (- (QuantNbr F)) by XREAL_1:6;
hence ex r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) by A12, A23, XXREAL_0:2; :: thesis: verum

end;

now :: thesis: ( q = 'not' G1 implies ex r, r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) )

assume A24: q = 'not' G1 ; :: thesis: ex r, r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )
take r = r; :: thesis: ex r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n )
QuantNbr r <= n by A15, A24, CQC_SIM1:16;
hence ex r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) by A12; :: thesis: verum

end;

hence ex r being Element of CQC-WFF Al st
( r = L . ((len L) - (k + 1)) & QuantNbr r <= n ) by A14, A13, A21, A18, A16, QC_LANG2:def 19; :: thesis: verum

end;

L . (len L) = p by A2, Def5;
then A25: S₁[ 0 ] by A1;
for k being Nat holds S₁[k] from NAT_1:sch 2(A25, A6);
then ex r being Element of CQC-WFF Al st
( r = L . ((len L) - l) & QuantNbr r <= n ) by A5;
hence ex r being Element of CQC-WFF Al st
( r = L . i & QuantNbr r <= n ) ; :: thesis: verum