theorem Th3: :: QC_LANG3:3

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