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 ( n <= 1 & n >= 1 ) by HEYTING3:1, NAT_1:13;
hence n = 1 by XXREAL_0:1; :: thesis: verum