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