theorem :: QC_LANG3:35

for A being QC-alphabet
for V being non empty Subset of (QC-variables A) holds Vars ((VERUM A),V) = {} by Lm2;