let n be Element of 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 )
assume A1: ( n >= 1 & a > 0 & A = { q where q is Point of (TOP-REAL n) : |.q.| = a } ) ; :: thesis: 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 set ; :: 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 consider q being Point of (TOP-REAL n) such that
A2: ( q = x & |.q.| < a ) ;
thus x in the carrier of (TOP-REAL n) by A2; :: thesis: verum

end;

then reconsider W = { q where q is Point of (TOP-REAL n) : |.q.| < a } as Subset of (Euclid n) by TOPREAL3:13;
reconsider P = W as Subset of (TOP-REAL n) by TOPREAL3:13;
reconsider P = P as Subset of (TOP-REAL n) ;
A3: the carrier of ((TOP-REAL n) | (A ` )) = A ` by PRE_TOPC:29;
then reconsider P1 = Component_of (Down P,(A ` )) as Subset of (TOP-REAL n) by XBOOLE_1:1;
A4: P c= A `

proof

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

now

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

end;

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

end;

|.(0. (TOP-REAL n)).| = 0 by TOPRNS_1:24;
then A7: 0. (TOP-REAL n) in P by A1;
then reconsider G = A ` as non empty Subset of (TOP-REAL n) by A4;
A8: not (TOP-REAL n) | G is empty ;
A9: Down P,(A ` ) <> {} by A4, A7, XBOOLE_0:def 4;
A10: Down P,(A ` ) = P by A4, XBOOLE_1:28;
P is connected by Th77, JORDAN1:9;
then (TOP-REAL n) | P is connected by CONNSP_1:def 3;
then ((TOP-REAL n) | (A ` )) | (Down P,(A ` )) is connected by A4, A10, PRE_TOPC:28;
then A11: Down P,(A ` ) is connected by CONNSP_1:def 3;
then A12: Component_of (Down P,(A ` )) is_a_component_of (TOP-REAL n) | (A ` ) by A8, A9, CONNSP_3:9;
then A13: Component_of (Down P,(A ` )) is connected by CONNSP_1:def 5;
A14: P c= Component_of (Down P,(A ` )) by A7, A8, A10, A11, CONNSP_3:13;
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 A3, XBOOLE_1:1;
reconsider D = D2 as Subset of (Euclid n) by TOPREAL3:13;
reconsider D = D as Subset of (Euclid n) ;

now

assume not D2 is Bounded ; :: thesis: contradiction
then consider q being Point of (TOP-REAL n) such that
A15: ( q in D2 & |.q.| >= a ) by Th40;
set p = 0. (TOP-REAL n);
A16: |.(0. (TOP-REAL n)).| < a by A1, TOPRNS_1:24;
A17: 0. (TOP-REAL n) <> q by A1, A15, TOPRNS_1:24;
D c= the carrier of ((TOP-REAL n) | (A ` )) ;
then A18: D2 c= A ` by PRE_TOPC:29;
then A19: D2 = Down D2,(A ` ) by XBOOLE_1:28;
reconsider B = A ` as non empty Subset of (TOP-REAL n) by A4, A7;
reconsider RR = (TOP-REAL n) | B as non empty TopSpace ;
RR is locally_connected by A1, Th90;
then Component_of (Down P,(A ` )) is open by A9, A11, CONNSP_2:21, CONNSP_3:9;
then consider G being Subset of (TOP-REAL n) such that
A20: ( G is open & Down D2,(A ` ) = G /\ ([#] ((TOP-REAL n) | (A ` ))) ) by A19, TOPS_2:32;
A21: G /\ (A ` ) = D2 by A19, A20, PRE_TOPC:def 10;
A ` is open by A1, Th88;
then ( D2 is connected & D2 is open ) by A13, A20, A21, CONNSP_1:24, TOPS_1:38;
then consider f1 being Function of I[01] ,(TOP-REAL n) such that
A22: ( f1 is continuous & rng f1 c= D2 & f1 . 0 = 0. (TOP-REAL n) & f1 . 1 = q ) by A7, A14, A15, A17, Th87;
A23: |.(pi f1,0 ).| < a by A16, A22, Def10, BORSUK_1:def 17;
|.(pi f1,1).| >= a by A15, A22, Def10, BORSUK_1:def 18;
then consider t0 being Point of I[01] such that
A24: |.(pi f1,t0).| = a by A22, A23, Th94;
reconsider q2 = f1 . t0 as Point of (TOP-REAL n) ;
A25: q2 in A by A1, A24;
t0 in [#] I[01] ;
then t0 in dom f1 by FUNCT_2:def 1;
then q2 in rng f1 by FUNCT_1:def 5;
then q2 in D2 by A22;
then A /\ (A ` ) <> {} the carrier of (TOP-REAL n) by A18, A25, XBOOLE_0:def 4;
then A meets A ` by XBOOLE_0:def 7;
hence contradiction by XBOOLE_1:79; :: thesis: verum

end;

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

end;

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

proof

let x be set ; :: 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 A28: 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 A26;
hence x in union { B where B is Subset of (TOP-REAL n) : B is_inside_component_of A } by A28, TARSKI:def 4; :: thesis: verum

end;

now

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

case A29: 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

let x be set ; :: 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
A30: ( x in y & 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
A31: ( B = y & B is_inside_component_of A ) by A30;
A32: the carrier of ((TOP-REAL n) | (A ` )) = A ` by PRE_TOPC:29;
consider C being Subset of ((TOP-REAL n) | (A ` )) such that
A33: ( C = B & C is_a_component_of (TOP-REAL n) | (A ` ) & C is bounded Subset of (Euclid n) ) by A31, Th17;
reconsider p = x as Point of ((TOP-REAL n) | (A ` )) by A30, A31, A33;
reconsider E = A ` as non empty Subset of (TOP-REAL n) by A4, A7;
A34: p in the carrier of ((TOP-REAL n) | E) ;
then A35: ( p in the carrier of (TOP-REAL n) & not p in A ) by A32, XBOOLE_0:def 5;
reconsider q2 = p as Point of (TOP-REAL n) by A32, A34;
|.q2.| <> a by A1, A35;
then A36: ( |.q2.| < a or |.q2.| > a ) by XXREAL_0:1;

now

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 A36;

case A37: 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 set ; :: 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
A38: ( q = z & |.q.| > a ) ;

now

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

end;

hence z in A ` by A38, 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:29;
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 set ; :: 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 consider q being Point of (TOP-REAL n) such that
A39: ( q = z & |.q.| > a ) ;
thus z in the carrier of (TOP-REAL n) by A39; :: 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 connected by A29, Th59;
then A40: (TOP-REAL n) | P2 is connected by CONNSP_1:def 3;
P2 is Subset of (Euclid n) by TOPREAL3:13;
then reconsider W2 = { q where q is Point of (TOP-REAL n) : |.q.| > a } as Subset of (Euclid n) ;
P2 = W2 ;
then A41: not W2 is bounded by A29, Th69;

A42: now

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

end;

then W2 /\ ((A ` ) ` ) = {} by XBOOLE_0:def 7;
then P2 \ (A ` ) = {} by SUBSET_1:32;
then A45: W2 c= A ` by XBOOLE_1:37;
then (TOP-REAL n) | P2 = ((TOP-REAL n) | (A ` )) | Q by PRE_TOPC:28;
then A46: Q is connected by A40, CONNSP_1:def 3;
Q = Down P2,(A ` ) by A45, XBOOLE_1:28;
then Up (Component_of Q) is_outside_component_of A by A29, A41, A42, Th59, Th71;
then A47: Component_of Q c= UBD A by Th27;
Q c= Component_of Q by A46, CONNSP_3:1;
then A48: p in Component_of Q by A37;
B c= BDD A by A31, Th26;
then p in (BDD A) /\ (UBD A) by A30, A31, A47, A48, XBOOLE_0:def 4;
then BDD A meets UBD A by XBOOLE_0:4;
hence x in P1 by Th28; :: 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 A11, CONNSP_3:1;
hence x in P1 by A10, 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 A27, XBOOLE_0:def 10;
hence ex B being Subset of (TOP-REAL n) st
( B is_inside_component_of A & B = BDD A ) by A26; :: 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 A1, XXREAL_0:1;
union { B where B is Subset of (TOP-REAL n) : B is_inside_component_of A } c= P1

proof

let x be set ; :: 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 & 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
A53: ( B = y & B is_inside_component_of A ) by A52;
A54: the carrier of ((TOP-REAL n) | (A ` )) = A ` by PRE_TOPC:29;
consider C being Subset of ((TOP-REAL n) | (A ` )) such that
A55: ( C = B & C is_a_component_of (TOP-REAL n) | (A ` ) & C is bounded Subset of (Euclid n) ) by A53, Th17;
reconsider p = x as Point of ((TOP-REAL n) | (A ` )) by A52, A53, A55;
reconsider E = A ` as non empty Subset of (TOP-REAL n) by A4, A7;
A56: p in the carrier of ((TOP-REAL n) | E) ;
then A57: ( p in the carrier of (TOP-REAL n) & not p in A ) by A54, XBOOLE_0:def 5;
reconsider q2 = p as Point of (TOP-REAL n) by A54, A56;
|.q2.| <> a by A1, A57;
then A58: ( |.q2.| < a or |.q2.| > a ) by XXREAL_0:1;

now

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 A58;

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
A59: ( q0 = p & |.q0.| > a ) ;
q0 is Element of REAL n by EUCLID:25;
then q0 is Element of n -tuples_on REAL by EUCLID:25;
then consider r0 being Real such that
A60: q0 = <*r0*> by A51, FINSEQ_2:117;
A61: |.q0.| = abs r0 by A60, Th95;

A62: now

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

case 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 = abs 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 A59, A60, A61; :: thesis: verum

end;

case 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:26;
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 A59, A60; :: thesis: verum

end;

end;

end;

now

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;

case 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 set ; :: 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 & ex r being Real st
( q = <*r*> & r > a ) ) ;
consider r being Real such that
A65: ( q = <*r*> & r > a ) by A64;
reconsider xr = <*r*> as Element of REAL n by A1, A50, XXREAL_0:1;
len xr = 1 by FINSEQ_1:56;
then xr . 1 = xr /. 1 by FINSEQ_4:24;
then A66: Proj q,1 = xr . 1 by A65, JORDAN2B:def 1;
A67: len (sqr xr) = 1 by A51, FINSEQ_1:def 18;
(sqr xr) . 1 = (Proj q,1) ^2 by A66, VALUED_1:11;
then A68: sqr xr = <*((Proj q,1) ^2 )*> by A67, FINSEQ_1:57;
sqrt ((Proj q,1) ^2 ) = abs (Proj q,1) by COMPLEX1:158
.= abs r by A66, FINSEQ_1:57 ;
then A69: |.q.| = abs r by A65, A68, FINSOP_1:12
.= r by A1, A65, ABSVALUE:def 1 ;

now

assume q in A ; :: thesis: contradiction
then ex q2 being Point of (TOP-REAL n) st
( q2 = q & |.q2.| = a ) by A1;
hence contradiction by A65, A69; :: 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:29;
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 set ; :: 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 consider q being Point of (TOP-REAL n) such that
A70: ( q = z & |.q.| > a ) ;
thus z in the carrier of (TOP-REAL n) by A70; :: thesis: verum

end;

then reconsider P2 = { q where q is Point of (TOP-REAL n) : |.q.| > a } as Subset of (TOP-REAL n) ;
{ 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 set ; :: 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 consider q being Point of (TOP-REAL n) such that
A71: ( q = z & ex r being Real st
( q = <*r*> & r > a ) ) ;
thus z in the carrier of (TOP-REAL n) by A71; :: 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) ;
P2 is Subset of (Euclid n) by TOPREAL3:13;
then reconsider W2 = { q where q is Point of (TOP-REAL n) : |.q.| > a } as Subset of (Euclid n) ;
reconsider W3 = P3 as Subset of (Euclid n) by TOPREAL3:13;
W3 = P3 ;
then A72: P3 is connected by A51, Th67;
then A73: (TOP-REAL n) | P3 is connected by CONNSP_1:def 3;
A74: not W3 is bounded by A51, Th67;

A75: now

assume A76: not W2 /\ A = {} ; :: thesis: contradiction
consider z being Element of W2 /\ A;
A77: ( z in W2 & z in A ) by A76, XBOOLE_0:def 4;
then A78: 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 A1, A77;
hence contradiction by A78; :: thesis: verum

end;

A79: W3 c= W2

proof

let z be set ; :: 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
A80: ( q = z & ex r being Real st
( q = <*r*> & r > a ) ) ;
consider r being Real such that
A81: ( q = <*r*> & r > a ) by A80;
reconsider xr = <*r*> as Element of REAL n by A1, A50, XXREAL_0:1;
len xr = 1 by FINSEQ_1:56;
then xr . 1 = xr /. 1 by FINSEQ_4:24;
then A82: Proj q,1 = xr . 1 by A81, JORDAN2B:def 1;
A83: len (sqr xr) = 1 by A51, FINSEQ_1:def 18;
(sqr xr) . 1 = (Proj q,1) ^2 by A82, VALUED_1:11;
then A84: sqr xr = <*((Proj q,1) ^2 )*> by A83, FINSEQ_1:57;
sqrt ((Proj q,1) ^2 ) = abs (Proj q,1) by COMPLEX1:158
.= abs r by A82, FINSEQ_1:57 ;
then A85: |.q.| = abs r by A81, A84, FINSOP_1:12;
r = abs r by A1, A81, ABSVALUE:def 1;
hence z in W2 by A80, A81, A85; :: thesis: verum

end;

then W3 /\ A = {} by A75, XBOOLE_1:3, XBOOLE_1:26;
then A86: W3 misses A by XBOOLE_0:def 7;
W3 /\ ((A ` ) ` ) = {} by A75, A79, XBOOLE_1:3, XBOOLE_1:26;
then W3 \ (A ` ) = {} by SUBSET_1:32;
then A87: W3 c= A ` by XBOOLE_1:37;
then (TOP-REAL n) | P3 = ((TOP-REAL n) | (A ` )) | Q by PRE_TOPC:28;
then A88: Q is connected by A73, CONNSP_1:def 3;
Q = Down P3,(A ` ) by A87, XBOOLE_1:28;
then Up (Component_of Q) is_outside_component_of A by A72, A74, A86, Th71;
then A89: Component_of Q c= UBD A by Th27;
Q c= Component_of Q by A88, CONNSP_3:1;
then A90: p in Component_of Q by A63;
B c= BDD A by A53, Th26;
then (BDD A) /\ (UBD A) <> {} by A52, A53, A89, A90, XBOOLE_0:def 4;
then BDD A meets UBD A by XBOOLE_0:def 7;
hence x in P1 by Th28; :: thesis: verum

end;

case 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 set ; :: 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 & ex r being Real st
( q = <*r*> & r < - a ) ) ;
consider r being Real such that
A93: ( q = <*r*> & r < - a ) by A92;
A94: r < - 0 by A1, A93;
reconsider xr = <*r*> as Element of REAL n by A1, A50, XXREAL_0:1;
len xr = 1 by FINSEQ_1:56;
then xr . 1 = xr /. 1 by FINSEQ_4:24;
then A95: Proj q,1 = xr . 1 by A93, JORDAN2B:def 1;
A96: len (sqr xr) = 1 by A51, FINSEQ_1:def 18;
(sqr xr) . 1 = (Proj q,1) ^2 by A95, VALUED_1:11;
then A97: sqr xr = <*((Proj q,1) ^2 )*> by A96, FINSEQ_1:57;
sqrt ((Proj q,1) ^2 ) = abs (Proj q,1) by COMPLEX1:158
.= abs r by A95, FINSEQ_1:57 ;
then A98: |.q.| = abs r by A93, A97, FINSOP_1:12
.= - r by A94, ABSVALUE:def 1 ;

now

assume q in A ; :: thesis: contradiction
then ex q2 being Point of (TOP-REAL n) st
( q2 = q & |.q2.| = a ) by A1;
hence contradiction by A93, A98; :: 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:29;
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 set ; :: 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 consider q being Point of (TOP-REAL n) such that
A99: ( q = z & |.q.| > a ) ;
thus z in the carrier of (TOP-REAL n) by A99; :: thesis: verum

end;

then reconsider P2 = { q where q is Point of (TOP-REAL n) : |.q.| > a } as Subset of (TOP-REAL n) ;
{ 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 set ; :: 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 consider q being Point of (TOP-REAL n) such that
A100: ( q = z & ex r being Real st
( q = <*r*> & r < - a ) ) ;
thus z in the carrier of (TOP-REAL n) by A100; :: 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) ;
P2 is Subset of (Euclid n) by TOPREAL3:13;
then reconsider W2 = { q where q is Point of (TOP-REAL n) : |.q.| > a } as Subset of (Euclid n) ;
reconsider W3 = P3 as Subset of (Euclid n) by TOPREAL3:13;
W3 = P3 ;
then A101: P3 is connected by A51, Th68;
then A102: (TOP-REAL n) | P3 is connected by CONNSP_1:def 3;
A103: not W3 is bounded by A51, Th68;

A104: now

assume A105: not W2 /\ A = {} ; :: thesis: contradiction
consider z being Element of W2 /\ A;
A106: ( z in W2 & z in A ) by A105, XBOOLE_0:def 4;
then A107: 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 A1, A106;
hence contradiction by A107; :: thesis: verum

end;

A108: W3 c= W2

proof

let z be set ; :: 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
A109: ( q = z & ex r being Real st
( q = <*r*> & r < - a ) ) ;
consider r being Real such that
A110: ( q = <*r*> & r < - a ) by A109;
A111: r < - 0 by A1, A110;
A112: - r > - (- a) by A110, XREAL_1:26;
reconsider xr = <*r*> as Element of REAL n by A1, A50, XXREAL_0:1;
len xr = 1 by FINSEQ_1:56;
then xr . 1 = xr /. 1 by FINSEQ_4:24;
then A113: Proj q,1 = xr . 1 by A110, JORDAN2B:def 1;
A114: len (sqr xr) = 1 by A51, FINSEQ_1:def 18;
(sqr xr) . 1 = (Proj q,1) ^2 by A113, VALUED_1:11;
then A115: sqr xr = <*((Proj q,1) ^2 )*> by A114, FINSEQ_1:57;
sqrt ((Proj q,1) ^2 ) = abs (Proj q,1) by COMPLEX1:158
.= abs r by A113, FINSEQ_1:57 ;
then |.q.| = abs r by A110, A115, FINSOP_1:12;
then |.q.| > a by A111, A112, ABSVALUE:def 1;
hence z in W2 by A109; :: thesis: verum

end;

then W3 /\ A = {} by A104, XBOOLE_1:3, XBOOLE_1:26;
then A116: W3 misses A by XBOOLE_0:def 7;
W3 /\ ((A ` ) ` ) = {} by A104, A108, XBOOLE_1:3, XBOOLE_1:26;
then W3 \ (A ` ) = {} by SUBSET_1:32;
then A117: W3 c= A ` by XBOOLE_1:37;
then (TOP-REAL n) | P3 = ((TOP-REAL n) | (A ` )) | Q by PRE_TOPC:28;
then A118: Q is connected by A102, CONNSP_1:def 3;
Q = Down P3,(A ` ) by A117, XBOOLE_1:28;
then Up (Component_of Q) is_outside_component_of A by A101, A103, A116, Th71;
then A119: Component_of Q c= UBD A by Th27;
Q c= Component_of Q by A118, CONNSP_3:1;
then A120: p in Component_of Q by A91;
B c= BDD A by A53, Th26;
then p in (BDD A) /\ (UBD A) by A52, A53, A119, A120, XBOOLE_0:def 4;
then BDD A meets UBD A by XBOOLE_0:def 7;
hence x in P1 by Th28; :: thesis: verum

end;

end;

end;

hence x in P1 ; :: thesis: verum

end;

case A121: 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 A11, CONNSP_3:1;
hence x in P1 by A10, A121; :: 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 A27, XBOOLE_0:def 10;
hence ex B being Subset of (TOP-REAL n) st
( B is_inside_component_of A & B = BDD A ) by A26; :: thesis: verum

end;

end;

end;

hence BDD A is_inside_component_of A ; :: thesis: verum