let Al be QC-alphabet ; for n being Nat
for p, q being Element of CQC-WFF Al st QuantNbr p = n & q is_subformula_of p holds
QuantNbr q <= n
let n be Nat; for p, q being Element of CQC-WFF Al st QuantNbr p = n & q is_subformula_of p holds
QuantNbr q <= n
let p, q be Element of CQC-WFF Al; ( QuantNbr p = n & q is_subformula_of p implies QuantNbr q <= n )
set L = the PATH of q,p;
set m = len the PATH of q,p;
assume that
A1:
QuantNbr p = n
and
A2:
q is_subformula_of p
; QuantNbr q <= n
1 <= len the PATH of q,p
by A2, Def5;
then
ex r being Element of CQC-WFF Al st
( r = the PATH of q,p . 1 & QuantNbr r <= n )
by A1, A2, Th29;
hence
QuantNbr q <= n
by A2, Def5; verum