theorem :: MOEBIUS3:58

for n being non zero Nat
for x being object st x in [:(bool (SetPrimes n)),(Seg n):] holds
x `1 is finite Subset of SetPrimes