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