theorem :: QC_LANG2:76

for A being QC-alphabet
for H being Element of QC-WFF A st H is negative holds
the_argument_of H is_proper_subformula_of H