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:def 2;
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 10;
reconsider B = D as bounded Subset of (Euclid 2) by JORDAN2C:def 2;
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 10;
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

assume D9 is Bounded ; :: thesis: contradiction
then D9 is bounded Subset of (Euclid 2) by JORDAN2C:def 2;
hence contradiction by JORDAN1K:8, TBSP_1:19; :: thesis: verum

end;

A5: now

assume C9 is Bounded ; :: thesis: contradiction
then C9 is bounded Subset of (Euclid 2) by JORDAN2C:def 2;
hence contradiction by JORDAN1K:8, TBSP_1:19; :: thesis: verum

end;

(Ball x3,r3) ` c= ((Ball x1,r1) \/ (Ball x2,r2)) ` by A3, SUBSET_1:31;
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:31;
then (Ball x2,r2) ` misses B by SUBSET_1:43;
then D9 c= UBD D by A4, JORDAN2C:133;
then A9: (Ball x3,r3) ` c= UBD D by A8, XBOOLE_1:1;
(Ball x1,r1) ` c= A ` by A1, SUBSET_1:31;
then (Ball x1,r1) ` misses A by SUBSET_1:43;
then C9 c= UBD C by A5, JORDAN2C:133;
then A10: (Ball x3,r3) ` c= UBD C by A7, XBOOLE_1:1;
(Ball x3,r3) ` <> {} (Euclid 2) by JORDAN1K:8, TBSP_1:19;
hence UBD C meets UBD D by A10, A9, XBOOLE_1:68; :: thesis: verum