:: deftheorem Def5 defines Proth NAT_6:def 5 :
for p being Nat holds
( p is Proth iff ex k being odd Nat ex n being positive Nat st
( 2 |^ n > k & p = (k * (2 |^ n)) + 1 ) );