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