let A be Subset of (TOP-REAL 2); :: thesis: ( A is bounded & A is Jordan implies BDD A is_inside_component_of A )
assume that
A1: A is bounded and
A2: A is Jordan ; :: thesis: BDD A is_inside_component_of A
reconsider D = A ` as non empty Subset of (TOP-REAL 2) by A2, JORDAN1:def 2;
consider A1, A2 being Subset of (TOP-REAL 2) such that
A3: A ` = A1 \/ A2 and
A4: A1 misses A2 and
(Cl A1) \ A1 = (Cl A2) \ A2 and
A5: for C1, C2 being Subset of ((TOP-REAL 2) | (A `)) st C1 = A1 & C2 = A2 holds
( C1 is a_component & C2 is a_component ) by A2, JORDAN1:def 2;
A6: UBD A is_outside_component_of A by A1, Th53;
then UBD A is_a_component_of A ` ;
then consider B1 being Subset of ((TOP-REAL 2) | (A `)) such that
A7: B1 = UBD A and
A8: B1 is a_component by CONNSP_1:def 6;
A9: Down (A1,(A `)) = A1 by A3, XBOOLE_1:21;
A10: Down (A2,(A `)) = A2 by A3, XBOOLE_1:21;
then A11: Down (A2,(A `)) is a_component by A5, A9;
then A12: A2 is_a_component_of A ` by A10, CONNSP_1:def 6;
A13: not (TOP-REAL 2) | D is empty ;
A14: Down (A1,(A `)) is a_component by A5, A9, A10;
then A15: A1 is_a_component_of A ` by A9, CONNSP_1:def 6;

per cases ( B1 = A1 or B1 misses Down (A1,(A `)) ) by A9, A14, A8, CONNSP_1:35;

suppose A16: B1 = A1 ; :: thesis: BDD A is_inside_component_of A

A17: now :: thesis: BDD A c= A2

assume not BDD A c= A2 ; :: thesis: contradiction
then consider x being object such that
A18: x in BDD A and
A19: not x in A2 ;
consider y being set such that
A20: x in y and
A21: y in { B3 where B3 is Subset of (TOP-REAL 2) : B3 is_inside_component_of A } by A18, TARSKI:def 4;
consider B3 being Subset of (TOP-REAL 2) such that
A22: y = B3 and
A23: B3 is_inside_component_of A by A21;
A24: B3 is_a_component_of A ` by A23;
then consider B4 being Subset of ((TOP-REAL 2) | (A `)) such that
A25: B4 = B3 and
A26: B4 is a_component by CONNSP_1:def 6;
A27: B3 <> {} ((TOP-REAL 2) | (A `)) by A13, A25, A26, CONNSP_1:32;
B4 <> Down (A1,(A `)) by A9, A7, A16, A23, A25, A6;
then A28: B3 misses A1 by A9, A14, A25, A26, CONNSP_1:35;
( B4 = Down (A2,(A `)) or B4 misses Down (A2,(A `)) ) by A11, A26, CONNSP_1:35;
then A29: ( B4 = Down (A2,(A `)) or B4 /\ (Down (A2,(A `))) = {} ((TOP-REAL 2) | (A `)) ) ;
B3 = B3 /\ (A1 \/ A2) by A3, A24, SPRECT_1:5, XBOOLE_1:28
.= (B3 /\ A1) \/ (B3 /\ A2) by XBOOLE_1:23
.= {} by A10, A19, A20, A22, A25, A29, A28 ;
hence contradiction by A27; :: thesis: verum

end;

now :: thesis: A2 is bounded

assume not A2 is bounded ; :: thesis: contradiction
then A2 is_outside_component_of A by A12;
then A2 /\ (UBD A) <> {} by Th14, XBOOLE_1:28;
hence contradiction by A4, A7, A16; :: thesis: verum

end;

then A30: A2 is_inside_component_of A by A12;
then A2 c= BDD A by Th13;
hence BDD A is_inside_component_of A by A30, A17, XBOOLE_0:def 10; :: thesis: verum

end;

suppose A31: B1 misses Down (A1,(A `)) ; :: thesis: BDD A is_inside_component_of A

set E1 = Down (A1,(A `));
set E2 = Down (A2,(A `));
(Down (A1,(A `))) \/ (Down (A2,(A `))) = [#] ((TOP-REAL 2) | (A `)) by A3, A9, A10, PRE_TOPC:def 5;
then A32: UBD A = A2 by A10, A11, A13, A7, A8, A31, Th91;
A33: (BDD A) \/ (UBD A) = A ` by Th18;
A34: BDD A misses UBD A by Th15;
A35: BDD A c= A1

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in BDD A or z in A1 )
assume z in BDD A ; :: thesis: z in A1
then ( z in A ` & not z in UBD A ) by A34, A33, XBOOLE_0:3, XBOOLE_0:def 3;
hence z in A1 by A3, A32, XBOOLE_0:def 3; :: thesis: verum

end;

A36: BDD A is bounded by A1, Th90;
A1 c= BDD A

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in A1 or z in BDD A )
assume z in A1 ; :: thesis: z in BDD A
then ( z in A ` & not z in UBD A ) by A3, A4, A32, XBOOLE_0:3, XBOOLE_0:def 3;
hence z in BDD A by A33, XBOOLE_0:def 3; :: thesis: verum

end;

then BDD A = A1 by A35;
hence BDD A is_inside_component_of A by A15, A36; :: thesis: verum

end;

end;