let m be Nat; :: thesis: ( m >= 1 implies m + 2 > 1 )
assume A1: m >= 1 ; :: thesis: m + 2 > 1
m + 2 > m by XREAL_1:31;
hence m + 2 > 1 by A1, XXREAL_0:2; :: thesis: verum