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

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