let n be 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 object ; :: 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 ex q being Point of (TOP-REAL n) st
( q = x & |.q.| < r ) ;
then x in the carrier of (TOP-REAL n) ;
hence x in the carrier of (Euclid n) by TOPREAL3:8; :: 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
reconsider C = { q1 where q1 is Point of (TOP-REAL n) : |.q1.| < r } as Subset of (TOP-REAL n) by A1, TOPREAL3:8;
let A be Subset of (Euclid n); :: thesis: ( A = { q1 where q1 is Point of (TOP-REAL n) : |.q1.| < r } implies A is bounded )
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 ex q1 being Point of (TOP-REAL n) st
( q1 = q & |.q1.| < r ) ;
hence |.q.| < r ; :: thesis: verum

end;

then A2: C is bounded by Th21;
assume A = { q1 where q1 is Point of (TOP-REAL n) : |.q1.| < r } ; :: thesis: A is bounded
hence A is bounded by A2, Th5; :: thesis: verum