theorem Th54: :: CALCUL_1:55

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