:: deftheorem defines All QC_LANG2:def 6 :
for A being QC-alphabet
for x, y being bound_QC-variable of A
for p being Element of QC-WFF A holds All (x,y,p) = All (x,(All (y,p)));