let m, n be Nat; :: thesis: ( primenumber m = primenumber n implies m = n )
assume A1: primenumber m = primenumber n ; :: thesis: m = n
assume m <> n ; :: thesis: contradiction
then ( m < n or m > n ) by XXREAL_0:1;
hence contradiction by A1, MOEBIUS2:21; :: thesis: verum