theorem :: QC_LANG1:7

for A being QC-alphabet holds QC-WFF A is A -closed by Def11;