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