theorem :: CALCUL_1:68

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for f being FinSequence of CQC-WFF Al holds
( |- f ^ <*(All (x,p))*> iff |- f ^ <*('not' (Ex (x,('not' p))))*> )