let n be Element of 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 6;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in UBD (L~ (Cage C,n)) or x in UBD C )
assume A2: x in UBD (L~ (Cage C,n)) ; :: thesis: x in UBD C
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 6;
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:13;
B is_a_component_of (L~ (Cage C,n)) ` by A6, JORDAN2C:def 4;
then consider B2 being Subset of ((TOP-REAL 2) | ((L~ (Cage C,n)) ` )) such that
A7: B2 = B and
A8: B2 is_a_component_of (TOP-REAL 2) | ((L~ (Cage C,n)) ` ) by CONNSP_1:def 6;
B2 is connected by A8, CONNSP_1:def 5;
then A9: B is connected by A7, CONNSP_1:24;
not B is Bounded by A6, JORDAN2C:def 4;
then A10: not B1 is bounded by JORDAN2C:def 2;
the carrier of ((TOP-REAL 2) | (C ` )) = C ` by PRE_TOPC:29;
then reconsider P1 = Component_of (Down B,(C ` )) as Subset of (TOP-REAL 2) by XBOOLE_1:1;
RightComp (Cage C,n) is_inside_component_of L~ (Cage C,n) by GOBRD14:45;
then A11: ( C c= RightComp (Cage C,n) & B1 misses RightComp (Cage C,n) ) by A6, Th11, JORDAN2C:126;
then B1 misses C by XBOOLE_1:63;
then A12: P1 is_outside_component_of C by A9, A10, JORDAN2C:71;
A13: B1 /\ (RightComp (Cage C,n)) = {} by A11, XBOOLE_0:def 7;
B c= C `

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in B or a in C ` )
assume A14: a in B ; :: thesis: a in C `
then not a in C by A11, A13, XBOOLE_0:def 4;
hence a in C ` by A14, XBOOLE_0:def 5; :: thesis: verum

end;

then Down B,(C ` ) = B by XBOOLE_1:28;
then A15: Down B,(C ` ) c= Component_of (Down B,(C ` )) by A9, CONNSP_3:1, JORDAN2C:15;
not x in C by A3, A5, A11, A13, XBOOLE_0:def 4;
then x in C ` by A3, A5, XBOOLE_0:def 5;
then A16: x in B /\ (C ` ) by A3, A5, XBOOLE_0:def 4;
P1 in { W where W is Subset of (TOP-REAL 2) : W is_outside_component_of C } by A12;
hence x in UBD C by A1, A15, A16, TARSKI:def 4; :: thesis: verum