:: deftheorem Def21 defines universal QC_LANG1:def 21 :
for A being QC-alphabet
for F being Element of QC-WFF A holds
( F is universal iff ex x being bound_QC-variable of A ex p being Element of QC-WFF A st F = All (x,p) );