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