for A being QC-alphabet
for p being Element of QC-WFF A st p is negative holds
len (@ (the_argument_of p)) < len (@ p)