theorem Th48: :: CALCUL_1:48

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