let j, l, m be Nat; :: thesis: ( l >= m implies MajP (l,j) >= MajP (m,j) )
assume A1: l >= m ; :: thesis: 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; :: thesis: verum