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