:: deftheorem defines BoolePrime MOEBIUS2:def 6 :
for p being Prime holds BoolePrime p = Funcs (((Seg p) /\ SetPrimes),2);