for A being QC-alphabet
for H being Element of QC-WFF A holds
( H is_subformula_of VERUM A iff H = VERUM A ) by Def21, Th64;