for j, m being Nat st j > 2 to_power m holds
MajP (m,j) > m