theorem :: MOEBIUS3:57

for n being non zero Nat
for x being object st x in bool (SetPrimes n) holds
x is finite Subset of SetPrimes