let n be Nat; :: thesis: for m being Nat st n <= m & m <= n + 2 & not m = n & not m = n + 1 holds
m = n + 2
let m be Nat; :: thesis: ( n <= m & m <= n + 2 & not m = n & not m = n + 1 implies m = n + 2 )
assume that
A1: n <= m and
A2: m <= n + 2 ; :: thesis: ( m = n or m = n + 1 or m = n + 2 )

per cases ( m <= n + 1 or m > n + 1 ) ;

suppose m <= n + 1 ; :: thesis: ( m = n or m = n + 1 or m = n + 2 )

hence ( m = n or m = n + 1 or m = n + 2 ) by A1, Th9; :: thesis: verum

end;

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

then ( m = n + 1 or m = (n + 1) + 1 ) by A2, Th9;
hence ( m = n or m = n + 1 or m = n + 2 ) ; :: thesis: verum

end;

end;