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