let p be Element of QC-WFF ; :: thesis: ( p is universal implies len (@ (the_scope_of p)) < len (@ p) )
assume A1: p is universal ; :: thesis: len (@ (the_scope_of p)) < len (@ p)
then consider x being bound_QC-variable, q being Element of QC-WFF such that
A2: p = All (x,q) by Def20;
(len (@ q)) + (len <*x*>) = len (<*x*> ^ (@ q)) by FINSEQ_1:22;
then A3: len (@ q) <= len (<*x*> ^ (@ q)) by NAT_1:11;
p = <*[3,0]*> ^ (<*x*> ^ (@ q)) by A2, FINSEQ_1:32;
then len (@ p) = (len <*[3,0]*>) + (len (<*x*> ^ (@ q))) by FINSEQ_1:22
.= (len (<*x*> ^ (@ q))) + 1 by FINSEQ_1:40 ;
then len (@ q) < len (@ p) by A3, NAT_1:13;
hence len (@ (the_scope_of p)) < len (@ p) by A1, A2, Def27; :: thesis: verum