theorem Th88: :: QC_LANG2:88

for A being QC-alphabet
for H being Element of QC-WFF A holds Subformulae ('not' H) = (Subformulae H) \/ {('not' H)}