theorem Th15: :: LUKASI_1:15

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