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

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

hence
A \/ B is interval
by Th84; :: thesis: verum
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

end;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;

end;

suppose that A8:
x in A
and

A9: y in B ; :: thesis: r in A \/ B

end;

A9: y in B ; :: thesis: r in A \/ B

end;