let x, y be odd Element of NAT ; :: thesis: ( x < y iff x + 2 <= y )

hereby :: thesis: ( x + 2 <= y implies x < y )

assume x < y ; :: thesis: x + 2 <= y
then x + 1 <= y by NAT_1:13;
then x + 1 < y by XXREAL_0:1;
then (x + 1) + 1 < y + 1 by XREAL_1:8;
hence x + 2 <= y by NAT_1:13; :: thesis: verum

end;

assume x + 2 <= y ; :: thesis: x < y
then (x + 2) - 2 < y - 0 by XREAL_1:15;
hence x < y ; :: thesis: verum