let n be Nat; :: thesis: for A being Subset of (TOP-REAL n)
for a being Real st n >= 1 & a > 0 & A = { q where q is Point of (TOP-REAL n) : |.q.| = a } holds
BDD A is_inside_component_of A
let A be Subset of (TOP-REAL n); :: thesis: for a being Real st n >= 1 & a > 0 & A = { q where q is Point of (TOP-REAL n) : |.q.| = a } holds
BDD A is_inside_component_of A
let a be Real; :: thesis: ( n >= 1 & a > 0 & A = { q where q is Point of (TOP-REAL n) : |.q.| = a } implies BDD A is_inside_component_of A )
{ q where q is Point of (TOP-REAL n) : |.q.| < a } c= the carrier of (TOP-REAL 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.| < a } or x in the carrier of (TOP-REAL n) )
assume x in { q where q is Point of (TOP-REAL n) : |.q.| < a } ; :: thesis: x in the carrier of (TOP-REAL n)
then ex q being Point of (TOP-REAL n) st
( q = x & |.q.| < a ) ;
hence x in the carrier of (TOP-REAL n) ; :: thesis: verum

end;

then reconsider W = { q where q is Point of (TOP-REAL n) : |.q.| < a } as Subset of (Euclid n) by TOPREAL3:8;
reconsider P = W as Subset of (TOP-REAL n) by TOPREAL3:8;
reconsider P = P as Subset of (TOP-REAL n) ;
A1: the carrier of ((TOP-REAL n) | (A `)) = A ` by PRE_TOPC:8;
then reconsider P1 = Component_of (Down (P,(A `))) as Subset of (TOP-REAL n) by XBOOLE_1:1;
assume A2: ( n >= 1 & a > 0 & A = { q where q is Point of (TOP-REAL n) : |.q.| = a } ) ; :: thesis: BDD A is_inside_component_of A
A3: P c= A `

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P or x in A ` )
assume A4: x in P ; :: thesis: x in A `
then reconsider q = x as Point of (TOP-REAL n) ;
A5: ex q1 being Point of (TOP-REAL n) st
( q1 = q & |.q1.| < a ) by A4;

now :: thesis: not q in A

assume q in A ; :: thesis: contradiction
then ex q2 being Point of (TOP-REAL n) st
( q2 = q & |.q2.| = a ) by A2;
hence contradiction by A5; :: thesis: verum

end;

hence x in A ` by XBOOLE_0:def 5; :: thesis: verum

end;

then A6: Down (P,(A `)) = P by XBOOLE_1:28;
P is convex by Th54;
then (TOP-REAL n) | P is connected by CONNSP_1:def 3;
then ((TOP-REAL n) | (A `)) | (Down (P,(A `))) is connected by A3, A6, PRE_TOPC:7;
then A7: Down (P,(A `)) is connected by CONNSP_1:def 3;
|.(0. (TOP-REAL n)).| = 0 by TOPRNS_1:23;
then A8: 0. (TOP-REAL n) in P by A2;
then reconsider G = A ` as non empty Subset of (TOP-REAL n) by A3;
A9: not (TOP-REAL n) | G is empty ;
A10: P c= Component_of (Down (P,(A `))) by A6, A7, CONNSP_3:13;
A11: Down (P,(A `)) <> {} by A3, A8, XBOOLE_0:def 4;
then A12: Component_of (Down (P,(A `))) is a_component by A9, A7, CONNSP_3:9;
then A13: Component_of (Down (P,(A `))) is connected by CONNSP_1:def 5;
Component_of (Down (P,(A `))) is bounded Subset of (Euclid n)

proof

reconsider D2 = Component_of (Down (P,(A `))) as Subset of (TOP-REAL n) by A1, XBOOLE_1:1;
reconsider D = D2 as Subset of (Euclid n) by TOPREAL3:8;
reconsider D = D as Subset of (Euclid n) ;

now :: thesis: D2 is bounded

reconsider B = A ` as non empty Subset of (TOP-REAL n) by A3, A8;
set p = 0. (TOP-REAL n);
reconsider RR = (TOP-REAL n) | B as non empty TopSpace ;
assume not D2 is bounded ; :: thesis: contradiction
then consider q being Point of (TOP-REAL n) such that
A14: q in D2 and
A15: |.q.| >= a by Th21;
A16: ( A ` is open & D2 is connected ) by A2, A13, Th64, CONNSP_1:23;
D c= the carrier of ((TOP-REAL n) | (A `)) ;
then A17: D2 c= A ` by PRE_TOPC:8;
then A18: D2 = Down (D2,(A `)) by XBOOLE_1:28;
RR is locally_connected by A2, Th66;
then Component_of (Down (P,(A `))) is open by A11, A7, CONNSP_2:15, CONNSP_3:9;
then consider G being Subset of (TOP-REAL n) such that
A19: G is open and
A20: Down (D2,(A `)) = G /\ ([#] ((TOP-REAL n) | (A `))) by A18, TOPS_2:24;
A21: G /\ (A `) = D2 by A18, A20, PRE_TOPC:def 5;
0. (TOP-REAL n) <> q by A2, A15, TOPRNS_1:23;
then consider f1 being Function of I[01],(TOP-REAL n) such that
A22: f1 is continuous and
A23: rng f1 c= D2 and
A24: f1 . 0 = 0. (TOP-REAL n) and
A25: f1 . 1 = q by A8, A10, A14, A19, A21, A16, Th63;
A26: |.(f1 /. 1).| >= a by A15, A25, BORSUK_1:def 15, FUNCT_2:def 13;
|.(0. (TOP-REAL n)).| < a by A2, TOPRNS_1:23;
then |.(f1 /. 0).| < a by A24, BORSUK_1:def 14, FUNCT_2:def 13;
then consider t0 being Point of I[01] such that
A27: |.(f1 /. t0).| = a by A22, A26, Th70;
reconsider q2 = f1 . t0 as Point of (TOP-REAL n) ;
t0 in [#] I[01] ;
then t0 in dom f1 by FUNCT_2:def 1;
then q2 in rng f1 by FUNCT_1:def 3;
then A28: q2 in D2 by A23;
q2 in A by A2, A27;
then A /\ (A `) <> {} the carrier of (TOP-REAL n) by A17, A28, XBOOLE_0:def 4;
then A meets A ` ;
hence contradiction by XBOOLE_1:79; :: thesis: verum

end;

hence Component_of (Down (P,(A `))) is bounded Subset of (Euclid n) by Th5; :: thesis: verum

end;

then A29: P1 is_inside_component_of A by A12, Th7;
A30: P1 c= union { B where B is Subset of (TOP-REAL n) : B is_inside_component_of A }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P1 or x in union { B where B is Subset of (TOP-REAL n) : B is_inside_component_of A } )
assume A31: x in P1 ; :: thesis: x in union { B where B is Subset of (TOP-REAL n) : B is_inside_component_of A }
P1 in { B where B is Subset of (TOP-REAL n) : B is_inside_component_of A } by A29;
hence x in union { B where B is Subset of (TOP-REAL n) : B is_inside_component_of A } by A31, TARSKI:def 4; :: thesis: verum

