theorem :: MOEBIUS2:20

for m, n being Nat holds
( SetPrimenumber m c= SetPrimenumber n or SetPrimenumber n c= SetPrimenumber m )