theorem Th28: :: LUKASI_1:28

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