let A be Subset of (TOP-REAL 2); :: thesis:
assume A1: ( A is Bounded & A is Jordan ) ; :: thesis:
then consider A1, A2 being Subset of (TOP-REAL 2) such that
A2: ( A ` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & ( for C1, C2 being Subset of ((TOP-REAL 2) | (A ` )) st C1 = A1 & C2 = A2 holds
( C1 is_a_component_of (TOP-REAL 2) | (A ` ) & C2 is_a_component_of (TOP-REAL 2) | (A ` ) ) ) ) by JORDAN1:def 2;
A3: Down A1,(A ` ) = A1 by A2, XBOOLE_1:21;
A4: Down A2,(A ` ) = A2 by A2, XBOOLE_1:21;
then A5: ( Down A1,(A ` ) is_a_component_of (TOP-REAL 2) | (A ` ) & Down A2,(A ` ) is_a_component_of (TOP-REAL 2) | (A ` ) ) by A2, A3;
then A6: A1 is_a_component_of A ` by A3, CONNSP_1:def 6;
A7: A2 is_a_component_of A ` by A4, A5, CONNSP_1:def 6;
reconsider D = A ` as non empty Subset of (TOP-REAL 2) by A1, JORDAN1:def 2;
A8: not (TOP-REAL 2) | D is empty ;
then A9: Down A2,(A ` ) <> {} ((TOP-REAL 2) | (A ` )) by A5, CONNSP_1:34;
A10: 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
A11: ( B1 = UBD A & B1 is_a_component_of (TOP-REAL 2) | (A ` ) ) by CONNSP_1:def 6;

per cases by A3, A5, A11, CONNSP_1:37;

suppose A12: B1 = A1 ; :: thesis:

now

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

end;

then A13: A2 is_inside_component_of A by A7, Def3;
then A14: A2 c= BDD A by Th26;

now

assume not BDD A c= A2 ; :: thesis:
then consider x being set such that
A15: ( x in BDD A & not x in A2 ) by TARSKI:def 3;
consider y being set such that
A16: ( x in y & y in { B3 where B3 is Subset of (TOP-REAL 2) : B3 is_inside_component_of A } ) by A15, TARSKI:def 4;
consider B3 being Subset of (TOP-REAL 2) such that
A17: ( y = B3 & B3 is_inside_component_of A ) by A16;
A18: B3 is_a_component_of A ` by A17, Def3;
then consider B4 being Subset of ((TOP-REAL 2) | (A ` )) such that
A19: ( B4 = B3 & B4 is_a_component_of (TOP-REAL 2) | (A ` ) ) by CONNSP_1:def 6;
A20: B3 <> {} ((TOP-REAL 2) | (A ` )) by A8, A19, CONNSP_1:34;
( B4 = Down A2,(A ` ) or B4 misses Down A2,(A ` ) ) by A5, A19, CONNSP_1:37;
then A21: ( B4 = Down A2,(A ` ) or B4 /\ (Down A2,(A ` )) = {} ((TOP-REAL 2) | (A ` )) ) by XBOOLE_0:def 7;

now

assume B4 = Down A1,(A ` ) ; :: thesis:
then UBD A is Bounded by A3, A11, A12, A17, A19, Def3;
hence contradiction by A10, Def4; :: thesis:

end;

then A22: ( B3 misses A1 & B3 misses A2 ) by A3, A4, A5, A15, A16, A17, A19, CONNSP_1:37;
B3 c= A ` by A18, SPRECT_1:7;
then B3 = B3 /\ (A1 \/ A2) by A2, XBOOLE_1:28
.= (B3 /\ A1) \/ (B3 /\ A2) by XBOOLE_1:23
.= {} by A4, A16, A17, A19, A21, A22, XBOOLE_0:def 7 ;
hence contradiction by A20; :: thesis:

end;

hence BDD A is_inside_component_of A by A13, A14, XBOOLE_0:def 10; :: thesis:

end;

suppose A23: B1 misses Down A1,(A ` ) ; :: thesis:

A24: BDD A misses UBD A by Th28;
A25: (BDD A) \/ (UBD A) = A ` by Th31;
set E1 = Down A1,(A ` );
set E2 = Down A2,(A ` );
(Down A1,(A ` )) \/ (Down A2,(A ` )) = [#] ((TOP-REAL 2) | (A ` )) by A2, A3, A4, PRE_TOPC:def 10;
then A26: UBD A = A2 by A4, A5, A8, A11, A23, Th115;
A27: BDD A c= A1

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume A28: z in BDD A ; :: thesis:
then A29: z in A ` by A25, XBOOLE_0:def 3;
not z in UBD A by A24, A28, XBOOLE_0:3;
hence z in A1 by A2, A26, A29, XBOOLE_0:def 3; :: thesis:

end;

A1 c= BDD A

proof

let z be set ; :: according to TARSKI:def 3 :: thesis:
assume A30: z in A1 ; :: thesis:
then A31: z in A ` by A2, XBOOLE_0:def 3;
not z in UBD A by A2, A26, A30, XBOOLE_0:3;
hence z in BDD A by A25, A31, XBOOLE_0:def 3; :: thesis:

end;

then A32: BDD A = A1 by A27, XBOOLE_0:def 10;
BDD A is Bounded by A1, Th114;
hence BDD A is_inside_component_of A by A6, A32, Def3; :: thesis:

end;