for A being QC-alphabet
for F, G, H being Element of QC-WFF A st F is_subformula_of G & G is_subformula_of H holds
F is_subformula_of H