let A, B be ext-real-membered set ; :: thesis: ( A is connected & B is connected & A meets B implies A \/ B is connected )
assume that
A1: A is connected and
A2: B is connected ; :: thesis: ( not A meets B or A \/ B is connected )
given z being ext-real number such that A3: z in A and
A4: z in B ; :: according to MEMBERED:def 20 :: thesis: A \/ B is connected
for x, y, r being ext-real number st x in A \/ B & y in A \/ B & x <= r & r <= y holds
r in A \/ B

proof

let x, y, r be ext-real number ; :: 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

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;

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

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

end;

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

per cases ( r <= z or z <= r ) ;

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

then r in A by A1, A3, A7, A9, Th84;
hence r in A \/ B by XBOOLE_0:def 3; :: thesis: verum

end;

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

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

end;

end;

end;

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

per cases ( z <= r or r <= z ) ;

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

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

end;

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

then r in B by A2, A4, A7, A11, Th84;
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, A7, A8, Th84;
hence r in A \/ B by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence A \/ B is connected by Th92; :: thesis: verum