let n be non zero Nat; :: thesis: ( PrimeDivisors n is empty implies n = 1 )
set X = PrimeDivisors n;
assume A1: PrimeDivisors n is empty ; :: thesis: n = 1
assume n <> 1 ; :: thesis: contradiction
then consider p being Prime such that
A2: p divides n by MOEBIUS1:5;
p in PrimeDivisors n by A2;
hence contradiction by A1; :: thesis: verum