theorem :: QC_LANG2:95

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