theorem Th10: :: LUKASI_1:10

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