let n be natural number ; :: thesis: ( not n is square-containing implies Moebius n <> 0 )
assume not n is square-containing ; :: thesis: Moebius n <> 0
then consider n' being non zero natural number such that
A1: ( n' = n & Moebius n = (- 1) |^ (card (support (ppf n'))) ) by Def3;
thus Moebius n <> 0 by A1, CARD_4:51; :: thesis: verum