let j, m be Nat; :: thesis: ( j <= 2 to_power m implies MajP (m,j) = m )
A1: for k being Nat st 2 to_power k >= j & k >= m holds
k >= m ;
assume j <= 2 to_power m ; :: thesis: MajP (m,j) = m
hence MajP (m,j) = m by A1, Def1; :: thesis: verum