let s, q, p be Element of CQC-WFF ; :: thesis: ( s => (q => p) in TAUT implies q => (s => p) in TAUT )
assume A1: s => (q => p) in TAUT ; :: thesis: q => (s => p) in TAUT
(s => (q => p)) => (q => (s => p)) in TAUT by Th8;
hence q => (s => p) in TAUT by A1, CQC_THE1:46; :: thesis: verum