:: deftheorem defines SetPrimes MOEBIUS3:def 4 :
for n being Nat holds SetPrimes n = SetPrimes /\ (Seg n);