let b be Nat; :: thesis: for p, a being Prime st a divides p |^ b holds
a = p
let p, a be Prime; :: thesis: ( a divides p |^ b implies a = p )
assume a divides p |^ b ; :: thesis: a = p
then ( a <> 1 & a divides p ) by Th5, INT_2:def 4;
hence a = p by INT_2:def 4; :: thesis: verum