let p be Element of QC-WFF ; :: thesis: ( p is negative implies len (@ (the_argument_of p)) < len (@ p) )
assume A1: p is negative ; :: thesis: len (@ (the_argument_of p)) < len (@ p)
then consider q being Element of QC-WFF such that
A2: p = 'not' q by Def18;
len (@ p) = (len <*[1,0]*>) + (len (@ q)) by A2, FINSEQ_1:22
.= (len (@ q)) + 1 by FINSEQ_1:40 ;
then len (@ q) < len (@ p) by NAT_1:13;
hence len (@ (the_argument_of p)) < len (@ p) by A1, A2, Def23; :: thesis: verum