let Al be QC-alphabet ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum