let n be odd Nat; :: thesis: ( not n <= 8 or n = 1 or n = 3 or n = 5 or n = 7 )
assume A1: n <= 8 ; :: thesis: ( n = 1 or n = 3 or n = 5 or n = 7 )
n <> 2 * 4 ;
then n < 7 + 1 by A1, XXREAL_0:1;
then A2: n <= 7 by NAT_1:13;

per cases ( n = 7 or n < 6 + 1 ) by A2, XXREAL_0:1;

suppose n = 7 ; :: thesis: ( n = 1 or n = 3 or n = 5 or n = 7 )

hence ( n = 1 or n = 3 or n = 5 or n = 7 ) ; :: thesis: verum

end;

suppose n < 6 + 1 ; :: thesis: ( n = 1 or n = 3 or n = 5 or n = 7 )

then n <= 6 by NAT_1:13;
hence ( n = 1 or n = 3 or n = 5 or n = 7 ) by Th8; :: thesis: verum

end;

end;