let n be 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:93;
assume A2: n >= 1 ; :: thesis: UBD ({} (TOP-REAL n)) = REAL n

A3: now :: thesis: ex D being Subset of (Euclid n) st
( D = [#] ((TOP-REAL n) | (({} (TOP-REAL n)) `)) & not D is bounded )

reconsider D1 = [#] ((TOP-REAL n) | (({} (TOP-REAL n)) `)) as Subset of (Euclid n) by A1, TOPREAL3:8;
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, Th5;
hence contradiction by A2, Th22; :: thesis: verum

end;

[#] ((TOP-REAL n) | (({} (TOP-REAL n)) `)) is a_component by A1, CONNSP_1:45;
then [#] (TOP-REAL n) is_outside_component_of {} (TOP-REAL n) by A1, A3, Th8;
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:22; :: according to XBOOLE_0:def 10 :: thesis: REAL n c= UBD ({} (TOP-REAL n))
let x be object ; :: 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:22;
hence x in UBD ({} (TOP-REAL n)) by A4, TARSKI:def 4; :: thesis: verum