let n be Nat; :: thesis: ( n in SCNAT iff Moebius n <> 0 )

hereby :: thesis: ( Moebius n <> 0 implies n in SCNAT )

assume n in SCNAT ; :: thesis: Moebius n <> 0
then n is square-free by Def2;
hence Moebius n <> 0 ; :: thesis: verum

end;

assume Moebius n <> 0 ; :: thesis: n in SCNAT
then n is square-free by Def3;
hence n in SCNAT by Def2; :: thesis: verum