let a be Integer; :: thesis: for b being square-free Nat holds a gcd b is square-free
let b be square-free Nat; :: thesis: a gcd b is square-free
assume not a gcd b is square-free ; :: thesis: contradiction
then consider p being prime Nat such that
A1: p |^ 2 divides a gcd b ;
a gcd b divides b by INT_2:def 2;
hence contradiction by A1, INT_2:9, MOEBIUS1:def 1; :: thesis: verum