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