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