:: deftheorem Def11 defines QC-WFF QC_LANG1:def 11 :
for A being QC-alphabet
for b₂ being non empty set holds
( b₂ = QC-WFF A iff ( b₂ is A -closed & ( for D being non empty set st D is A -closed holds
b₂ c= D ) ) );