let m be Nat; :: thesis: ( m > 0 implies m * 2 >= m + 1 )
assume m > 0 ; :: thesis: m * 2 >= m + 1
then A1: m >= 0 + 1 by INT_1:7;
m * 2 = m + m ;
hence m * 2 >= m + 1 by A1, XREAL_1:6; :: thesis: verum