theorem Th43: :: CALCUL_1:43

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x, y being bound_QC-variable of Al
for f being FinSequence of CQC-WFF Al st Suc f = p . (x,y) & not y in still_not-bound_in (Ant f) & not y in still_not-bound_in (All (x,p)) & |- f holds
|- (Ant f) ^ <*(All (x,p))*>