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