for A being QC-alphabet
for F, H being Element of QC-WFF A st F is_subformula_of H holds
Subformulae F c= Subformulae H