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:25;
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 A5: ( z in REAL n & not z in { q where q is Point of (TOP-REAL n) : |.q.| < r } ) by XBOOLE_0:def 5;
reconsider q0 = z as Point of (TOP-REAL n) by A4;
|.q0.| >= r by A5;
then not q0 in A by A1;
hence z in A ` by XBOOLE_0:def 5; :: thesis: verum

end;

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

end;

hence BDD A is Bounded ; :: thesis: verum

end;

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

then n < 1 + 1 ;
then n <= 1 by NAT_1:13;
then A14: n = 1 by A2, XXREAL_0:1;
{ 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 consider q being Point of (TOP-REAL n) such that
A15: ( q = z & ( for r2 being Real st q = |[r2]| holds
r2 <= - r ) ) ;
thus z in the carrier of (TOP-REAL n) by A15; :: 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) ;
{ 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 consider q being Point of (TOP-REAL n) such that
A16: ( q = z & ( for r2 being Real st q = |[r2]| holds
r2 >= r ) ) ;
thus z in the carrier of (TOP-REAL n) by A16; :: 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) ;
A17: 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 A18: z in P ; :: thesis: z in P1 \/ P2
then A19: ( z in REAL n & not z in { q where q is Point of (TOP-REAL n) : |.q.| < r } ) by XBOOLE_0:def 5;
reconsider q0 = z as Point of (TOP-REAL n) by A18;
A20: |.q0.| >= r by A19;
consider r3 being Real such that
A21: q0 = <*r3*> by A14, JORDAN2B:24;
A22: abs r3 >= r by A20, A21, Th12;

per cases ( - r >= r3 or r3 >= r ) by A22, SEQ_2:9;

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

then for r2 being Real st q0 = |[r2]| holds
r2 <= - r by A21, JORDAN2B:29;
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 A21, JORDAN2B:29;
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 A23: z in P1 \/ P2 ; :: thesis: z in P

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

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

then consider q being Point of (TOP-REAL n) such that
A24: ( q = z & ( for r2 being Real st q = |[r2]| holds
r2 <= - r ) ) ;
A25: z in the carrier of (TOP-REAL n) by A24;
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 )
assume A26: q2 = z ; :: thesis: |.q2.| >= r
consider r3 being Real such that
A27: q2 = <*r3*> by A14, JORDAN2B:24;
A28: r3 <= - r by A24, A26, A27;

now

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

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

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

end;

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

then - r <= - 0 ;
then abs r3 = - r3 by A28, Th1;
hence abs r3 >= r by A28, XREAL_1:27; :: thesis: verum

end;

end;

end;

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

end;

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

end;

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

then consider q being Point of (TOP-REAL n) such that
A29: ( q = z & ( for r2 being Real st q = |[r2]| holds
r2 >= r ) ) ;
A30: z in the carrier of (TOP-REAL n) by A29;
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 )
assume A31: q2 = z ; :: thesis: |.q2.| >= r
consider r3 being Real such that
A32: q2 = <*r3*> by A14, JORDAN2B:24;
A33: r3 >= r by A29, A31, A32;

now

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

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

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

end;

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

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

end;

end;

end;

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

end;

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

end;

end;

end;

then A34: P = P1 \/ P2 by A17, XBOOLE_0:def 10;
then P1 c= P by XBOOLE_1:7;
then A35: Down P1,(A ` ) = P1 by A3, XBOOLE_1:1, XBOOLE_1:28;
P2 c= P by A34, XBOOLE_1:7;
then A36: Down P2,(A ` ) = P2 by A3, XBOOLE_1:1, XBOOLE_1:28;
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 A37: ( w1 in P1 & w2 in P1 ) ; :: thesis: LSeg w1,w2 c= P1
then consider q1 being Point of (TOP-REAL n) such that
A38: ( q1 = w1 & ( for r2 being Real st q1 = |[r2]| holds
r2 <= - r ) ) ;
consider q2 being Point of (TOP-REAL n) such that
A39: ( q2 = w2 & ( for r2 being Real st q2 = |[r2]| holds
r2 <= - r ) ) by A37;
consider r3 being Real such that
A40: w1 = <*r3*> by A14, JORDAN2B:24;
A41: r3 <= - r by A38, A40;
consider r4 being Real such that
A42: w2 = <*r4*> by A14, JORDAN2B:24;
A43: r4 <= - r by A39, A42;
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 z in { (((1 - r2) * w1) + (r2 * w2)) where r2 is Real : ( 0 <= r2 & r2 <= 1 ) } ;
then consider r2 being Real such that
A44: ( z = ((1 - r2) * w1) + (r2 * w2) & 0 <= r2 & r2 <= 1 ) ;
w1 = |[r3]| by A40;
then A45: (1 - r2) * w1 = (1 - r2) * |[r3]| by A40, A14, EUCLID:69
.= |[((1 - r2) * r3)]| by A40, JORDAN2B:26 ;
r2 * w2 = |[(r2 * r4)]| by A42, A14, JORDAN2B:26;
then A46: z = |[(((1 - r2) * r3) + (r2 * r4))]| by A44, A45, A14, JORDAN2B:27;
reconsider q4 = z as Point of (TOP-REAL n) by A44;
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 A47: r5 = ((1 - r2) * r3) + (r2 * r4) by A46, JORDAN2B:29;
1 - r2 >= 0 by A44, XREAL_1:50;
then A48: (1 - r2) * r3 <= (1 - r2) * (- r) by A41, XREAL_1:66;
A49: r2 * r4 <= r2 * (- r) by A43, A44, XREAL_1:66;
((1 - r2) * (- r)) + (r2 * (- r)) = - r ;
hence r5 <= - r by A47, A48, A49, XREAL_1:9; :: thesis: verum

end;

hence z in P1 ; :: thesis: verum

end;

end;

then A50: P1 is convex by JORDAN1:def 1;
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 A51: ( w1 in P2 & w2 in P2 ) ; :: thesis: LSeg w1,w2 c= P2
then consider q1 being Point of (TOP-REAL n) such that
A52: ( q1 = w1 & ( for r2 being Real st q1 = |[r2]| holds
r2 >= r ) ) ;
consider q2 being Point of (TOP-REAL n) such that
A53: ( q2 = w2 & ( for r2 being Real st q2 = |[r2]| holds
r2 >= r ) ) by A51;
consider r3 being Real such that
A54: w1 = <*r3*> by A14, JORDAN2B:24;
consider r4 being Real such that
A55: w2 = <*r4*> by A14, JORDAN2B:24;
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 z in { (((1 - r2) * w1) + (r2 * w2)) where r2 is Real : ( 0 <= r2 & r2 <= 1 ) } ;
then consider r2 being Real such that
A56: ( z = ((1 - r2) * w1) + (r2 * w2) & 0 <= r2 & r2 <= 1 ) ;
A57: (1 - r2) * w1 = |[((1 - r2) * r3)]| by A54, A14, JORDAN2B:26;
r2 * w2 = |[(r2 * r4)]| by A55, A14, JORDAN2B:26;
then A58: z = |[(((1 - r2) * r3) + (r2 * r4))]| by A56, A57, A14, JORDAN2B:27;
reconsider q4 = z as Point of (TOP-REAL n) by A56;
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 A59: r5 = ((1 - r2) * r3) + (r2 * r4) by A58, JORDAN2B:29;
1 - r2 >= 0 by A56, XREAL_1:50;
then A60: (1 - r2) * r3 >= (1 - r2) * r by A52, A54, XREAL_1:66;
A61: r2 * r4 >= r2 * r by A53, A55, A56, XREAL_1:66;
((1 - r2) * r) + (r2 * r) = r ;
hence r5 >= r by A59, A60, A61, XREAL_1:9; :: thesis: verum

end;

hence z in P2 ; :: thesis: verum

end;

end;

then A62: P2 is convex by JORDAN1:def 1;

A63: now

assume P1 is Bounded ; :: thesis: contradiction
then consider r being Real such that
A64: for q being Point of (TOP-REAL n) st q in P1 holds
|.q.| < r by Th40;
set p3 = |[(- ((abs r) + (abs r)))]|;
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 A65: r5 = - ((abs r) + (abs r)) by JORDAN2B:29;
r <= abs r by ABSVALUE:11;
then A66: - (abs r) <= - r by XREAL_1:26;
abs r >= 0 by COMPLEX1:132;
then abs r <= (abs r) + (abs r) by XREAL_1:33;
then - (abs r) >= - ((abs r) + (abs r)) by XREAL_1:26;
hence r5 <= - r by A65, A66, XXREAL_0:2; :: thesis: verum

end;

then A67: |[(- ((abs r) + (abs r)))]| in P1 by A14;
A68: |.|[(- ((abs r) + (abs r)))]|.| = abs (- ((abs r) + (abs r))) by Th12
.= abs ((abs r) + (abs r)) by COMPLEX1:138 ;
A69: 0 <= abs r by COMPLEX1:132;
A70: 0 <= abs r by COMPLEX1:132;
then 0 <= (abs r) + (abs r) by A69;
then A71: abs ((abs r) + (abs r)) = (abs r) + (abs r) by ABSVALUE:def 1;
A72: r <= abs r by ABSVALUE:11;
abs r <= (abs r) + (abs r) by A70, XREAL_1:33;
hence contradiction by A64, A67, A68, A71, A72, XXREAL_0:2; :: thesis: verum

end;

A73: now

assume P2 is Bounded ; :: thesis: contradiction
then consider r being Real such that
A74: for q being Point of (TOP-REAL n) st q in P2 holds
|.q.| < r by Th40;
set p3 = |[((abs r) + (abs r))]|;
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 A75: r5 = (abs r) + (abs r) by JORDAN2B:29;
A76: r <= abs r by ABSVALUE:11;
abs r >= 0 by COMPLEX1:132;
then abs r <= (abs r) + (abs r) by XREAL_1:33;
hence r5 >= r by A75, A76, XXREAL_0:2; :: thesis: verum

end;

then A77: |[((abs r) + (abs r))]| in P2 by A14;
A78: |.|[((abs r) + (abs r))]|.| = abs ((abs r) + (abs r)) by Th12;
A79: 0 <= abs r by COMPLEX1:132;
A80: 0 <= abs r by COMPLEX1:132;
then 0 <= (abs r) + (abs r) by A79;
then A81: abs ((abs r) + (abs r)) = (abs r) + (abs r) by ABSVALUE:def 1;
A82: r <= abs r by ABSVALUE:11;
abs r <= (abs r) + (abs r) by A80, XREAL_1:33;
hence contradiction by A74, A77, A78, A81, A82, XXREAL_0:2; :: thesis: verum

end;

A83: Down P1,(A ` ) is connected by A35, A50, Th15;
A84: Down P2,(A ` ) is connected by A36, A62, Th15;

now

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

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

suppose q in P1 ; :: thesis: contradiction

then P1 /\ B4 <> {} ((TOP-REAL n) | (A ` )) by A86, A87, A88, XBOOLE_0:def 4;
then A91: P1 meets B4 by XBOOLE_0:def 7;
B3 is Bounded by A87, Def3;
hence contradiction by A35, A63, A83, A88, A91, Th16, CONNSP_1:38; :: thesis: verum

end;

suppose q in P2 ; :: thesis: contradiction

then P2 /\ B4 <> {} ((TOP-REAL n) | (A ` )) by A86, A87, A88, XBOOLE_0:def 4;
then A92: P2 meets B4 by XBOOLE_0:def 7;
B3 is Bounded by A87, Def3;
hence contradiction by A36, A73, A84, A88, A92, Th16, CONNSP_1:38; :: 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 A93: 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 in the carrier of (TOP-REAL n) ;
then q2 in REAL n by EUCLID:25;
then q2 = 0. (TOP-REAL n) by A93, Th113, TARSKI:def 1;
hence |.q2.| < 1 by TOPRNS_1:24; :: 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;