theorem :: QC_LANG2:94

for A being QC-alphabet
for H being Element of QC-WFF A holds
( ( H = VERUM A or H is atomic ) iff Subformulae H = {H} )