let n be Element of NAT ; :: thesis: for A being Subset of (TOP-REAL n) st A is Bounded holds
BDD A is Bounded
let A be Subset of (TOP-REAL n); :: thesis: ( A is Bounded implies BDD A is Bounded )
assume A is Bounded ; :: thesis: BDD A is Bounded
then consider r being Real such that
A1: for q being Point of (TOP-REAL n) st q in A holds
|.q.| < r by Th40;

per cases ( n >= 1 or n < 1 ) ;

suppose A2: n >= 1 ; :: thesis: BDD A is Bounded

set a = r;
reconsider P = (REAL n) \ { q where q is Point of (TOP-REAL n) : |.q.| < r } as Subset of (TOP-REAL n) by EUCLID:22;
A3: P c= A `

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in P or z in A ` )
assume A4: z in P ; :: thesis: z in A `
then reconsider q0 = z as Point of (TOP-REAL n) ;
not z in { q where q is Point of (TOP-REAL n) : |.q.| < r } by A4, XBOOLE_0:def 5;
then |.q0.| >= r ;
then not q0 in A by A1;
hence z in A ` by XBOOLE_0:def 5; :: thesis: verum

end;

then A5: Down (P,(A `)) = P by XBOOLE_1:28;

now

per cases ( n >= 2 or n < 2 ) ;

suppose n >= 2 ; :: thesis: BDD A is Bounded

then A6: P is connected by Th61;

now

assume not BDD A is Bounded ; :: thesis: contradiction
then consider q being Point of (TOP-REAL n) such that
A7: q in BDD A and
A8: not |.q.| < r by Th40;
consider y being set such that
A9: q in y and
A10: y in { B3 where B3 is Subset of (TOP-REAL n) : B3 is_inside_component_of A } by A7, TARSKI:def 4;
consider B3 being Subset of (TOP-REAL n) such that
A11: y = B3 and
A12: B3 is_inside_component_of A by A10;
q in the carrier of (TOP-REAL n) ;
then A13: q in REAL n by EUCLID:22;
B3 is_a_component_of A ` by A12, Def3;
then consider B4 being Subset of ((TOP-REAL n) | (A `)) such that
A14: B4 = B3 and
A15: B4 is a_component by CONNSP_1:def 6;
for q2 being Point of (TOP-REAL n) st q2 = q holds
|.q2.| >= r by A8;
then not q in { q2 where q2 is Point of (TOP-REAL n) : |.q2.| < r } ;
then q in P by A13, XBOOLE_0:def 5;
then P /\ B4 <> {} ((TOP-REAL n) | (A `)) by A9, A11, A14, XBOOLE_0:def 4;
then P meets B4 by XBOOLE_0:def 7;
then A16: P c= B4 by A5, A6, A15, Th15, CONNSP_1:36;
B3 is Bounded by A12, Def3;
hence contradiction by A2, A14, A16, Th16, Th62; :: thesis: verum

end;

hence BDD A is Bounded ; :: thesis: verum

end;

suppose A17: n < 2 ; :: thesis: BDD A is Bounded

{ q where q is Point of (TOP-REAL n) : for r2 being Real st q = |[r2]| holds
r2 >= r } c= the carrier of (TOP-REAL n)

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in { q where q is Point of (TOP-REAL n) : for r2 being Real st q = |[r2]| holds
r2 >= r } or z in the carrier of (TOP-REAL n) )
assume z in { q where q is Point of (TOP-REAL n) : for r2 being Real st q = |[r2]| holds
r2 >= r } ; :: thesis: z in the carrier of (TOP-REAL n)
then ex q being Point of (TOP-REAL n) st
( q = z & ( for r2 being Real st q = |[r2]| holds
r2 >= r ) ) ;
hence z in the carrier of (TOP-REAL n) ; :: thesis: verum

end;

then reconsider P2 = { q where q is Point of (TOP-REAL n) : for r2 being Real st q = |[r2]| holds
r2 >= r } as Subset of (TOP-REAL n) ;
{ q where q is Point of (TOP-REAL n) : for r2 being Real st q = |[r2]| holds
r2 <= - r } c= the carrier of (TOP-REAL n)

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in { q where q is Point of (TOP-REAL n) : for r2 being Real st q = |[r2]| holds
r2 <= - r } or z in the carrier of (TOP-REAL n) )
assume z in { q where q is Point of (TOP-REAL n) : for r2 being Real st q = |[r2]| holds
r2 <= - r } ; :: thesis: z in the carrier of (TOP-REAL n)
then ex q being Point of (TOP-REAL n) st
( q = z & ( for r2 being Real st q = |[r2]| holds
r2 <= - r ) ) ;
hence z in the carrier of (TOP-REAL n) ; :: thesis: verum

