theorem :: QC_LANG3:53

for A being QC-alphabet holds Free (VERUM A) = {} by Lm2;