PR# 15079 First precondition of {ARRAY}.subarray appears to be wrong

The first precondition of {ARRAY}.subarray appears to be wrong.

The third precondition allows for an array of size zero where the end_position < start_position.

However, the first precondition asserts that the index must be valid i.e. between lower and upper, which will be false for an array of size zero. 

Thus it does not allow subarrays of size zero (which it should).

==
subarray (start_pos, end_pos: INTEGER_32): ARRAY [G]
			-- Array made of items of current array within
			-- bounds `start_pos' and `end_pos'.
		require
			valid_start_pos: valid_index (start_pos)
			valid_end_pos: end_pos <= upper
			valid_bounds: (start_pos <= end_pos) or (start_pos = end_pos + 1)
		do
			create Result.make (start_pos, end_pos)
			if start_pos <= end_pos then
				Result.subcopy (Current, start_pos, end_pos, start_pos)
			end
		ensure
			lower: Result.lower = start_pos
			upper: Result.upper = end_pos
		end

See above.

Fixed in rev#101778 of EiffelStudio 18.07 release.