let A, B be ext-real-membered set ; :: thesis: ( A is interval & B is interval & A meets B implies A \/ B is interval )

assume that

A1: A is interval and

A2: B is interval ; :: thesis: ( not A meets B or A \/ B is interval )

given z being ExtReal such that A3: z in A and

A4: z in B ; :: according to MEMBERED:def 20 :: thesis: A \/ B is interval

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 interval ; :: thesis: ( not A meets B or A \/ B is interval )

given z being ExtReal such that A3: z in A and

A4: z in B ; :: according to MEMBERED:def 20 :: thesis: A \/ B is interval

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 Th88; :: 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

A5: x in A \/ B and

A6: y in A \/ B and

A7: x <= r and

A8: r <= y ; :: thesis: r in A \/ B

end;assume that

A5: x in A \/ B and

A6: y in A \/ B and

A7: x <= r and

A8: 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 A5, A6, XBOOLE_0:def 3;

end;

suppose that A9:
x in A
and

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

end;

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

end;