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