theorem :: MOEBIUS3:35

for m, n being Nat st m <= n holds
SetPrimes m c= SetPrimes n by XBOOLE_1:26, FINSEQ_1:5;