theorem Th85: :: QC_LANG2:85

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