let l, m, j 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