let n be Nat; for A being Subset of (TOP-REAL n) holds BDD A misses UBD A
let A be Subset of (TOP-REAL n); BDD A misses UBD A
set x = the Element of (BDD A) /\ (UBD A);
assume A1:
(BDD A) /\ (UBD A) <> {}
; XBOOLE_0:def 7 contradiction
then
the Element of (BDD A) /\ (UBD A) in union { B where B is Subset of (TOP-REAL n) : B is_inside_component_of A }
by XBOOLE_0:def 4;
then consider y being set such that
A2:
the Element of (BDD A) /\ (UBD A) in y
and
A3:
y in { B where B is Subset of (TOP-REAL n) : B is_inside_component_of A }
by TARSKI:def 4;
the Element of (BDD A) /\ (UBD A) 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
A4:
the Element of (BDD A) /\ (UBD A) in y2
and
A5:
y2 in { B2 where B2 is Subset of (TOP-REAL n) : B2 is_outside_component_of A }
by TARSKI:def 4;
consider B being Subset of (TOP-REAL n) such that
A6:
y = B
and
A7:
B is_inside_component_of A
by A3;
consider B2 being Subset of (TOP-REAL n) such that
A8:
y2 = B2
and
A9:
B2 is_outside_component_of A
by A5;
consider C being Subset of ((TOP-REAL n) | (A `)) such that
A10:
C = B
and
A11:
( C is a_component & C is bounded Subset of (Euclid n) )
by A7, Th7;
consider C2 being Subset of ((TOP-REAL n) | (A `)) such that
A12:
C2 = B2
and
A13:
( C2 is a_component & C2 is not bounded Subset of (Euclid n) )
by A9, Th8;
C /\ C2 <> {} ((TOP-REAL n) | (A `))
by A2, A6, A10, A4, A8, A12, XBOOLE_0:def 4;
then
C meets C2
;
hence
contradiction
by A11, A13, CONNSP_1:35; verum