theorem Th8: :: LUKASI_1:8

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