theorem Th40: :: CALCUL_1:40

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