let A be QC-alphabet ; :: thesis: for p being Element of QC-WFF A st p is negative holds
len (@ (the_argument_of p)) < len (@ p)
let p be Element of QC-WFF A; :: 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 A such that
A2: p = 'not' q ;
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, Def24; :: thesis: verum