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