end;

then reconsider P1 = { q where q is Point of (TOP-REAL n) : for r2 being Real st q = |[r2]| holds
r2 <= - r } as Subset of (TOP-REAL n) ;
n < 1 + 1 by A17;
then n <= 1 by NAT_1:13;
then A19: n = 1 by A2, XXREAL_0:1;
A20: P c= P1 \/ P2

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in P or z in P1 \/ P2 )
assume A21: z in P ; :: thesis: z in P1 \/ P2
then reconsider q0 = z as Point of (TOP-REAL n) ;
consider r3 being Real such that
A22: q0 = <*r3*> by A19, JORDAN2B:20;
not z in { q where q is Point of (TOP-REAL n) : |.q.| < r } by A21, XBOOLE_0:def 5;
then |.q0.| >= r ;
then A23: abs r3 >= r by A22, Th12;

per cases ( - r >= r3 or r3 >= r ) by A23, SEQ_2:1;

suppose - r >= r3 ; :: thesis: z in P1 \/ P2

then for r2 being Real st q0 = |[r2]| holds
r2 <= - r by A22, JORDAN2B:23;
then q0 in P1 ;
hence z in P1 \/ P2 by XBOOLE_0:def 3; :: thesis: verum

end;

suppose r3 >= r ; :: thesis: z in P1 \/ P2

then for r2 being Real st q0 = |[r2]| holds
r2 >= r by A22, JORDAN2B:23;
then q0 in P2 ;
hence z in P1 \/ P2 by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

P1 \/ P2 c= P

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in P1 \/ P2 or z in P )
assume A24: z in P1 \/ P2 ; :: thesis: z in P

per cases ( z in P1 or z in P2 ) by A24, XBOOLE_0:def 3;

suppose A25: z in P1 ; :: thesis: z in P

then A26: ex q being Point of (TOP-REAL n) st
( q = z & ( for r2 being Real st q = |[r2]| holds
r2 <= - r ) ) ;
for q2 being Point of (TOP-REAL n) st q2 = z holds
|.q2.| >= r

proof

let q2 be Point of (TOP-REAL n); :: thesis: ( q2 = z implies |.q2.| >= r )
consider r3 being Real such that
A27: q2 = <*r3*> by A19, JORDAN2B:20;
assume A28: q2 = z ; :: thesis: |.q2.| >= r
then A29: r3 <= - r by A26, A27;

now

per cases ( r < 0 or r >= 0 ) ;

case r < 0 ; :: thesis: abs r3 >= r

hence abs r3 >= r by COMPLEX1:46; :: thesis: verum

end;

case r >= 0 ; :: thesis: abs r3 >= r

then - r <= - 0 ;
then abs r3 = - r3 by A29, Th1;
hence abs r3 >= r by A26, A28, A27, XREAL_1:25; :: thesis: verum

end;

end;

end;

hence |.q2.| >= r by A27, Th12; :: thesis: verum

end;

then A30: not z in { q2 where q2 is Point of (TOP-REAL n) : |.q2.| < r } ;
z in the carrier of (TOP-REAL n) by A25;
then z in REAL n by EUCLID:22;
hence z in P by A30, XBOOLE_0:def 5; :: thesis: verum

end;

suppose A31: z in P2 ; :: thesis: z in P

then A32: ex q being Point of (TOP-REAL n) st
( q = z & ( for r2 being Real st q = |[r2]| holds
r2 >= r ) ) ;
for q2 being Point of (TOP-REAL n) st q2 = z holds
|.q2.| >= r

proof

let q2 be Point of (TOP-REAL n); :: thesis: ( q2 = z implies |.q2.| >= r )
consider r3 being Real such that
A33: q2 = <*r3*> by A19, JORDAN2B:20;
assume q2 = z ; :: thesis: |.q2.| >= r
then A34: r3 >= r by A32, A33;

now

per cases ( r < 0 or r >= 0 ) ;

