theorem :: LUKASI_1:51
for A being QC-alphabet
for p, q, r being Element of CQC-WFF A st p => q is valid holds
(r => p) => (r => q) is valid