theorem Th42: :: CALCUL_1:42

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 = All (x,p) & |- f holds
|- (Ant f) ^ <*(p . (x,y))*>