theorem :: LUKASI_1:47

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