:: deftheorem defines Fixed QC_LANG3:def 6 :
for A being QC-alphabet
for p being Element of QC-WFF A holds Fixed p = Vars (p,(fixed_QC-variables A));