let q, s, p, r be Element of CQC-WFF ; :: thesis: ((q => (s => p)) => r) => ((s => (q => p)) => r) in TAUT
( (s => (q => p)) => (q => (s => p)) in TAUT & ((s => (q => p)) => (q => (s => p))) => (((q => (s => p)) => r) => ((s => (q => p)) => r)) in TAUT ) by Th1, Th8;
hence ((q => (s => p)) => r) => ((s => (q => p)) => r) in TAUT by CQC_THE1:82; :: thesis: verum