:: deftheorem defines perfect NAT_5:def 6 :
for n0 being natural non zero Number holds
( n0 is perfect iff sigma n0 = 2 * n0 );