theorem :: NAT_5:38

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