let n, m be odd Integer; :: thesis: ( m < n implies m + 2 <= n )
assume m < n ; :: thesis: m + 2 <= n
then m + 1 <= n by INT_1:7;
then m + 1 < n by XXREAL_0:1;
then (m + 1) + 1 <= n by INT_1:7;
hence m + 2 <= n ; :: thesis: verum