for A being QC-alphabet
for F, G being Element of QC-WFF A st F is_subformula_of G holds
len (@ F) <= len (@ G)