set P = NatDivisors n;
A1: not 0 in NatDivisors n

proof

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

end;

NatDivisors n c= Seg n by Th40;
hence ( NatDivisors n is finite & NatDivisors n is with_non-empty_elements ) by A1, MEASURE6:def 2; :: thesis: verum