let n be Element of NAT ; :: thesis: for r being Real holds
( ex B being Subset of (Euclid n) st B = { q where q is Point of (TOP-REAL n) : |.q.| < r } & ( for A being Subset of (Euclid n) st A = { q1 where q1 is Point of (TOP-REAL n) : |.q1.| < r } holds
A is bounded ) )
let r be Real; :: thesis: ( ex B being Subset of (Euclid n) st B = { q where q is Point of (TOP-REAL n) : |.q.| < r } & ( for A being Subset of (Euclid n) st A = { q1 where q1 is Point of (TOP-REAL n) : |.q1.| < r } holds
A is bounded ) )
A1: { q where q is Point of (TOP-REAL n) : |.q.| < r } c= the carrier of (Euclid n)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { q where q is Point of (TOP-REAL n) : |.q.| < r } or x in the carrier of (Euclid n) )
assume x in { q where q is Point of (TOP-REAL n) : |.q.| < r } ; :: thesis: x in the carrier of (Euclid n)
then consider q being Point of (TOP-REAL n) such that
A2: ( q = x & |.q.| < r ) ;
x in the carrier of (TOP-REAL n) by A2;
hence x in the carrier of (Euclid n) by TOPREAL3:13; :: thesis: verum

end;

hence ex B being Subset of (Euclid n) st B = { q where q is Point of (TOP-REAL n) : |.q.| < r } ; :: thesis: for A being Subset of (Euclid n) st A = { q1 where q1 is Point of (TOP-REAL n) : |.q1.| < r } holds
A is bounded
let A be Subset of (Euclid n); :: thesis: ( A = { q1 where q1 is Point of (TOP-REAL n) : |.q1.| < r } implies A is bounded )
assume A3: A = { q1 where q1 is Point of (TOP-REAL n) : |.q1.| < r } ; :: thesis: A is bounded
reconsider C = { q1 where q1 is Point of (TOP-REAL n) : |.q1.| < r } as Subset of (TOP-REAL n) by A1, TOPREAL3:13;
for q being Point of (TOP-REAL n) st q in C holds
|.q.| < r

proof

let q be Point of (TOP-REAL n); :: thesis: ( q in C implies |.q.| < r )
assume q in C ; :: thesis: |.q.| < r
then consider q1 being Point of (TOP-REAL n) such that
A4: ( q1 = q & |.q1.| < r ) ;
thus |.q.| < r by A4; :: thesis: verum

end;

then C is Bounded by Th40;
hence A is bounded by A3, Def2; :: thesis: verum