let p, q be Element of HP-WFF ; :: thesis: q => ((q => p) => p) in HP_TAUT
A1: ((q => p) => (q => p)) => (q => ((q => p) => p)) in HP_TAUT by Th26;
(q => p) => (q => p) in HP_TAUT by Th14;
hence q => ((q => p) => p) in HP_TAUT by A1, Def10; :: thesis: verum