:: deftheorem Def5 defines QC-correct AOFA_L00:def 5 :
for X being set
for L being QCLangSignature over X holds
( L is QC-correct iff ( the quant-sort of L = {1,2} & the quantifiers of L is one-to-one & rng the quantifiers of L misses rng the connectives of L & ( for q, x being object st q in the quant-sort of L & x in X holds
the quantifiers of L . (q,x) is_of_type <* the formula-sort of L*>, the formula-sort of L ) ) );