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