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, Th76;
then UBD A is_a_component_of A ` by Def4;
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 ;
then A14: Down (A2,(A `)) <> {} ((TOP-REAL 2) | (A `)) by A11, CONNSP_1:32;
A15: Down (A1,(A `)) is a_component by A5, A9, A10;
then A16: A1 is_a_component_of A ` by A9, CONNSP_1:def 6;

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

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

A18: now

assume not BDD A c= A2 ; :: thesis: contradiction
then consider x being set such that
A19: x in BDD A and
A20: not x in A2 by TARSKI:def 3;
consider y being set such that
A21: x in y and
A22: y in { B3 where B3 is Subset of (TOP-REAL 2) : B3 is_inside_component_of A } by A19, TARSKI:def 4;
consider B3 being Subset of (TOP-REAL 2) such that
A23: y = B3 and
A24: B3 is_inside_component_of A by A22;
A25: B3 is_a_component_of A ` by A24, Def3;
then consider B4 being Subset of ((TOP-REAL 2) | (A `)) such that
A26: B4 = B3 and
A27: B4 is a_component by CONNSP_1:def 6;
A28: B3 <> {} ((TOP-REAL 2) | (A `)) by A13, A26, A27, CONNSP_1:32;

now

assume B4 = Down (A1,(A `)) ; :: thesis: contradiction
then UBD A is Bounded by A9, A7, A17, A24, A26, Def3;
hence contradiction by A6, Def4; :: thesis: verum

end;

then A29: B3 misses A1 by A9, A15, A26, A27, CONNSP_1:35;
( B4 = Down (A2,(A `)) or B4 misses Down (A2,(A `)) ) by A11, A27, CONNSP_1:35;
then A30: ( B4 = Down (A2,(A `)) or B4 /\ (Down (A2,(A `))) = {} ((TOP-REAL 2) | (A `)) ) by XBOOLE_0:def 7;
B3 = B3 /\ (A1 \/ A2) by A3, A25, SPRECT_1:5, XBOOLE_1:28
.= (B3 /\ A1) \/ (B3 /\ A2) by XBOOLE_1:23
.= {} by A10, A20, A21, A23, A26, A30, A29, XBOOLE_0:def 7 ;
hence contradiction by A28; :: thesis: verum

end;

now

assume not A2 is Bounded ; :: thesis: contradiction
then A2 is_outside_component_of A by A12, Def4;
then A2 /\ (UBD A) <> {} by A10, A14, Th27, XBOOLE_1:28;
hence contradiction by A4, A7, A17, XBOOLE_0:def 7; :: thesis: verum

end;

then A31: A2 is_inside_component_of A by A12, Def3;
then A2 c= BDD A by Th26;
hence BDD A is_inside_component_of A by A31, A18, XBOOLE_0:def 10; :: thesis: verum

end;

suppose A32: 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 A33: UBD A = A2 by A10, A11, A13, A7, A8, A32, Th115;
A34: (BDD A) \/ (UBD A) = A ` by Th31;
A35: BDD A misses UBD A by Th28;
A36: BDD A c= A1

proof

let z be set ; :: 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 A35, A34, XBOOLE_0:3, XBOOLE_0:def 3;
hence z in A1 by A3, A33, XBOOLE_0:def 3; :: thesis: verum

end;

A37: BDD A is Bounded by A1, Th114;
A1 c= BDD A

proof

let z be set ; :: 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, A33, XBOOLE_0:3, XBOOLE_0:def 3;
hence z in BDD A by A34, XBOOLE_0:def 3; :: thesis: verum

end;

then BDD A = A1 by A36, XBOOLE_0:def 10;
hence BDD A is_inside_component_of A by A16, A37, Def3; :: thesis: verum

end;

end;