theorem Th16: :: PROCAL_1:16

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