theorem Th22: :: SUBSTUT1:22

for A being QC-alphabet
for S being Element of QC-Sub-WFF A st S is Sub_negative holds
len (@ ((Sub_the_argument_of S) `1)) < len (@ (S `1))