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