let C be being_simple_closed_curve Subset of (TOP-REAL 2); :: thesis: for D being Simple_closed_curve holds UBD C meets UBD D
let D be Simple_closed_curve; :: thesis: UBD C meets UBD D
reconsider A = C as bounded Subset of (Euclid 2) by JORDAN2C:11;
consider r1 being Real, x1 being Point of (Euclid 2) such that
0 < r1 and
A1: A c= Ball (x1,r1) by METRIC_6:def 3;
reconsider B = D as bounded Subset of (Euclid 2) by JORDAN2C:11;
consider r2 being Real, x2 being Point of (Euclid 2) such that
0 < r2 and
A2: B c= Ball (x2,r2) by METRIC_6:def 3;
reconsider C9 = (Ball (x1,r1)) ` , D9 = (Ball (x2,r2)) ` as connected Subset of (TOP-REAL 2) by JORDAN1K:37;
consider x3 being Point of (Euclid 2), r3 being Real such that
A3: (Ball (x1,r1)) \/ (Ball (x2,r2)) c= Ball (x3,r3) by WEIERSTR:1;

A4: now :: thesis: not D9 is bounded

assume D9 is bounded ; :: thesis: contradiction
then D9 is bounded Subset of (Euclid 2) by JORDAN2C:11;
hence contradiction by JORDAN1K:8; :: thesis: verum

end;

A5: now :: thesis: not C9 is bounded

assume C9 is bounded ; :: thesis: contradiction
then C9 is bounded Subset of (Euclid 2) by JORDAN2C:11;
hence contradiction by JORDAN1K:8; :: thesis: verum

end;

(Ball (x3,r3)) ` c= ((Ball (x1,r1)) \/ (Ball (x2,r2))) ` by A3, SUBSET_1:12;
then A6: (Ball (x3,r3)) ` c= ((Ball (x1,r1)) `) /\ ((Ball (x2,r2)) `) by XBOOLE_1:53;
then A7: (Ball (x3,r3)) ` c= (Ball (x1,r1)) ` by XBOOLE_1:18;
A8: (Ball (x3,r3)) ` c= (Ball (x2,r2)) ` by A6, XBOOLE_1:18;
(Ball (x2,r2)) ` c= B ` by A2, SUBSET_1:12;
then (Ball (x2,r2)) ` misses B by SUBSET_1:23;
then D9 c= UBD D by A4, JORDAN2C:125;
then A9: (Ball (x3,r3)) ` c= UBD D by A8;
(Ball (x1,r1)) ` c= A ` by A1, SUBSET_1:12;
then (Ball (x1,r1)) ` misses A by SUBSET_1:23;
then C9 c= UBD C by A5, JORDAN2C:125;
then A10: (Ball (x3,r3)) ` c= UBD C by A7;
(Ball (x3,r3)) ` <> {} (Euclid 2) by JORDAN1K:8;
hence UBD C meets UBD D by A10, A9, XBOOLE_1:68; :: thesis: verum