for Al being QC-alphabet holds [:(QC-WFF Al),(vSUB Al):] c= dom (QSub Al)