for A being QC-alphabet
for H being Element of QC-WFF A holds
( H is_subformula_of FALSUM A iff ( H = FALSUM A or H = VERUM A ) )