end;

now :: thesis: ( ( n >= 2 & ex B being Subset of (TOP-REAL n) st
( B is_inside_component_of A & B = BDD A ) ) or ( n < 2 & ex B being Subset of (TOP-REAL n) st
( B is_inside_component_of A & B = BDD A ) ) )

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

case A32: n >= 2 ; :: thesis: ex B being Subset of (TOP-REAL n) st
( B is_inside_component_of A & B = BDD A )

union { B where B is Subset of (TOP-REAL n) : B is_inside_component_of A } c= P1

proof

reconsider E = A ` as non empty Subset of (TOP-REAL n) by A3, A8;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union { B where B is Subset of (TOP-REAL n) : B is_inside_component_of A } or x in P1 )
assume x in union { B where B is Subset of (TOP-REAL n) : B is_inside_component_of A } ; :: thesis: x in P1
then consider y being set such that
A33: x in y and
A34: y in { B where B is Subset of (TOP-REAL n) : B is_inside_component_of A } by TARSKI:def 4;
consider B being Subset of (TOP-REAL n) such that
A35: B = y and
A36: B is_inside_component_of A by A34;
ex C being Subset of ((TOP-REAL n) | (A `)) st
( C = B & C is a_component & C is bounded Subset of (Euclid n) ) by A36, Th7;
then reconsider p = x as Point of ((TOP-REAL n) | (A `)) by A33, A35;
A37: ( the carrier of ((TOP-REAL n) | (A `)) = A ` & p in the carrier of ((TOP-REAL n) | E) ) by PRE_TOPC:8;
then reconsider q2 = p as Point of (TOP-REAL n) ;
not p in A by A37, XBOOLE_0:def 5;
then |.q2.| <> a by A2;
then A38: ( |.q2.| < a or |.q2.| > a ) by XXREAL_0:1;

now :: thesis: ( ( p in { q where q is Point of (TOP-REAL n) : |.q.| > a } & x in P1 ) or ( p in { q1 where q1 is Point of (TOP-REAL n) : |.q1.| < a } & x in P1 ) )

per cases ( p in { q where q is Point of (TOP-REAL n) : |.q.| > a } or p in { q1 where q1 is Point of (TOP-REAL n) : |.q1.| < a } ) by A38;

case A39: p in { q where q is Point of (TOP-REAL n) : |.q.| > a } ; :: thesis: x in P1

{ q where q is Point of (TOP-REAL n) : |.q.| > a } c= A `

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { q where q is Point of (TOP-REAL n) : |.q.| > a } or z in A ` )
assume z in { q where q is Point of (TOP-REAL n) : |.q.| > a } ; :: thesis: z in A `
then consider q being Point of (TOP-REAL n) such that
A40: q = z and
A41: |.q.| > a ;

