let n be Element of NAT ; :: thesis: for p, q being Element of CQC-WFF st QuantNbr p = n & q is_subformula_of p holds
QuantNbr q <= n
let p, q be Element of CQC-WFF ; :: 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, Def6;
then ex r being Element of CQC-WFF st
( r = the PATH of q,p . 1 & QuantNbr r <= n ) by A1, A2, Th29;
hence QuantNbr q <= n by A2, Def6; :: thesis: verum