let n be Element of NAT ; :: thesis: for A being Subset of (TOP-REAL n) holds BDD A misses UBD A
let A be Subset of (TOP-REAL n); :: thesis: BDD A misses UBD A
assume A1: (BDD A) /\ (UBD A) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction
consider x being Element of (BDD A) /\ (UBD A);
x in union { B where B is Subset of (TOP-REAL n) : B is_inside_component_of A } by A1, XBOOLE_0:def 4;
then consider y being set such that
A2: ( x in y & y in { B where B is Subset of (TOP-REAL n) : B is_inside_component_of A } ) by TARSKI:def 4;
consider B being Subset of (TOP-REAL n) such that
A3: ( y = B & B is_inside_component_of A ) by A2;
consider C being Subset of ((TOP-REAL n) | (A ` )) such that
A4: ( C = B & C is_a_component_of (TOP-REAL n) | (A ` ) & C is bounded Subset of (Euclid n) ) by A3, Th17;
x in union { B2 where B2 is Subset of (TOP-REAL n) : B2 is_outside_component_of A } by A1, XBOOLE_0:def 4;
then consider y2 being set such that
A5: ( x in y2 & y2 in { B2 where B2 is Subset of (TOP-REAL n) : B2 is_outside_component_of A } ) by TARSKI:def 4;
consider B2 being Subset of (TOP-REAL n) such that
A6: ( y2 = B2 & B2 is_outside_component_of A ) by A5;
consider C2 being Subset of ((TOP-REAL n) | (A ` )) such that
A7: ( C2 = B2 & C2 is_a_component_of (TOP-REAL n) | (A ` ) & C2 is not bounded Subset of (Euclid n) ) by A6, Th18;
C /\ C2 <> {} ((TOP-REAL n) | (A ` )) by A2, A3, A4, A5, A6, A7, XBOOLE_0:def 4;
then C meets C2 by XBOOLE_0:def 7;
hence contradiction by A4, A7, CONNSP_1:37; :: thesis: verum