let n be odd Nat; :: thesis: ( n <= 2 implies n = 1 )
assume A1: n <= 2 ; :: thesis: n = 1
n <> 2 * 1 ;
then n < 1 + 1 by A1, XXREAL_0:1;
then A2: n <= 1 by NAT_1:13;
n >= 1 by ABIAN:12;
hence n = 1 by A2, XXREAL_0:1; :: thesis: verum