let n be natural number ; :: 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 not n is square-containing by Def2;
hence Moebius n <> 0 ; :: thesis: verum

end;

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