let n be Nat; :: thesis: for W being Subset of (Euclid n) st n >= 1 & W = REAL n holds
not W is bounded
let W be Subset of (Euclid n); :: thesis: ( n >= 1 & W = REAL n implies not W is bounded )
assume that
A1: n >= 1 and
A2: W = REAL n ; :: thesis: not W is bounded
reconsider y0 = 0. (TOP-REAL n) as Point of (Euclid n) by EUCLID:67;
assume W is bounded ; :: thesis: contradiction
then consider r being Real such that
A3: 0 < r and
A4: for x, y being Point of (Euclid n) st x in W & y in W holds
dist (x,y) <= r ;
reconsider x0 = (r + 1) * (1.REAL n) as Point of (Euclid n) by TOPREAL3:8;
dist (x0,y0) <= r by A2, A4;
then |.(((r + 1) * (1.REAL n)) - (0. (TOP-REAL n))).| <= r by JGRAPH_1:28;
then |.((r + 1) * (1.REAL n)).| <= r by RLVECT_1:13;
then |.(r + 1).| * |.(1.REAL n).| <= r by TOPRNS_1:7;
then |.(r + 1).| * (sqrt n) <= r by EUCLID:73;
then A5: (r + 1) * (sqrt n) <= r by A3, ABSVALUE:def 1;
sqrt 1 <= sqrt n by A1, SQUARE_1:26;
then (r + 1) * 1 <= (r + 1) * (sqrt n) by A3, XREAL_1:64;
then (r + 1) * 1 <= r by A5, XXREAL_0:2;
then (r + 1) - r <= r - r by XREAL_1:9;
then 1 <= 0 ;
hence contradiction ; :: thesis: verum