let n be Nat; :: thesis: for A being Subset of (TOP-REAL n) holds
( A is bounded iff A is bounded Subset of (Euclid n) )
let A be Subset of (TOP-REAL n); :: thesis: ( A is bounded iff A is bounded Subset of (Euclid n) )
reconsider z = 0* n as Element of (Euclid n) ;
thus ( A is bounded implies A is bounded Subset of (Euclid n) ) :: thesis: ( A is bounded Subset of (Euclid n) implies A is bounded )

proof

assume A1: A is bounded ; :: thesis: A is bounded Subset of (Euclid n)
reconsider B = A as Subset of (Euclid n) by EUCLID:67;
z = 0. (TOP-REAL n) by EUCLID:70;
then reconsider V = Ball (z,1) as a_neighborhood of 0. (TOP-REAL n) by GOBOARD6:2;
consider s being Real such that
A2: s > 0 and
A3: for t being Real st t > s holds
A c= t * V by A1;
set r = s + 1;
0 < s + 1 by A2;
then (s + 1) * V = Ball (z,((s + 1) * 1)) by Lm2;
then B c= Ball (z,(s + 1)) by A3, XREAL_1:29;
hence A is bounded Subset of (Euclid n) by A2, METRIC_6:def 3; :: thesis: verum

end;

assume A4: A is bounded Subset of (Euclid n) ; :: thesis: A is bounded
then reconsider B = A as Subset of (Euclid n) ;
consider r1 being Real such that
A5: 0 < r1 and
A6: B c= Ball (z,r1) by A4, METRIC_6:29;
let V be a_neighborhood of 0. (TOP-REAL n); :: according to RLTOPSP1:def 12 :: thesis: ex b₁ being object st
( not b₁ <= 0 & ( for b₂ being object holds
( b₂ <= b₁ or A c= b₂ * V ) ) )
0. (TOP-REAL n) = 0* n by EUCLID:70;
then z in Int V by CONNSP_2:def 1;
then consider r2 being Real such that
A7: r2 > 0 and
A8: Ball (z,r2) c= V by GOBOARD6:5;
reconsider r2 = r2 as Real ;
take s = r1 / r2; :: thesis: ( not s <= 0 & ( for b₁ being object holds
( b₁ <= s or A c= b₁ * V ) ) )
thus A9: s > 0 by A5, A7, XREAL_1:139; :: thesis: for b₁ being object holds
( b₁ <= s or A c= b₁ * V )
let t be Real; :: thesis: ( t <= s or A c= t * V )
reconsider BA = Ball (z,r2) as Subset of (TOP-REAL n) by EUCLID:67;
s * r2 = r1 by A7, XCMPLX_1:87;
then A10: A c= s * BA by A6, A9, Lm2;
assume t > s ; :: thesis: A c= t * V
then s * BA c= t * BA by A9, Lm3;
then A11: A c= t * BA by A10;
t * BA c= t * V by A8, CONVEX1:39;
hence A c= t * V by A11; :: thesis: verum