theorem :: QC_LANG2:97

for A being QC-alphabet
for H being Element of QC-WFF A st H is universal holds
Subformulae H = (Subformulae (the_scope_of H)) \/ {H}