theorem Th45: :: CQC_THE3:45

for A being QC-alphabet
for p, q being Element of CQC-WFF A st p is closed & 'not' p |- 'not' q holds
q |- p