let n be Element of NAT ; :: thesis: ( n >= 1 implies UBD ({} (TOP-REAL n)) = REAL n )
assume A1: n >= 1 ; :: thesis: UBD ({} (TOP-REAL n)) = REAL n
UBD ({} (TOP-REAL n)) c= the carrier of (TOP-REAL n) ;
hence UBD ({} (TOP-REAL n)) c= REAL n by EUCLID:25; :: according to XBOOLE_0:def 10 :: thesis: REAL n c= UBD ({} (TOP-REAL n))
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in REAL n or x in UBD ({} (TOP-REAL n)) )
assume A2: x in REAL n ; :: thesis: x in UBD ({} (TOP-REAL n))
set A = {} (TOP-REAL n);
X: ({} (TOP-REAL n)) ` = [#] (TOP-REAL n) ;
A3: (TOP-REAL n) | ([#] (TOP-REAL n)) = TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) by TSEP_1:100;
then A4: [#] ((TOP-REAL n) | (({} (TOP-REAL n)) ` )) = [#] TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) by X, TSEP_1:100;
[#] (TOP-REAL n) is_a_component_of TOP-REAL n by Th23;
then A5: [#] ((TOP-REAL n) | (({} (TOP-REAL n)) ` )) is_a_component_of (TOP-REAL n) | (({} (TOP-REAL n)) ` ) by A3, A4, CONNSP_1:48;

now

assume A6: for D being Subset of (Euclid n) st D = [#] ((TOP-REAL n) | (({} (TOP-REAL n)) ` )) holds
D is bounded ; :: thesis: contradiction
reconsider D1 = [#] ((TOP-REAL n) | (({} (TOP-REAL n)) ` )) as Subset of (Euclid n) by A3, TOPREAL3:13;
D1 is bounded by A6;
then [#] (TOP-REAL n) is Bounded by A3, Def2;
hence contradiction by A1, Th41; :: thesis: verum

end;

then ( x in [#] (TOP-REAL n) & [#] (TOP-REAL n) is_outside_component_of {} (TOP-REAL n) ) by A2, A4, A5, Th18, EUCLID:25;
then ( x in [#] (TOP-REAL n) & [#] (TOP-REAL n) in { B2 where B2 is Subset of (TOP-REAL n) : B2 is_outside_component_of {} (TOP-REAL n) } ) ;
hence x in UBD ({} (TOP-REAL n)) by TARSKI:def 4; :: thesis: verum