theorem Th25: :: LUKASI_1:25

for A being QC-alphabet
for p being Element of CQC-WFF A holds ('not' ('not' p)) => p in TAUT A