let n be Element of NAT ; :: thesis: ( 1 <= n & n <= 2 & not n = 1 implies n = 2 )
assume that
A1: 1 <= n and
A2: n <= 2 ; :: thesis: ( n = 1 or n = 2 )

per cases ( n = 1 or n > 1 ) by A1, XXREAL_0:1;

suppose n = 1 ; :: thesis: ( n = 1 or n = 2 )

hence ( n = 1 or n = 2 ) ; :: thesis: verum

end;

suppose n > 1 ; :: thesis: ( n = 1 or n = 2 )

then n >= 1 + 1 by NAT_1:13;
hence ( n = 1 or n = 2 ) by A2, XXREAL_0:1; :: thesis: verum

end;

end;