let n, m be Element of NAT ; :: thesis: ( n <= m & m <= n + 4 & not m = n & not m = n + 1 & not m = n + 2 & not m = n + 3 implies m = n + 4 )
assume A1: ( n <= m & m <= n + 4 ) ; :: thesis: ( m = n or m = n + 1 or m = n + 2 or m = n + 3 or m = n + 4 )

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

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

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

end;

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

then ( m = n + 3 or m = (n + 3) + 1 ) by A1, NAT_1:9;
hence ( m = n or m = n + 1 or m = n + 2 or m = n + 3 or m = n + 4 ) ; :: thesis: verum

end;

end;