for n being Nat holds
( n in SCNAT iff Moebius n <> 0 )