theorem Th22: :: BINARI_4:22

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