let n be Nat; :: thesis: ( n >= 1 implies UBD ({} (TOP-REAL n)) = [#] (TOP-REAL n) )
set X = { B where B is Subset of (TOP-REAL n) : B is_outside_component_of {} (TOP-REAL n) } ;
assume n >= 1 ; :: thesis: UBD ({} (TOP-REAL n)) = [#] (TOP-REAL n)
then A1: not [#] (TOP-REAL n) is bounded by JORDAN2C:35;
thus UBD ({} (TOP-REAL n)) c= [#] (TOP-REAL n) ; :: according to XBOOLE_0:def 10 :: thesis: [#] (TOP-REAL n) c= UBD ({} (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;
[#] (TOP-REAL n) = ({} (TOP-REAL n)) ` ;
then [#] (TOP-REAL n) is_outside_component_of {} (TOP-REAL n) by A1, A3, JORDAN2C:def 3;
then [#] (TOP-REAL n) in { B where B is Subset of (TOP-REAL n) : B is_outside_component_of {} (TOP-REAL n) } ;
then [#] (TOP-REAL n) c= union { B where B is Subset of (TOP-REAL n) : B is_outside_component_of {} (TOP-REAL n) } by ZFMISC_1:74;
hence [#] (TOP-REAL n) c= UBD ({} (TOP-REAL n)) by JORDAN2C:def 5; :: thesis: verum