let n be odd Nat; :: thesis: ( 1 <> n implies ex m being odd Nat st m + 2 = n )
A1: 1 <= n by ABIAN:12;
assume 1 <> n ; :: thesis: ex m being odd Nat st m + 2 = n
then (2 * 0) + 1 < n by A1, XXREAL_0:1;
then 1 + 2 <= n by Th4;
then (1 + 2) - 2 <= n - 2 by XREAL_1:9;
then n - (2 * 1) in NAT by INT_1:3;
then reconsider m = n - 2 as odd Nat ;
take m ; :: thesis: m + 2 = n
thus m + 2 = n ; :: thesis: verum