theorem :: QC_LANG3:63

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