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 )
consider L being PATH of q,p;
set m = len L;
assume A1: ( QuantNbr p = n & q is_subformula_of p ) ; :: thesis: QuantNbr q <= n
then ( 1 <= len L & L . 1 = q & L . (len L) = p & ( for i being Element of NAT st 1 <= i & i < len L holds
ex G1, H1 being Element of QC-WFF st
( L . i = G1 & L . (i + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) ) by Def6;
then consider r being Element of CQC-WFF such that
A2: ( r = L . 1 & QuantNbr r <= n ) by A1, Th29;
thus QuantNbr q <= n by A1, A2, Def6; :: thesis: verum