let n be Nat; :: thesis: ( n >= 1 implies BDD ({} (TOP-REAL n)) = {} (TOP-REAL n) )
set X = { B where B is Subset of (TOP-REAL n) : B is_inside_component_of {} (TOP-REAL n) } ;
assume n >= 1 ; :: thesis: BDD ({} (TOP-REAL n)) = {} (TOP-REAL n)
then A1: not [#] (TOP-REAL n) is bounded by JORDAN2C:35;

now :: thesis: not { B where B is Subset of (TOP-REAL n) : B is_inside_component_of {} (TOP-REAL n) } <> {}

[#] (TOP-REAL n) is a_component ;
then A2: [#] TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) is a_component by CONNSP_1:45;
(TOP-REAL n) | ([#] (TOP-REAL n)) = TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) by TSEP_1:93;
then A3: [#] (TOP-REAL n) is_a_component_of [#] (TOP-REAL n) by A2, CONNSP_1:def 6;
assume { B where B is Subset of (TOP-REAL n) : B is_inside_component_of {} (TOP-REAL n) } <> {} ; :: thesis: contradiction
then consider x being object such that
A4: x in { B where B is Subset of (TOP-REAL n) : B is_inside_component_of {} (TOP-REAL n) } by XBOOLE_0:def 1;
consider B being Subset of (TOP-REAL n) such that
x = B and
A5: B is_inside_component_of {} (TOP-REAL n) by A4;
B is_a_component_of ({} (TOP-REAL n)) ` by A5, JORDAN2C:def 2;
then B = [#] (TOP-REAL n) by A3, Th7;
hence contradiction by A1, A5, JORDAN2C:def 2; :: thesis: verum

end;

hence BDD ({} (TOP-REAL n)) = {} (TOP-REAL n) by JORDAN2C:def 4, ZFMISC_1:2; :: thesis: verum