let A, B be ext-real-membered set ; :: thesis: ( A is connected & B is left_end & B is connected & sup A = inf B implies A \/ B is connected )
assume that
Z1: A is connected and
Z2: ( B is left_end & B is connected ) and
Z3: sup A = inf B ; :: thesis: A \/ B is connected
set z = inf B;
G2: inf B in B by Z2, Def5;
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
Z3': x in A \/ B and
Z4: y in A \/ B and
Z5: x < r and
Z6: 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 Z3', Z4, XBOOLE_0:def 3;

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

then r in A by Z1, Z5, Z6, Th84;
hence r in A \/ B by XBOOLE_0:def 3; :: thesis: verum

end;

suppose that S1: x in A and
S2: 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 Z1, S1, Z5, Th85, Z3;
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 Z2, S2, G2, Z6, Th84;
hence r in A \/ B by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

suppose that S1: x in B and
S2: y in A ; :: thesis: r in A \/ B

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

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

y <= inf B by S2, Z3, Th3B;
hence r in A \/ B by S, Z6, XXREAL_0:2; :: thesis: verum

end;

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

then r in B by Z2, S1, G2, Z5, 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 Z2, Z5, Z6, Th84;
hence r in A \/ B by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

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