let j, l, m be Nat; ( l >= m implies MajP (l,j) >= MajP (m,j) )
assume A1:
l >= m
; MajP (l,j) >= MajP (m,j)
A2:
2 to_power (MajP (l,j)) >= j
by Def1;
MajP (l,j) >= l
by Def1;
then
MajP (l,j) >= m
by A1, XXREAL_0:2;
hence
MajP (l,j) >= MajP (m,j)
by A2, Def1; verum