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