suppose r < 0 ; :: thesis: abs r3 >= r

hence abs r3 >= r by COMPLEX1:46; :: thesis: verum

end;

suppose r >= 0 ; :: thesis: abs r3 >= r

hence abs r3 >= r by A34, ABSVALUE:def 1; :: thesis: verum

end;

end;

end;

hence |.q2.| >= r by A33, Th12; :: thesis: verum

end;

then A35: not z in { q2 where q2 is Point of (TOP-REAL n) : |.q2.| < r } ;
z in the carrier of (TOP-REAL n) by A31;
then z in REAL n by EUCLID:22;
hence z in P by A35, XBOOLE_0:def 5; :: thesis: verum

end;

end;

end;

then A36: P = P1 \/ P2 by A20, XBOOLE_0:def 10;
then P2 c= P by XBOOLE_1:7;
then A37: Down (P2,(A `)) = P2 by A3, XBOOLE_1:1, XBOOLE_1:28;
for w1, w2 being Point of (TOP-REAL n) st w1 in P2 & w2 in P2 holds
LSeg (w1,w2) c= P2

proof

let w1, w2 be Point of (TOP-REAL n); :: thesis: ( w1 in P2 & w2 in P2 implies LSeg (w1,w2) c= P2 )
assume that
A38: w1 in P2 and
A39: w2 in P2 ; :: thesis: LSeg (w1,w2) c= P2
A40: ex q2 being Point of (TOP-REAL n) st
( q2 = w2 & ( for r2 being Real st q2 = |[r2]| holds
r2 >= r ) ) by A39;
consider r3 being Real such that
A41: w1 = <*r3*> by A19, JORDAN2B:20;
consider r4 being Real such that
A42: w2 = <*r4*> by A19, JORDAN2B:20;
A43: ex q1 being Point of (TOP-REAL n) st
( q1 = w1 & ( for r2 being Real st q1 = |[r2]| holds
r2 >= r ) ) by A38;
thus LSeg (w1,w2) c= P2 :: thesis: verum

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in LSeg (w1,w2) or z in P2 )
assume z in LSeg (w1,w2) ; :: thesis: z in P2
then consider r2 being Real such that
A44: z = ((1 - r2) * w1) + (r2 * w2) and
A45: 0 <= r2 and
A46: r2 <= 1 ;
reconsider q4 = z as Point of (TOP-REAL n) by A44;
( (1 - r2) * w1 = |[((1 - r2) * r3)]| & r2 * w2 = |[(r2 * r4)]| ) by A19, A41, A42, JORDAN2B:21;
then A47: z = |[(((1 - r2) * r3) + (r2 * r4))]| by A19, A44, JORDAN2B:22;
for r5 being Real st q4 = |[r5]| holds
r5 >= r

proof

let r5 be Real; :: thesis: ( q4 = |[r5]| implies r5 >= r )
assume q4 = |[r5]| ; :: thesis: r5 >= r
then A48: r5 = ((1 - r2) * r3) + (r2 * r4) by A47, JORDAN2B:23;
1 - r2 >= 0 by A46, XREAL_1:48;
then A49: (1 - r2) * r3 >= (1 - r2) * r by A43, A41, XREAL_1:64;
( r2 * r4 >= r2 * r & ((1 - r2) * r) + (r2 * r) = r ) by A40, A42, A45, XREAL_1:64;
hence r5 >= r by A48, A49, XREAL_1:7; :: thesis: verum

end;

hence z in P2 ; :: thesis: verum

end;

end;

then P2 is convex by JORDAN1:def 1;
then A50: Down (P2,(A `)) is connected by A37, Th15;
P1 c= P by A36, XBOOLE_1:7;
then A51: Down (P1,(A `)) = P1 by A3, XBOOLE_1:1, XBOOLE_1:28;

A52: now

assume P2 is Bounded ; :: thesis: contradiction
then consider r being Real such that
A53: for q being Point of (TOP-REAL n) st q in P2 holds
|.q.| < r by Th40;
( 0 <= abs r & 0 <= abs r ) by COMPLEX1:46;
then A54: abs ((abs r) + (abs r)) = (abs r) + (abs r) by ABSVALUE:def 1;
set p3 = |[((abs r) + (abs r))]|;
A55: abs r <= (abs r) + (abs r) by COMPLEX1:46, XREAL_1:31;
for r5 being Real st |[((abs r) + (abs r))]| = |[r5]| holds
r5 >= r

proof

let r5 be Real; :: thesis: ( |[((abs r) + (abs r))]| = |[r5]| implies r5 >= r )
assume |[((abs r) + (abs r))]| = |[r5]| ; :: thesis: r5 >= r
then A56: r5 = (abs r) + (abs r) by JORDAN2B:23;
( r <= abs r & abs r <= (abs r) + (abs r) ) by ABSVALUE:4, COMPLEX1:46, XREAL_1:31;
hence r5 >= r by A56, XXREAL_0:2; :: thesis: verum

end;

then A57: |[((abs r) + (abs r))]| in P2 by A19;
( |.|[((abs r) + (abs r))]|.| = abs ((abs r) + (abs r)) & r <= abs r ) by Th12, ABSVALUE:4;
hence contradiction by A53, A57, A54, A55, XXREAL_0:2; :: thesis: verum

end;

A58: now

assume P1 is Bounded ; :: thesis: contradiction
then consider r being Real such that
A59: for q being Point of (TOP-REAL n) st q in P1 holds
|.q.| < r by Th40;
( 0 <= abs r & 0 <= abs r ) by COMPLEX1:46;
then A60: abs ((abs r) + (abs r)) = (abs r) + (abs r) by ABSVALUE:def 1;
set p3 = |[(- ((abs r) + (abs r)))]|;
A61: ( r <= abs r & abs r <= (abs r) + (abs r) ) by ABSVALUE:4, COMPLEX1:46, XREAL_1:31;
for r5 being Real st |[(- ((abs r) + (abs r)))]| = |[r5]| holds
r5 <= - r

proof

let r5 be Real; :: thesis: ( |[(- ((abs r) + (abs r)))]| = |[r5]| implies r5 <= - r )
r <= abs r by ABSVALUE:4;
then A62: - (abs r) <= - r by XREAL_1:24;
abs r <= (abs r) + (abs r) by COMPLEX1:46, XREAL_1:31;
then A63: - (abs r) >= - ((abs r) + (abs r)) by XREAL_1:24;
assume |[(- ((abs r) + (abs r)))]| = |[r5]| ; :: thesis: r5 <= - r
then r5 = - ((abs r) + (abs r)) by JORDAN2B:23;
hence r5 <= - r by A62, A63, XXREAL_0:2; :: thesis: verum

end;

then A64: |[(- ((abs r) + (abs r)))]| in P1 by A19;
|.|[(- ((abs r) + (abs r)))]|.| = abs (- ((abs r) + (abs r))) by Th12
.= abs ((abs r) + (abs r)) by COMPLEX1:52 ;
hence contradiction by A59, A64, A60, A61, XXREAL_0:2; :: thesis: verum

end;

for w1, w2 being Point of (TOP-REAL n) st w1 in P1 & w2 in P1 holds
LSeg (w1,w2) c= P1

proof

let w1, w2 be Point of (TOP-REAL n); :: thesis: ( w1 in P1 & w2 in P1 implies LSeg (w1,w2) c= P1 )
assume that
A65: w1 in P1 and
A66: w2 in P1 ; :: thesis: LSeg (w1,w2) c= P1
consider r4 being Real such that
A67: w2 = <*r4*> by A19, JORDAN2B:20;
ex q2 being Point of (TOP-REAL n) st
( q2 = w2 & ( for r2 being Real st q2 = |[r2]| holds
r2 <= - r ) ) by A66;
then A68: r4 <= - r by A67;
consider r3 being Real such that
A69: w1 = <*r3*> by A19, JORDAN2B:20;
ex q1 being Point of (TOP-REAL n) st
( q1 = w1 & ( for r2 being Real st q1 = |[r2]| holds
r2 <= - r ) ) by A65;
then A70: r3 <= - r by A69;
thus LSeg (w1,w2) c= P1 :: thesis: verum

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in LSeg (w1,w2) or z in P1 )
assume z in LSeg (w1,w2) ; :: thesis: z in P1
then consider r2 being Real such that
A71: z = ((1 - r2) * w1) + (r2 * w2) and
A72: 0 <= r2 and
A73: r2 <= 1 ;
reconsider q4 = z as Point of (TOP-REAL n) by A71;
A74: r2 * w2 = |[(r2 * r4)]| by A19, A67, JORDAN2B:21;
(1 - r2) * w1 = (1 - r2) * |[r3]| by A69
.= |[((1 - r2) * r3)]| by JORDAN2B:21 ;
then A75: z = |[(((1 - r2) * r3) + (r2 * r4))]| by A19, A71, A74, JORDAN2B:22;
for r5 being Real st q4 = |[r5]| holds
r5 <= - r

proof

let r5 be Real; :: thesis: ( q4 = |[r5]| implies r5 <= - r )
assume q4 = |[r5]| ; :: thesis: r5 <= - r
then A76: r5 = ((1 - r2) * r3) + (r2 * r4) by A75, JORDAN2B:23;
1 - r2 >= 0 by A73, XREAL_1:48;
then A77: (1 - r2) * r3 <= (1 - r2) * (- r) by A70, XREAL_1:64;
( r2 * r4 <= r2 * (- r) & ((1 - r2) * (- r)) + (r2 * (- r)) = - r ) by A68, A72, XREAL_1:64;
hence r5 <= - r by A76, A77, XREAL_1:7; :: thesis: verum

end;

hence z in P1 ; :: thesis: verum

end;

end;

then P1 is convex by JORDAN1:def 1;
then A78: Down (P1,(A `)) is connected by A51, Th15;

