let n be Element of 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 A1: ( n >= 1 & W = REAL n ) ; :: thesis: not W is bounded
assume W is bounded ; :: thesis: contradiction
then consider r being Real such that
A2: ( 0 < r & ( for x, y being Point of (Euclid n) st x in W & y in W holds
dist x,y <= r ) ) by TBSP_1:def 9;
reconsider x0 = (r + 1) * (1.REAL n) as Point of (Euclid n) by TOPREAL3:13;
the carrier of (TOP-REAL n) = the carrier of (Euclid n) by EUCLID:71;
then reconsider y0 = 0. (TOP-REAL n) as Point of (Euclid n) by XX, YY;
dist x0,y0 <= r by A1, A2;
then |.(((r + 1) * (1.REAL n)) - (0. (TOP-REAL n))).| <= r by JGRAPH_1:45;
then |.((r + 1) * (1.REAL n)).| <= r by RLVECT_1:26, RLVECT_1:27;
then (abs (r + 1)) * |.(1.REAL n).| <= r by TOPRNS_1:8;
then A3: (abs (r + 1)) * (sqrt n) <= r by Th35;
A4: r + 1 > 0 by A2;
then A5: (r + 1) * (sqrt n) <= r by A3, ABSVALUE:def 1;
sqrt 1 <= sqrt n by A1, SQUARE_1:94;
then (r + 1) * 1 <= (r + 1) * (sqrt n) by A4, SQUARE_1:83, XREAL_1:66;
then (r + 1) * 1 <= r by A5, XXREAL_0:2;
then (r + 1) - r <= r - r by XREAL_1:11;
then 1 <= 0 ;
hence contradiction ; :: thesis: verum