let A, B be ext-real-membered set ; :: thesis: ( A is interval & B is left_end & B is interval & sup A = inf B implies A \/ B is interval )
assume that
A1: A is interval and
A2: ( B is left_end & B is interval ) and
A3: sup A = inf B ; :: thesis: A \/ B is interval
set z = inf B;
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: ( x in A \/ B & y in A \/ B & x < r & r < y implies r in A \/ B )
assume that
A4: x in A \/ B and
A5: y in A \/ B and
A6: x < r and
A7: r < y ; :: thesis: r in A \/ B

per cases ( ( x in A & y in A ) or ( x in A & y in B ) or ( x in B & y in A ) or ( x in B & y in B ) ) by A4, A5, XBOOLE_0:def 3;

suppose ( x in A & y in A ) ; :: thesis: r in A \/ B

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

end;

suppose that A8: x in A and
A9: y in B ; :: thesis: r in A \/ B

per cases ( r < inf B or inf B <= r ) ;

suppose r < inf B ; :: thesis: r in A \/ B

then r in A by A1, A3, A6, A8, Th81;
hence r in A \/ B by XBOOLE_0:def 3; :: thesis: verum

end;

suppose inf B <= r ; :: thesis: r in A \/ B

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

end;

end;

end;

suppose that A10: x in B and
A11: y in A ; :: thesis: r in A \/ B

per cases ( inf B < r or r <= inf B ) ;

suppose A12: inf B < r ; :: thesis: r in A \/ B

y <= inf B by A3, A11, Th4;
hence r in A \/ B by A7, A12, XXREAL_0:2; :: thesis: verum

end;

suppose r <= inf B ; :: thesis: r in A \/ B

then r in B by A2, A6, A10, Th80;
hence r in A \/ B by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

suppose ( x in B & y in B ) ; :: thesis: r in A \/ B

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

end;

end;

end;

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