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