theorem :: NAT_5:39

for n0 being non zero Nat st n0 is even & n0 is perfect holds
ex p being Nat st
( (2 |^ p) -' 1 is prime & n0 = (2 |^ (p -' 1)) * ((2 |^ p) -' 1) )