theorem :: LUKASI_1:18

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