Understanding intersect operator

As discussed in thread , the consequent being a degenerate sequence is illegal as per LRM.
Tool seem to interpret the consequent in context of intersect operator and the assertion fails once the LHS sequence ends