theorem :: QC_LANG2:87

for A being QC-alphabet holds Subformulae (FALSUM A) = {(VERUM A),(FALSUM A)}