now :: thesis: not q in A

assume q in A ; :: thesis: contradiction
then ex q2 being Point of (TOP-REAL n) st
( q2 = q & |.q2.| = a ) by A2;
hence contradiction by A41; :: thesis: verum

end;

hence z in A ` by A40, XBOOLE_0:def 5; :: thesis: verum

end;

then reconsider Q = { q where q is Point of (TOP-REAL n) : |.q.| > a } as Subset of ((TOP-REAL n) | (A `)) by PRE_TOPC:8;
reconsider Q = Q as Subset of ((TOP-REAL n) | (A `)) ;
{ q where q is Point of (TOP-REAL n) : |.q.| > a } c= the carrier of (TOP-REAL n)

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { q where q is Point of (TOP-REAL n) : |.q.| > a } or z in the carrier of (TOP-REAL n) )
assume z in { q where q is Point of (TOP-REAL n) : |.q.| > a } ; :: thesis: z in the carrier of (TOP-REAL n)
then ex q being Point of (TOP-REAL n) st
( q = z & |.q.| > a ) ;
hence z in the carrier of (TOP-REAL n) ; :: thesis: verum

end;

then reconsider P2 = { q where q is Point of (TOP-REAL n) : |.q.| > a } as Subset of (TOP-REAL n) ;
P2 is Subset of (Euclid n) by TOPREAL3:8;
then reconsider W2 = { q where q is Point of (TOP-REAL n) : |.q.| > a } as Subset of (Euclid n) ;
P2 is connected by A32, Th38;
then A42: (TOP-REAL n) | P2 is connected by CONNSP_1:def 3;
A43: not W2 is bounded by A32, Th46;

A44: now :: thesis: not W2 meets A

assume W2 meets A ; :: thesis: contradiction
then consider z being object such that
A45: ( z in W2 & z in A ) by XBOOLE_0:3;
( ex q being Point of (TOP-REAL n) st
( q = z & |.q.| > a ) & ex q2 being Point of (TOP-REAL n) st
( q2 = z & |.q2.| = a ) ) by A2, A45;
hence contradiction ; :: thesis: verum

end;

then W2 /\ ((A `) `) = {} ;
then P2 \ (A `) = {} by SUBSET_1:13;
then A46: W2 c= A ` by XBOOLE_1:37;
then Q = Down (P2,(A `)) by XBOOLE_1:28;
then Up (Component_of Q) is_outside_component_of A by A32, A43, A44, Th38, Th48;
then A47: Component_of Q c= UBD A by Th14;
(TOP-REAL n) | P2 = ((TOP-REAL n) | (A `)) | Q by A46, PRE_TOPC:7;
then Q is connected by A42, CONNSP_1:def 3;
then Q c= Component_of Q by CONNSP_3:1;
then A48: p in Component_of Q by A39;
B c= BDD A by A36, Th13;
then p in (BDD A) /\ (UBD A) by A33, A35, A47, A48, XBOOLE_0:def 4;
then BDD A meets UBD A ;
hence x in P1 by Th15; :: thesis: verum

end;

case A49: p in { q1 where q1 is Point of (TOP-REAL n) : |.q1.| < a } ; :: thesis: x in P1

Down (P,(A `)) c= Component_of (Down (P,(A `))) by A7, CONNSP_3:1;
hence x in P1 by A6, A49; :: thesis: verum

end;

end;

end;

hence x in P1 ; :: thesis: verum

end;

then P1 = union { B where B is Subset of (TOP-REAL n) : B is_inside_component_of A } by A30;
hence ex B being Subset of (TOP-REAL n) st
( B is_inside_component_of A & B = BDD A ) by A29; :: thesis: verum

end;

case n < 2 ; :: thesis: ex B being Subset of (TOP-REAL n) st
( B is_inside_component_of A & B = BDD A )

then n < 1 + 1 ;
then A50: n <= 1 by NAT_1:13;
then A51: n = 1 by A2, XXREAL_0:1;
union { B where B is Subset of (TOP-REAL n) : B is_inside_component_of A } c= P1

proof

reconsider E = A ` as non empty Subset of (TOP-REAL n) by A3, A8;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union { B where B is Subset of (TOP-REAL n) : B is_inside_component_of A } or x in P1 )
assume x in union { B where B is Subset of (TOP-REAL n) : B is_inside_component_of A } ; :: thesis: x in P1
then consider y being set such that
A52: x in y and
A53: y in { B where B is Subset of (TOP-REAL n) : B is_inside_component_of A } by TARSKI:def 4;
consider B being Subset of (TOP-REAL n) such that
A54: B = y and
A55: B is_inside_component_of A by A53;
ex C being Subset of ((TOP-REAL n) | (A `)) st
( C = B & C is a_component & C is bounded Subset of (Euclid n) ) by A55, Th7;
then reconsider p = x as Point of ((TOP-REAL n) | (A `)) by A52, A54;
A56: ( the carrier of ((TOP-REAL n) | (A `)) = A ` & p in the carrier of ((TOP-REAL n) | E) ) by PRE_TOPC:8;
then reconsider q2 = p as Point of (TOP-REAL n) ;
not p in A by A56, XBOOLE_0:def 5;
then |.q2.| <> a by A2;
then A57: ( |.q2.| < a or |.q2.| > a ) by XXREAL_0:1;

now :: thesis: ( ( p in { q where q is Point of (TOP-REAL n) : |.q.| > a } & x in P1 ) or ( p in { q1 where q1 is Point of (TOP-REAL n) : |.q1.| < a } & x in P1 ) )

per cases ( p in { q where q is Point of (TOP-REAL n) : |.q.| > a } or p in { q1 where q1 is Point of (TOP-REAL n) : |.q1.| < a } ) by A57;

case p in { q where q is Point of (TOP-REAL n) : |.q.| > a } ; :: thesis: x in P1

then consider q0 being Point of (TOP-REAL n) such that
A58: q0 = p and
A59: |.q0.| > a ;
q0 is Element of REAL n by EUCLID:22;
then consider r0 being Element of REAL such that
A60: q0 = <*r0*> by A51, FINSEQ_2:97;
A61: |.q0.| = |.r0.| by A60, Th71;

A62: now :: thesis: ( p in { q where q is Point of (TOP-REAL n) : ex r being Real st
( q = <*r*> & r > a ) } or p in { q1 where q1 is Point of (TOP-REAL n) : ex r1 being Real st
( q1 = <*r1*> & r1 < - a ) } )

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

suppose r0 >= 0 ; :: thesis: ( p in { q where q is Point of (TOP-REAL n) : ex r being Real st
( q = <*r*> & r > a ) } or p in { q1 where q1 is Point of (TOP-REAL n) : ex r1 being Real st
( q1 = <*r1*> & r1 < - a ) } )

then r0 = |.r0.| by ABSVALUE:def 1;
hence ( p in { q where q is Point of (TOP-REAL n) : ex r being Real st
( q = <*r*> & r > a ) } or p in { q1 where q1 is Point of (TOP-REAL n) : ex r1 being Real st
( q1 = <*r1*> & r1 < - a ) } ) by A58, A59, A60, A61; :: thesis: verum

end;

suppose r0 < 0 ; :: thesis: ( p in { q where q is Point of (TOP-REAL n) : ex r being Real st
( q = <*r*> & r > a ) } or p in { q1 where q1 is Point of (TOP-REAL n) : ex r1 being Real st
( q1 = <*r1*> & r1 < - a ) } )

then - r0 > a by A59, A61, ABSVALUE:def 1;
then - (- r0) < - a by XREAL_1:24;
hence ( p in { q where q is Point of (TOP-REAL n) : ex r being Real st
( q = <*r*> & r > a ) } or p in { q1 where q1 is Point of (TOP-REAL n) : ex r1 being Real st
( q1 = <*r1*> & r1 < - a ) } ) by A58, A60; :: thesis: verum

end;

end;

end;

now :: thesis: x in P1

per cases ( p in { q where q is Point of (TOP-REAL n) : ex r being Real st
( q = <*r*> & r > a ) } or p in { q1 where q1 is Point of (TOP-REAL n) : ex r1 being Real st
( q1 = <*r1*> & r1 < - a ) } ) by A62;

suppose A63: p in { q where q is Point of (TOP-REAL n) : ex r being Real st
( q = <*r*> & r > a ) } ; :: thesis: x in P1

{ q where q is Point of (TOP-REAL n) : ex r being Real st
( q = <*r*> & r > a ) } c= A `

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { q where q is Point of (TOP-REAL n) : ex r being Real st
( q = <*r*> & r > a ) } or z in A ` )
assume z in { q where q is Point of (TOP-REAL n) : ex r being Real st
( q = <*r*> & r > a ) } ; :: thesis: z in A `
then consider q being Point of (TOP-REAL n) such that
A64: q = z and
A65: ex r being Real st
( q = <*r*> & r > a ) ;
consider r being Real such that
A66: q = <*r*> and
A67: r > a by A65;
reconsider rr = r as Element of REAL by XREAL_0:def 1;
n = 1 by A2, A50, XXREAL_0:1;
then reconsider xr = <*rr*> as Element of REAL n ;
len xr = 1 by FINSEQ_1:39;
then A68: q /. 1 = xr . 1 by A66, FINSEQ_4:15;
then A69: (sqr xr) . 1 = (q /. 1) ^2 by VALUED_1:11;
A70: sqrt ((q /. 1) ^2) = |.(q /. 1).| by COMPLEX1:72
.= |.r.| by A68 ;
reconsider qk = (q /. 1) ^2 as Element of REAL by XREAL_0:def 1;
len (sqr xr) = 1 by A51, CARD_1:def 7;
then sqr xr = <*qk*> by A69, FINSEQ_1:40;
then A71: |.q.| = |.r.| by A66, A70, FINSOP_1:11
.= r by A2, A67, ABSVALUE:def 1 ;

now :: thesis: not q in A

assume q in A ; :: thesis: contradiction
then ex q2 being Point of (TOP-REAL n) st
( q2 = q & |.q2.| = a ) by A2;
hence contradiction by A67, A71; :: thesis: verum

end;

hence z in A ` by A64, XBOOLE_0:def 5; :: thesis: verum

end;

then reconsider Q = { q where q is Point of (TOP-REAL n) : ex r being Real st
( q = <*r*> & r > a ) } as Subset of ((TOP-REAL n) | (A `)) by PRE_TOPC:8;
{ q where q is Point of (TOP-REAL n) : ex r being Real st
( q = <*r*> & r > a ) } c= the carrier of (TOP-REAL n)

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { q where q is Point of (TOP-REAL n) : ex r being Real st
( q = <*r*> & r > a ) } or z in the carrier of (TOP-REAL n) )
assume z in { q where q is Point of (TOP-REAL n) : ex r being Real st
( q = <*r*> & r > a ) } ; :: thesis: z in the carrier of (TOP-REAL n)
then ex q being Point of (TOP-REAL n) st
( q = z & ex r being Real st
( q = <*r*> & r > a ) ) ;
hence z in the carrier of (TOP-REAL n) ; :: thesis: verum

end;

then reconsider P3 = { q where q is Point of (TOP-REAL n) : ex r being Real st
( q = <*r*> & r > a ) } as Subset of (TOP-REAL n) ;
reconsider W3 = P3 as Subset of (Euclid n) by TOPREAL3:8;
reconsider Q = Q as Subset of ((TOP-REAL n) | (A `)) ;
{ q where q is Point of (TOP-REAL n) : |.q.| > a } c= the carrier of (TOP-REAL n)

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { q where q is Point of (TOP-REAL n) : |.q.| > a } or z in the carrier of (TOP-REAL n) )
assume z in { q where q is Point of (TOP-REAL n) : |.q.| > a } ; :: thesis: z in the carrier of (TOP-REAL n)
then ex q being Point of (TOP-REAL n) st
( q = z & |.q.| > a ) ;
hence z in the carrier of (TOP-REAL n) ; :: thesis: verum

end;

then reconsider P2 = { q where q is Point of (TOP-REAL n) : |.q.| > a } as Subset of (TOP-REAL n) ;
P2 is Subset of (Euclid n) by TOPREAL3:8;
then reconsider W2 = { q where q is Point of (TOP-REAL n) : |.q.| > a } as Subset of (Euclid n) ;
A72: W3 c= W2

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in W3 or z in W2 )
assume z in W3 ; :: thesis: z in W2
then consider q being Point of (TOP-REAL n) such that
A73: q = z and
A74: ex r being Real st
( q = <*r*> & r > a ) ;
consider r being Real such that
A75: q = <*r*> and
A76: r > a by A74;
A77: r = |.r.| by A2, A76, ABSVALUE:def 1;
reconsider rr = r as Element of REAL by XREAL_0:def 1;
n = 1 by A2, A50, XXREAL_0:1;
then reconsider xr = <*rr*> as Element of REAL n ;
len xr = 1 by FINSEQ_1:39;
then A78: q /. 1 = xr . 1 by A75, FINSEQ_4:15;
then A79: (sqr xr) . 1 = (q /. 1) ^2 by VALUED_1:11;
reconsider qk = (q /. 1) ^2 as Element of REAL by XREAL_0:def 1;
len (sqr xr) = 1 by A51, CARD_1:def 7;
then A80: sqr xr = <*qk*> by A79, FINSEQ_1:40;
sqrt ((q /. 1) ^2) = |.(q /. 1).| by COMPLEX1:72
.= |.r.| by A78 ;
then |.xr.| = |.rr.| by A80, FINSOP_1:11;
then |.q.| = |.r.| by A75;
hence z in W2 by A73, A76, A77; :: thesis: verum

end;

A81: now :: thesis: W2 /\ A = {}

set z = the Element of W2 /\ A;
assume A82: not W2 /\ A = {} ; :: thesis: contradiction
then the Element of W2 /\ A in W2 by XBOOLE_0:def 4;
then A83: ex q being Point of (TOP-REAL n) st
( q = the Element of W2 /\ A & |.q.| > a ) ;
the Element of W2 /\ A in A by A82, XBOOLE_0:def 4;
then ex q2 being Point of (TOP-REAL n) st
( q2 = the Element of W2 /\ A & |.q2.| = a ) by A2;
hence contradiction by A83; :: thesis: verum

end;

then W3 /\ A = {} by A72, XBOOLE_1:3, XBOOLE_1:26;
then A84: W3 misses A ;
W3 /\ ((A `) `) = {} by A81, A72, XBOOLE_1:3, XBOOLE_1:26;
then W3 \ (A `) = {} by SUBSET_1:13;
then A85: W3 c= A ` by XBOOLE_1:37;
then A86: (TOP-REAL n) | P3 = ((TOP-REAL n) | (A `)) | Q by PRE_TOPC:7;
A87: P3 is convex by A51, Th42;
then (TOP-REAL n) | P3 is connected by CONNSP_1:def 3;
then Q is connected by A86, CONNSP_1:def 3;
then Q c= Component_of Q by CONNSP_3:1;
then A88: p in Component_of Q by A63;
A89: Q = Down (P3,(A `)) by A85, XBOOLE_1:28;
not W3 is bounded by A51, Th44;
then Up (Component_of Q) is_outside_component_of A by A87, A84, A89, Th48;
then A90: Component_of Q c= UBD A by Th14;
B c= BDD A by A55, Th13;
then (BDD A) /\ (UBD A) <> {} by A52, A54, A90, A88, XBOOLE_0:def 4;
then BDD A meets UBD A ;
hence x in P1 by Th15; :: thesis: verum

end;

suppose A91: p in { q1 where q1 is Point of (TOP-REAL n) : ex r1 being Real st
( q1 = <*r1*> & r1 < - a ) } ; :: thesis: x in P1

{ q where q is Point of (TOP-REAL n) : ex r being Real st
( q = <*r*> & r < - a ) } c= A `

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { q where q is Point of (TOP-REAL n) : ex r being Real st
( q = <*r*> & r < - a ) } or z in A ` )
assume z in { q where q is Point of (TOP-REAL n) : ex r being Real st
( q = <*r*> & r < - a ) } ; :: thesis: z in A `
then consider q being Point of (TOP-REAL n) such that
A92: q = z and
A93: ex r being Real st
( q = <*r*> & r < - a ) ;
consider r being Real such that
A94: q = <*r*> and
A95: r < - a by A93;
A96: r < - 0 by A2, A95;
reconsider rr = r as Element of REAL by XREAL_0:def 1;
n = 1 by A2, A50, XXREAL_0:1;
then reconsider xr = <*rr*> as Element of REAL n ;
len xr = 1 by FINSEQ_1:39;
then A97: q /. 1 = xr . 1 by A94, FINSEQ_4:15;
then A98: (sqr xr) . 1 = (q /. 1) ^2 by VALUED_1:11;
reconsider qk = (q /. 1) ^2 as Element of REAL by XREAL_0:def 1;
len (sqr xr) = 1 by A51, CARD_1:def 7;
then A99: sqr xr = <*qk*> by A98, FINSEQ_1:40;
sqrt ((q /. 1) ^2) = |.(q /. 1).| by COMPLEX1:72
.= |.r.| by A97 ;
then A100: |.q.| = |.r.| by A94, A99, FINSOP_1:11
.= - r by A96, ABSVALUE:def 1 ;

now :: thesis: not q in A

assume q in A ; :: thesis: contradiction
then ex q2 being Point of (TOP-REAL n) st
( q2 = q & |.q2.| = a ) by A2;
hence contradiction by A95, A100; :: thesis: verum

end;

hence z in A ` by A92, XBOOLE_0:def 5; :: thesis: verum

end;

then reconsider Q = { q where q is Point of (TOP-REAL n) : ex r being Real st
( q = <*r*> & r < - a ) } as Subset of ((TOP-REAL n) | (A `)) by PRE_TOPC:8;
{ q where q is Point of (TOP-REAL n) : ex r being Real st
( q = <*r*> & r < - a ) } c= the carrier of (TOP-REAL n)

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { q where q is Point of (TOP-REAL n) : ex r being Real st
( q = <*r*> & r < - a ) } or z in the carrier of (TOP-REAL n) )
assume z in { q where q is Point of (TOP-REAL n) : ex r being Real st
( q = <*r*> & r < - a ) } ; :: thesis: z in the carrier of (TOP-REAL n)
then ex q being Point of (TOP-REAL n) st
( q = z & ex r being Real st
( q = <*r*> & r < - a ) ) ;
hence z in the carrier of (TOP-REAL n) ; :: thesis: verum

end;

then reconsider P3 = { q where q is Point of (TOP-REAL n) : ex r being Real st
( q = <*r*> & r < - a ) } as Subset of (TOP-REAL n) ;
reconsider W3 = P3 as Subset of (Euclid n) by TOPREAL3:8;
reconsider Q = Q as Subset of ((TOP-REAL n) | (A `)) ;
{ q where q is Point of (TOP-REAL n) : |.q.| > a } c= the carrier of (TOP-REAL n)

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { q where q is Point of (TOP-REAL n) : |.q.| > a } or z in the carrier of (TOP-REAL n) )
assume z in { q where q is Point of (TOP-REAL n) : |.q.| > a } ; :: thesis: z in the carrier of (TOP-REAL n)
then ex q being Point of (TOP-REAL n) st
( q = z & |.q.| > a ) ;
hence z in the carrier of (TOP-REAL n) ; :: thesis: verum

end;

then reconsider P2 = { q where q is Point of (TOP-REAL n) : |.q.| > a } as Subset of (TOP-REAL n) ;
P2 is Subset of (Euclid n) by TOPREAL3:8;
then reconsider W2 = { q where q is Point of (TOP-REAL n) : |.q.| > a } as Subset of (Euclid n) ;
A101: W3 c= W2

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in W3 or z in W2 )
assume z in W3 ; :: thesis: z in W2
then consider q being Point of (TOP-REAL n) such that
A102: q = z and
A103: ex r being Real st
( q = <*r*> & r < - a ) ;
consider r being Real such that
A104: q = <*r*> and
A105: r < - a by A103;
A106: ( r < - 0 & - r > - (- a) ) by A2, A105, XREAL_1:24;
reconsider rr = r as Element of REAL by XREAL_0:def 1;
n = 1 by A2, A50, XXREAL_0:1;
then reconsider xr = <*rr*> as Element of REAL n ;
len xr = 1 by FINSEQ_1:39;
then A107: q /. 1 = xr . 1 by A104, FINSEQ_4:15;
then A108: (sqr xr) . 1 = (q /. 1) ^2 by VALUED_1:11;
reconsider qk = (q /. 1) ^2 as Element of REAL by XREAL_0:def 1;
len (sqr xr) = 1 by A51, CARD_1:def 7;
then A109: sqr xr = <*qk*> by A108, FINSEQ_1:40;
sqrt ((q /. 1) ^2) = |.(q /. 1).| by COMPLEX1:72
.= |.r.| by A107 ;
then |.q.| = |.r.| by A104, A109, FINSOP_1:11;
then |.q.| > a by A106, ABSVALUE:def 1;
hence z in W2 by A102; :: thesis: verum

