theorem :: BINARI_4:25

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