theorem Th79: :: QC_LANG2:79

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;