let A, B be ext-real-membered set ; :: thesis:
assume that
A1: ( A is right_end & A is interval ) and
A2: B is interval and
A3: sup A = inf B ; :: thesis:
set z = inf B;
A4: inf B in A by A1, A3;
for x, y, r being ExtReal st x in A \/ B & y in A \/ B & x < r & r < y holds
r in A \/ B

proof

let x, y, r be ExtReal; :: thesis:
assume that
A5: x in A \/ B and
A6: y in A \/ B and
A7: x < r and
A8: r < y ; :: thesis:

per cases by A5, A6, XBOOLE_0:def 3;

suppose ( x in A & y in A ) ; :: thesis:

then r in A by A1, A7, A8, Th80;
hence r in A \/ B by XBOOLE_0:def 3; :: thesis:

end;

suppose that A9: x in A and
A10: y in B ; :: thesis:

per cases ;

suppose r <= inf B ; :: thesis:

then r in A by A1, A4, A7, A9, Th80;
hence r in A \/ B by XBOOLE_0:def 3; :: thesis:

end;

suppose inf B < r ; :: thesis:

then r in B by A2, A8, A10, Th82;
hence r in A \/ B by XBOOLE_0:def 3; :: thesis:

end;

end;

end;

suppose that A11: x in B and
A12: y in A ; :: thesis:

per cases ;

suppose inf B <= r ; :: thesis:

then r in A by A1, A4, A8, A12, Th80;
hence r in A \/ B by XBOOLE_0:def 3; :: thesis:

end;

suppose A13: r < inf B ; :: thesis:

inf B <= x by A11, Th3;
hence r in A \/ B by A7, A13, XXREAL_0:2; :: thesis:

end;

end;

end;

suppose ( x in B & y in B ) ; :: thesis:

then r in B by A2, A7, A8, Th80;
hence r in A \/ B by XBOOLE_0:def 3; :: thesis:

end;

end;

end;

hence A \/ B is interval by Th84; :: thesis: