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;
p = <*[3,0 ]*> ^ (<*x*> ^ (@ q)) by A2, FINSEQ_1:45;
then A3: len (@ p) = (len <*[3,0 ]*>) + (len (<*x*> ^ (@ q))) by FINSEQ_1:35
.= (len (<*x*> ^ (@ q))) + 1 by FINSEQ_1:57 ;
(len (@ q)) + (len <*x*>) = len (<*x*> ^ (@ q)) by FINSEQ_1:35;
then len (@ q) <= len (<*x*> ^ (@ q)) by NAT_1:11;
then len (@ q) < len (@ p) by A3, NAT_1:13;
hence len (@ (the_scope_of p)) < len (@ p) by A1, A2, Def27; :: thesis: verum