theorem Th19: :: CALCUL_1:19

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 & 'not' p = Suc (Ant f) & 'not' (Suc f) = Suc g & Ant f |= Suc f & Ant g |= Suc g holds
Ant (Ant f) |= p