let p be Element of MC-wff ; :: thesis: p => (p '&' p) in IPC-Taut
A1: (p => (p => (p '&' p))) => (p => (p '&' p)) in IPC-Taut by Th30;
p => (p => (p '&' p)) in IPC-Taut by Def14;
hence p => (p '&' p) in IPC-Taut by A1, Def14; :: thesis: verum