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