let n be Element of NAT ; :: thesis: ( n >= 1 implies UBD ({} (TOP-REAL n)) = REAL n )
set A = {} (TOP-REAL n);
A1: (TOP-REAL n) | ([#] (TOP-REAL n)) = TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) by TSEP_1:100;
assume A2: n >= 1 ; :: thesis: UBD ({} (TOP-REAL n)) = REAL n

A3: now

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

end;

[#] (TOP-REAL n) is a_component by Th23;
then [#] ((TOP-REAL n) | (({} (TOP-REAL n)) ` )) is a_component by A1, CONNSP_1:48;
then [#] (TOP-REAL n) is_outside_component_of {} (TOP-REAL n) by A1, A3, Th18;
then A4: [#] (TOP-REAL n) in { B2 where B2 is Subset of (TOP-REAL n) : B2 is_outside_component_of {} (TOP-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 x in REAL n ; :: thesis: x in UBD ({} (TOP-REAL n))
then x in [#] (TOP-REAL n) by EUCLID:25;
hence x in UBD ({} (TOP-REAL n)) by A4, TARSKI:def 4; :: thesis: verum