let p, q be Prime; :: thesis: ( primeindex p = primeindex q implies p = q )
( primenumber (primeindex p) = p & primenumber (primeindex q) = q ) by Def4;
hence ( primeindex p = primeindex q implies p = q ) ; :: thesis: verum