set P = NatDivisors n;
not 0 in NatDivisors n

proof

assume 0 in NatDivisors n ; :: thesis: contradiction
then ex k being Nat st
( k = 0 & k <> 0 & k divides n ) ;
hence contradiction ; :: thesis: verum

end;

hence ( NatDivisors n is finite & NatDivisors n is with_non-empty_elements ) by MEASURE6:def 2; :: thesis: verum