now

assume not BDD A is Bounded ; :: thesis: contradiction
then consider q being Point of (TOP-REAL n) such that
A79: q in BDD A and
A80: not |.q.| < r by Th40;
consider y being set such that
A81: q in y and
A82: y in { B3 where B3 is Subset of (TOP-REAL n) : B3 is_inside_component_of A } by A79, TARSKI:def 4;
consider B3 being Subset of (TOP-REAL n) such that
A83: y = B3 and
A84: B3 is_inside_component_of A by A82;
q in the carrier of (TOP-REAL n) ;
then A85: q in REAL n by EUCLID:22;
for q2 being Point of (TOP-REAL n) st q2 = q holds
|.q2.| >= r by A80;
then not q in { q2 where q2 is Point of (TOP-REAL n) : |.q2.| < r } ;
then A86: q in P by A85, XBOOLE_0:def 5;
B3 is_a_component_of A ` by A84, Def3;
then consider B4 being Subset of ((TOP-REAL n) | (A `)) such that
A87: B4 = B3 and
A88: B4 is a_component by CONNSP_1:def 6;

per cases ( q in P1 or q in P2 ) by A20, A86, XBOOLE_0:def 3;

suppose q in P1 ; :: thesis: contradiction

then P1 /\ B4 <> {} ((TOP-REAL n) | (A `)) by A81, A83, A87, XBOOLE_0:def 4;
then A89: P1 meets B4 by XBOOLE_0:def 7;
B3 is Bounded by A84, Def3;
hence contradiction by A51, A58, A78, A87, A88, A89, Th16, CONNSP_1:36; :: thesis: verum

end;

suppose q in P2 ; :: thesis: contradiction

then P2 /\ B4 <> {} ((TOP-REAL n) | (A `)) by A81, A83, A87, XBOOLE_0:def 4;
then A90: P2 meets B4 by XBOOLE_0:def 7;
B3 is Bounded by A84, Def3;
hence contradiction by A37, A52, A50, A87, A88, A90, Th16, CONNSP_1:36; :: thesis: verum

end;

end;

end;

hence BDD A is Bounded ; :: thesis: verum

end;

end;

end;

hence BDD A is Bounded ; :: thesis: verum

end;

suppose n < 1 ; :: thesis: BDD A is Bounded

then n < 0 + 1 ;
then n <= 0 by NAT_1:13;
then A91: n = 0 by NAT_1:2;
for q2 being Point of (TOP-REAL n) holds |.q2.| < 1

proof

let q2 be Point of (TOP-REAL n); :: thesis: |.q2.| < 1
q2 = 0. (TOP-REAL n) by A91, Th113;
hence |.q2.| < 1 by TOPRNS_1:23; :: thesis: verum

end;

then for q2 being Point of (TOP-REAL n) st q2 in [#] (TOP-REAL n) holds
|.q2.| < 1 ;
then [#] (TOP-REAL n) is Bounded by Th40;
hence BDD A is Bounded by Th16; :: thesis: verum

end;

end;