let n be Nat; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds UBD (L~ (Cage (C,n))) c= UBD C
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: UBD (L~ (Cage (C,n))) c= UBD C
set f = Cage (C,n);
A1: UBD C = union { B where B is Subset of (TOP-REAL 2) : B is_outside_component_of C } by JORDAN2C:def 5;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in UBD (L~ (Cage (C,n))) or x in UBD C )
A2: UBD (L~ (Cage (C,n))) = union { B where B is Subset of (TOP-REAL 2) : B is_outside_component_of L~ (Cage (C,n)) } by JORDAN2C:def 5;
assume x in UBD (L~ (Cage (C,n))) ; :: thesis: x in UBD C
then consider L being set such that
A3: x in L and
A4: L in { B where B is Subset of (TOP-REAL 2) : B is_outside_component_of L~ (Cage (C,n)) } by A2, TARSKI:def 4;
consider B being Subset of (TOP-REAL 2) such that
A5: L = B and
A6: B is_outside_component_of L~ (Cage (C,n)) by A4;
reconsider B1 = B as Subset of (Euclid 2) by TOPREAL3:8;
A7: B1 misses RightComp (Cage (C,n)) by A6, GOBRD14:35, JORDAN2C:118;
then A8: B1 /\ (RightComp (Cage (C,n))) = {} ;
the carrier of ((TOP-REAL 2) | (C `)) = C ` by PRE_TOPC:8;
then reconsider P1 = Component_of (Down (B,(C `))) as Subset of (TOP-REAL 2) by XBOOLE_1:1;
B is_a_component_of (L~ (Cage (C,n))) ` by A6, JORDAN2C:def 3;
then consider B2 being Subset of ((TOP-REAL 2) | ((L~ (Cage (C,n))) `)) such that
A9: B2 = B and
A10: B2 is a_component by CONNSP_1:def 6;
B2 is connected by A10, CONNSP_1:def 5;
then A11: B is connected by A9, CONNSP_1:23;
A12: C c= RightComp (Cage (C,n)) by Th11;
then not x in C by A3, A5, A8, XBOOLE_0:def 4;
then x in C ` by A3, A5, XBOOLE_0:def 5;
then A13: x in B /\ (C `) by A3, A5, XBOOLE_0:def 4;
not B is bounded by A6, JORDAN2C:def 3;
then A14: not B1 is bounded by JORDAN2C:11;
B1 misses C by A7, Th11, XBOOLE_1:63;
then P1 is_outside_component_of C by A11, A14, JORDAN2C:63;
then A15: P1 in { W where W is Subset of (TOP-REAL 2) : W is_outside_component_of C } ;
B c= C `

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in B or a in C ` )
assume A16: a in B ; :: thesis: a in C `
then not a in C by A12, A8, XBOOLE_0:def 4;
hence a in C ` by A16, XBOOLE_0:def 5; :: thesis: verum

end;

then Down (B,(C `)) = B by XBOOLE_1:28;
then Down (B,(C `)) c= Component_of (Down (B,(C `))) by A11, CONNSP_1:46, CONNSP_3:1;
hence x in UBD C by A1, A13, A15, TARSKI:def 4; :: thesis: verum