theorem Th49: :: CALCUL_1:49

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