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:10; :: thesis: verum