theorem :: LUKASI_1:54

for A being QC-alphabet
for p, q being Element of CQC-WFF A holds
( ('not' ('not' p)) => q is valid iff p => q is valid )