theorem Th45: :: CALCUL_1:45

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for f being FinSequence of CQC-WFF Al st 1 <= len f & |- f & |- f ^ <*p*> holds
|- (Ant f) ^ <*p*>