theorem :: NUMBER18:23

for m being Nat st m >= 1 & Mersenne m is Prime holds
( card (PrimeDivisors (Mersenne m)) = 1 & card (PrimeDivisors ((Mersenne m) + 1)) = 1 )