end;

A110: now :: thesis: W2 /\ A = {}

set z = the Element of W2 /\ A;
assume A111: not W2 /\ A = {} ; :: thesis: contradiction
then the Element of W2 /\ A in W2 by XBOOLE_0:def 4;
then A112: ex q being Point of (TOP-REAL n) st
( q = the Element of W2 /\ A & |.q.| > a ) ;
the Element of W2 /\ A in A by A111, XBOOLE_0:def 4;
then ex q2 being Point of (TOP-REAL n) st
( q2 = the Element of W2 /\ A & |.q2.| = a ) by A2;
hence contradiction by A112; :: thesis: verum

end;

then W3 /\ A = {} by A101, XBOOLE_1:3, XBOOLE_1:26;
then A113: W3 misses A ;
W3 /\ ((A `) `) = {} by A110, A101, XBOOLE_1:3, XBOOLE_1:26;
then W3 \ (A `) = {} by SUBSET_1:13;
then A114: W3 c= A ` by XBOOLE_1:37;
then A115: (TOP-REAL n) | P3 = ((TOP-REAL n) | (A `)) | Q by PRE_TOPC:7;
A116: P3 is convex by A51, Th43;
then (TOP-REAL n) | P3 is connected by CONNSP_1:def 3;
then Q is connected by A115, CONNSP_1:def 3;
then Q c= Component_of Q by CONNSP_3:1;
then A117: p in Component_of Q by A91;
A118: Q = Down (P3,(A `)) by A114, XBOOLE_1:28;
Up (Component_of Q) is_outside_component_of A by A116, A113, A118, Th48, A51, Th45;
then A119: Component_of Q c= UBD A by Th14;
B c= BDD A by A55, Th13;
then p in (BDD A) /\ (UBD A) by A52, A54, A119, A117, XBOOLE_0:def 4;
then BDD A meets UBD A ;
hence x in P1 by Th15; :: thesis: verum

end;

end;

end;

hence x in P1 ; :: thesis: verum

end;

case A120: p in { q1 where q1 is Point of (TOP-REAL n) : |.q1.| < a } ; :: thesis: x in P1

Down (P,(A `)) c= Component_of (Down (P,(A `))) by A7, CONNSP_3:1;
hence x in P1 by A6, A120; :: thesis: verum

end;

end;

end;

hence x in P1 ; :: thesis: verum

end;

then P1 = union { B where B is Subset of (TOP-REAL n) : B is_inside_component_of A } by A30;
hence ex B being Subset of (TOP-REAL n) st
( B is_inside_component_of A & B = BDD A ) by A29; :: thesis: verum

end;

end;

end;

hence BDD A is_inside_component_of A ; :: thesis: verum