theorem Th38: :: CALCUL_1:38

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