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

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