theorem :: BINARI_4:21

for j, k, m being Nat st j >= k holds
MajP (m,j) >= MajP (m,k)