for p being Nat st p > 1 & Mersenne p is Prime holds
p is Prime by Th28;