:: Bounded Domains and Unbounded Domains :: by Yatsuka Nakamura , Andrzej Trybulec and Czeslaw Bylinski :: :: Received January 7, 1999 :: Copyright (c) 1999-2012 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, REAL_1, XXREAL_0, CARD_1, COMPLEX1, ARYTM_1, ARYTM_3, FINSEQ_1, RELAT_1, FUNCT_1, ORDINAL2, PRE_TOPC, EUCLID, RVSUM_1, SQUARE_1, XBOOLE_0, RELAT_2, TARSKI, STRUCT_0, NAT_1, XXREAL_2, CONNSP_1, METRIC_1, CONVEX1, CONNSP_3, ZFMISC_1, SETFAM_1, RLTOPSP1, FINSEQ_2, SUPINF_2, BORSUK_1, XXREAL_1, BORSUK_2, GRAPH_1, TOPMETR, TREAL_1, VALUED_1, FUNCT_4, RCOMP_1, TOPREAL1, TOPS_2, PCOMPS_1, WEIERSTR, SEQ_4, XREAL_0, ORDINAL1, PARTFUN1, FUNCOP_1, BINOP_2, ORDINAL4, JORDAN3, TBSP_1, CONNSP_2, RUSUB_4, SPPOL_1, GOBOARD2, SPRECT_1, TREES_1, PSCOMP_1, GOBOARD1, MCART_1, MATRIX_1, GOBOARD9, GOBOARD5, TOPS_1, JORDAN1, SPRECT_2, JORDAN2C; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, RVSUM_1, RELSET_1, PARTFUN1, FUNCT_2, ORDINAL1, CARD_1, NUMBERS, XREAL_0, XXREAL_2, COMPLEX1, SEQ_1, SEQM_3, PRE_TOPC, TOPS_1, TOPS_2, COMPTS_1, BINOP_1, METRIC_1, BINOP_2, PCOMPS_1, CONNSP_1, CONNSP_2, TBSP_1, CONNSP_3, TOPMETR, RCOMP_1, FINSEQ_1, FINSEQ_2, DOMAIN_1, STRUCT_0, SQUARE_1, BORSUK_2, XXREAL_0, SEQ_4, FINSEQ_6, FUNCOP_1, FUNCT_3, TREAL_1, FUNCT_4, RLVECT_1, RUSUB_4, RLTOPSP1, CONVEX1, EUCLID, SPPOL_1, PSCOMP_1, SPRECT_1, SPRECT_2, TOPREAL1, MATRIX_1, GOBOARD1, GOBOARD2, GOBOARD5, GOBOARD9, JORDAN2B, REAL_1, NAT_1, NAT_D, WEIERSTR; constructors REAL_1, SQUARE_1, FINSEQOP, RCOMP_1, FINSOP_1, TOPS_1, CONNSP_1, TOPS_2, COMPTS_1, TBSP_1, MONOID_0, TREAL_1, GOBOARD2, SPPOL_1, JORDAN1, PSCOMP_1, WEIERSTR, BORSUK_2, GOBOARD9, CONNSP_3, JORDAN2B, SPRECT_1, SPRECT_2, SEQ_1, BINOP_2, GOBOARD1, NAT_D, SEQ_4, FUNCSDOM, CONVEX1, RUSUB_4; registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, FINSEQ_1, STRUCT_0, PRE_TOPC, TOPS_1, METRIC_1, BORSUK_1, TBSP_1, EUCLID, TOPMETR, GOBOARD2, JORDAN1, BORSUK_2, SPRECT_1, SPRECT_3, VALUED_0, FINSEQ_2, RLTOPSP1, JORDAN2B, MONOID_0, SEQ_4, SPPOL_1, CARD_1, ZFMISC_1, NAT_1, REAL_1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; definitions TARSKI, XBOOLE_0, TOPS_2, TBSP_1, EUCLID, BINOP_1, SQUARE_1, SUBSET_1, PSCOMP_1, FINSEQ_2, CONNSP_3, RVSUM_1, STRUCT_0, VALUED_1, ALGSTR_0, RLTOPSP1, XXREAL_2, METRIC_1, CONVEX1; theorems PRE_TOPC, CONNSP_1, EUCLID, TBSP_1, TOPREAL3, NAT_1, JGRAPH_1, JORDAN1, TOPS_2, FUNCT_2, BORSUK_1, TOPMETR, TOPREAL1, FINSEQ_2, ABSVALUE, RVSUM_1, SQUARE_1, BORSUK_2, TOPREAL5, WEIERSTR, TARSKI, SEQ_4, FUNCT_1, METRIC_1, SUBSET_1, FUNCOP_1, ZFMISC_1, FINSEQ_1, FINSEQ_4, RELAT_1, FUNCT_3, RCOMP_1, FUNCT_4, HEINE, TREAL_1, CONNSP_3, JORDAN6, COMPTS_1, TSEP_1, CONNSP_2, TOPS_1, JORDAN5D, JORDAN2B, GOBOARD1, GOBOARD2, GOBOARD5, GOBOARD6, UNIFORM1, FINSEQ_6, MATRIX_1, GOBOARD9, GOBRD12, SPRECT_1, CARD_1, CARD_2, ENUMSET1, SPRECT_2, SPRECT_3, SEQ_2, RELSET_1, XBOOLE_0, XBOOLE_1, XREAL_0, TOPRNS_1, XCMPLX_0, XCMPLX_1, BINOP_2, COMPLEX1, XREAL_1, XXREAL_0, FINSOP_1, XXREAL_1, SEQM_3, NAT_D, VALUED_1, RLTOPSP1, RLVECT_1, XXREAL_2, FINSEQ_3, ORDINAL1, SPPOL_1, RUSUB_4, CONVEX1, METRIC_6, XTUPLE_0; schemes NAT_1, CLASSES1; begin :: from, RLAFFIN2, 2011.08.01, A.T. registration let n be Nat; cluster TOP-REAL n -> add-continuous Mult-continuous; coherence proof set T=TOP-REAL n,E=Euclid n,TE=TopSpaceMetr E; A1: the TopStruct of T=TE by EUCLID:def 8; A2: n in NAT by ORDINAL1:def 12; thus T is add-continuous proof let x1,x2 be Point of T,V be Subset of T such that A3: V is open and A4: x1+x2 in V; reconsider X1=x1,X2=x2,X12=x1+x2 as Point of E by A1,TOPMETR:12; reconsider v=V as Subset of TE by A1; V in the topology of T by A3,PRE_TOPC:def 2; then v is open by A1,PRE_TOPC:def 2; then consider r be real number such that A5: r>0 and A6: Ball(X12,r)c=v by A4,TOPMETR:15; set r2=r/2; reconsider B1=Ball(X1,r2),B2=Ball(X2,r2) as Subset of T by A1,TOPMETR:12; take B1,B2; thus B1 is open & B2 is open & x1 in B1 & x2 in B2 by A5,GOBOARD6:1,3,XREAL_1:215; let x be set; assume x in B1+B2; then x in {b1+b2 where b1,b2 is Element of T:b1 in B1 & b2 in B2} by RUSUB_4:def 9; then consider b1,b2 be Element of T such that A7: x=b1+b2 and A8: b1 in B1 and A9: b2 in B2; reconsider e1=b1,e2=b2,e12=b1+b2 as Point of E by A1,TOPMETR:12; reconsider y1=x1,y2=x2,c1=b1,c2=b2 as Element of REAL n by EUCLID:22; dist(X2,e2)0 and A17: Ball(AX,r)c=v by A15,TOPMETR:15; set r2=r/2; A18: r2>0 by A16,XREAL_1:215; then A19: r2/2>0 by XREAL_1:215; ex m be positive Real st abs(a)*m0; then reconsider m=r2/2/abs(a) as positive Real by A19,XREAL_1:139; take m; r2/20) by RVSUM_1:32 .=C-(Y-Y) by RVSUM_1:37 .=C-Y+Y by RVSUM_1:41; then A25: |.c.|<=|.c-y.|+|.y.| by EUCLID:12; A26: dist(X,e)=0 & |.y-c.|=dist(X,e) by A2,COMPLEX1:46,SPPOL_1:5; then |.a*y+-a*c.|<=abs(a)*m by A26,A28,XREAL_1:64; then A29: |.a*y+-a*c.|0)-s*C by RVSUM_1:32 .=a*y-(a*C-a*C)-s*c by RVSUM_1:37 .=a*y-a*C+a*C-s*c by RVSUM_1:41 .=a*y-a*C+a*C+-s*c .=a*y-a*C+(a*c+-s*c) by RVSUM_1:15 .=a*y+-a*c+(a*c+-s*c); then dist(AX,se)=|.a*y+-a*c+(a*c+-s*c).| by A2,SPPOL_1:5; then dist(AX,se)=|.q2.|; then |.q1.|- |.q2.|>=0 by XREAL_1:48; then |.q1.|- |.q2.|=abs(|.q1.|- |.q2.|) by ABSVALUE:def 1; hence thesis by TOPRNS_1:32; end; suppose A1: |.q1.|<|.q2.|; A2: |.q2.|- |.q1.|<= |.q2-q1.| by TOPRNS_1:32; |.q2.|- |.q1.|>0 by A1,XREAL_1:50; then abs(|.q2.|- |.q1.|)<= |.q2-q1.| by A2,ABSVALUE:def 1; then abs(|.q2.|- |.q1.|)<= |.q1-q2.| by TOPRNS_1:27; hence thesis by UNIFORM1:11; end; end; theorem Th10: |.|[r]|.|=abs(r) proof set p=|[r]|; reconsider w=|[r]| as Element of REAL 1 by EUCLID:22; sqr w=<*r^2*> by RVSUM_1:55; then (|.p.|) =sqrt (r^2) by FINSOP_1:11 .=abs r by COMPLEX1:72; hence thesis; end; Lm1: for n being Nat, r being Real st r > 0 for x,y,z being Element of Euclid n st x = 0*n for p being Element of TOP-REAL n st p = y & r*p = z holds r*dist(x,y) = dist(x,z) proof let n be Nat, r be Real such that A1: r > 0; let x,y,z be Element of Euclid n such that A2: x = 0*n; let p be Element of TOP-REAL n such that A3: p = y and A4: r*p = z; reconsider x1=x, y1 = y as Element of REAL n; A5: dist(x,z) = (Pitag_dist n).(x,z) .= |.x1-r*y1.| by A3,A4,EUCLID:def 6; A6: r*x1 = n |-> (0 *r) by A2,RVSUM_1:48 .= x1 by A2; dist(x,y) = (Pitag_dist n).(x,y) .= |.x1-y1.| by EUCLID:def 6; hence r*dist(x,y) = abs(r)*|.x1-y1.| by A1,ABSVALUE:def 1 .= |.r*(x1-y1).| by EUCLID:11 .= |.r*x1 + r*(-y1).| by RVSUM_1:51 .= |.r*x1 + (-1)*r*y1.| by RVSUM_1:49 .= dist(x,z) by A5,A6,RVSUM_1:49; end; Lm2: for n being Nat, r,s being Real st r > 0 for x being Element of Euclid n st x = 0*n for A being Subset of TOP-REAL n st A = Ball(x,s) holds r*A = Ball(x,r*s) proof let n be Nat, r,s be Real such that A1: r > 0; let x be Element of Euclid n such that A2: x = 0*n; let A be Subset of TOP-REAL n such that A3: A = Ball(x,s); thus r*A c= Ball(x,r*s) proof let y; assume y in r*A; then consider v being Element of TOP-REAL n such that A4: y = r * v and A5: v in A; v in {q where q is Element of Euclid n : dist(x,q) < s} by A5,A3,METRIC_1:def 14; then consider q being Element of Euclid n such that A6: v = q and A7: dist(x,q) < s; reconsider p = y as Element of Euclid n by A4,EUCLID:67; r*dist(x,q) = dist(x,p) by A1,A2,A6,A4,Lm1; then dist(x,p) < r*s by A7,A1,XREAL_1:68; then y in {e where e is Element of Euclid n : dist(x,e) < r*s}; hence y in Ball(x,r*s) by METRIC_1:def 14; end; let y; assume y in Ball(x,r*s); then y in {q where q is Element of Euclid n : dist(x,q) < r*s} by METRIC_1:def 14; then consider z being Element of Euclid n such that A8: y = z and A9: dist(x,z) < r*s; reconsider q = z as Element of TOP-REAL n by EUCLID:67; set p = r"*q; A10: y = 1 *q by A8,RVSUM_1:52 .= (r"*r)*q by A1,XCMPLX_0:def 7 .= r * p by RVSUM_1:49; reconsider f = p as Element of Euclid n by EUCLID:67; A11: dist(x,f) = r"*dist(x,z) by A1,A2,Lm1; s = 1 *s .= r"*r""*s by A1,XCMPLX_0:def 7 .= r"*(r*s); then dist(x,f) < s by A9,A11,A1,XREAL_1:68; then p in {e where e is Element of Euclid n : dist(x,e) < s}; then p in A by A3,METRIC_1:def 14; hence y in r*A by A10; end; Lm3: for n being Nat, r,s,t be Real st 0 < s & s <= t for x being Element of Euclid n st x = 0*n for BA being Subset of TOP-REAL n st BA = Ball(x,r) holds s*BA c= t*BA proof let n be Nat, r,s,t be Real such that A1: 0 < s and A2: s <= t; let x be Element of Euclid n such that A3: x = 0*n; let BA be Subset of TOP-REAL n such that A4: BA = Ball(x,r); let e be set; assume e in s*BA; then consider w being Element of TOP-REAL n such that A5: e = s * w and A6: w in BA; w in {q where q is Element of Euclid n : dist(x,q) < r} by A6,A4,METRIC_1:def 14; then consider q being Element of Euclid n such that A7: w = q and A8: dist(x,q) < r; set p = (s/t)*w; A9: e = s * w by A5 .= t*(s/t)*w by A1,A2,XCMPLX_1:87 .= t*((s/t)*w) by RVSUM_1:49 .= t*p; reconsider y = p as Element of Euclid n by EUCLID:67; A10: dist(x,y) = (s/t)*dist(x,q) by A3,A7,Lm1,A1,A2,XREAL_1:139; s/t <= 1 by A1,A2,XREAL_1:183; then dist(x,y) <= dist(x,q) by A10,METRIC_1:5,XREAL_1:153; then dist(x,y) < r by A8,XXREAL_0:2; then p in {f where f is Element of Euclid n : dist(x,f) < r}; then p in BA by A4,METRIC_1:def 14; hence e in t*BA by A9; end; theorem Th11: for n being Nat, A be Subset of TOP-REAL n holds A is bounded iff A is bounded Subset of Euclid n proof let n be Nat, A be Subset of TOP-REAL n; reconsider z = 0*n as Element of Euclid n; thus A is bounded implies A is bounded Subset of Euclid n proof assume A1: A is bounded; reconsider B = A as Subset of Euclid n by EUCLID:67; z = 0.TOP-REAL n by EUCLID:70; then reconsider V = Ball(z,1) as a_neighborhood of 0.TOP-REAL n by GOBOARD6:2; consider s being Real such that A2: s > 0 and A3: for t being Real st t > s holds A c= t*V by A1,RLTOPSP1:def 12; set r = s+1; 0 < r by A2; then r*V = Ball(z,r*1) by Lm2; then B c= Ball(z,r) by A3,XREAL_1:29; hence A is bounded Subset of Euclid n by A2,METRIC_6:def 3; end; assume A4: A is bounded Subset of Euclid n; then reconsider B = A as Subset of Euclid n; consider r1 being Real such that A5: 0 < r1 and A6: B c= Ball(z,r1) by A4,METRIC_6:29; let V be a_neighborhood of 0.TOP-REAL n; 0.TOP-REAL n = 0*n by EUCLID:70; then z in Int V by CONNSP_2:def 1; then consider r2 being real number such that A7: r2 > 0 and A8: Ball(z,r2) c= V by GOBOARD6:5; reconsider r2 as Real by XREAL_0:def 1; take s = r1/r2; thus A9: s > 0 by A5,A7,XREAL_1:139; let t; reconsider BA = Ball(z,r2) as Subset of TOP-REAL n by EUCLID:67; s*r2 = r1 by A7,XCMPLX_1:87; then A10: A c= s*BA by A6,A9,Lm2; assume t > s; then s*BA c= t*BA by A9,Lm3; then A11: A c= t*BA by A10,XBOOLE_1:1; t*BA c= t*V by A8,CONVEX1:39; hence A c= t*V by A11,XBOOLE_1:1; end; theorem for A,B being Subset of TOP-REAL n st B is bounded & A c= B holds A is bounded by RLTOPSP1:42; definition canceled; let n be Nat; let A, B be Subset of TOP-REAL n; pred B is_inside_component_of A means :Def2: B is_a_component_of A` & B is bounded; end; registration let M be non empty MetrStruct; cluster bounded for Subset of M; existence proof take {}M, 1; thus thesis; end; end; theorem Th13: for A being Subset of TOP-REAL n, B being Subset of TOP-REAL n holds B is_inside_component_of A iff ex C being Subset of ((TOP-REAL n) | (A`)) st C=B & C is a_component & C is bounded Subset of Euclid n proof let A be Subset of TOP-REAL n, B be Subset of TOP-REAL n; A1: B is_a_component_of A` iff ex C being Subset of (TOP-REAL n) | (A`) st C=B & C is a_component by CONNSP_1:def 6; A2: B is_inside_component_of A iff B is_a_component_of A` & B is bounded by Def2; thus B is_inside_component_of A implies ex C being Subset of ((TOP-REAL n) | (A`)) st C=B & C is a_component & C is bounded Subset of Euclid n proof assume A3: B is_inside_component_of A; then B is bounded Subset of Euclid n by A2,Th11; hence thesis by A1,A3,Def2; end; given C being Subset of ((TOP-REAL n) | (A`)) such that A4: C=B & C is a_component & C is bounded Subset of Euclid n; B is bounded & B is_a_component_of A` by A4,Th11,CONNSP_1:def 6; hence thesis by Def2; end; definition let n be Nat; let A, B be Subset of TOP-REAL n; pred B is_outside_component_of A means :Def3: B is_a_component_of A` & B is not bounded; end; theorem Th14: for A being Subset of TOP-REAL n, B being Subset of TOP-REAL n holds B is_outside_component_of A iff ex C being Subset of ((TOP-REAL n) | (A`)) st C=B & C is a_component & C is not bounded Subset of Euclid n proof let A be Subset of TOP-REAL n, B be Subset of TOP-REAL n; A1: B is_a_component_of A` iff ex C being Subset of (TOP-REAL n) | (A`) st C=B & C is a_component by CONNSP_1:def 6; A2: B is_outside_component_of A iff B is_a_component_of A` & not B is bounded by Def3; thus B is_outside_component_of A implies ex C being Subset of ((TOP-REAL n) | (A`)) st C=B & C is a_component & C is not bounded Subset of Euclid n proof reconsider D2=B as Subset of Euclid n by TOPREAL3:8; assume A3: B is_outside_component_of A; then consider C being Subset of (TOP-REAL n) | (A`) such that A4: C=B and A5: C is a_component by A1,Def3; now assume for D being Subset of Euclid n st D=C holds D is bounded; then D2 is bounded by A4; hence contradiction by A2,A3,Th11; end; hence thesis by A4,A5; end; given C being Subset of ((TOP-REAL n) | (A`)) such that A6: C=B & C is a_component & C is not bounded Subset of Euclid n; ( not B is bounded)& B is_a_component_of A` by A6,Th11,CONNSP_1:def 6; hence thesis by Def3; end; theorem for A,B being Subset of TOP-REAL n st B is_inside_component_of A holds B c= A` proof let A,B be Subset of TOP-REAL n; assume B is_inside_component_of A; then B is_a_component_of A` by Def2; hence thesis by SPRECT_1:5; end; theorem for A,B being Subset of TOP-REAL n st B is_outside_component_of A holds B c= A` proof let A,B be Subset of TOP-REAL n; assume B is_outside_component_of A; then B is_a_component_of A` by Def3; hence thesis by SPRECT_1:5; end; definition let n be Nat; let A be Subset of TOP-REAL n; func BDD A -> Subset of TOP-REAL n equals union{B where B is Subset of TOP-REAL n: B is_inside_component_of A}; correctness proof union{B where B is Subset of TOP-REAL n: B is_inside_component_of A} c= the carrier of TOP-REAL n proof let x; assume x in union{B where B is Subset of TOP-REAL n: B is_inside_component_of A}; then consider y being set such that A1: x in y and A2: y in {B where B is Subset of TOP-REAL n: B is_inside_component_of A} by TARSKI:def 4; ex B being Subset of TOP-REAL n st y=B & B is_inside_component_of A by A2; hence thesis by A1; end; hence thesis; end; end; definition let n be Nat; let A be Subset of TOP-REAL n; func UBD A -> Subset of TOP-REAL n equals union{B where B is Subset of TOP-REAL n: B is_outside_component_of A}; correctness proof union{B where B is Subset of TOP-REAL n: B is_outside_component_of A} c= the carrier of TOP-REAL n proof let x; assume x in union{B where B is Subset of TOP-REAL n: B is_outside_component_of A}; then consider y being set such that A1: x in y and A2: y in {B where B is Subset of TOP-REAL n: B is_outside_component_of A } by TARSKI:def 4; ex B being Subset of TOP-REAL n st y=B & B is_outside_component_of A by A2; hence thesis by A1; end; hence thesis; end; end; registration let n be Nat; cluster [#](TOP-REAL n) -> convex; coherence proof let w1,w2 be Point of TOP-REAL n; thus thesis; end; end; registration let n; cluster [#](TOP-REAL n) -> a_component; coherence proof set A=[#](TOP-REAL n); for B being Subset of TOP-REAL n st B is connected holds A c= B implies A = B by XBOOLE_0:def 10; hence thesis by CONNSP_1:def 5; end; end; canceled 3; theorem Th20: for A being Subset of TOP-REAL n holds BDD A is a_union_of_components of (TOP-REAL n) | A` proof let A be Subset of TOP-REAL n; {B where B is Subset of TOP-REAL n: B is_inside_component_of A} c= bool (the carrier of ((TOP-REAL n) | A`)) proof let x; assume x in {B where B is Subset of TOP-REAL n: B is_inside_component_of A}; then consider B being Subset of TOP-REAL n such that A1: x=B and A2: B is_inside_component_of A; ex C being Subset of ((TOP-REAL n) | (A`)) st C=B & C is a_component & C is bounded Subset of Euclid n by A2,Th13; hence thesis by A1; end; then reconsider F0={B where B is Subset of TOP-REAL n: B is_inside_component_of A } as Subset-Family of the carrier of ((TOP-REAL n) | A`); reconsider F0 as Subset-Family of (TOP-REAL n) | A`; A3: for B0 being Subset of ((TOP-REAL n) | A`) st B0 in F0 holds B0 is a_component proof let B0 be Subset of ((TOP-REAL n) | A`); assume B0 in F0; then consider B being Subset of TOP-REAL n such that A4: B=B0 and A5: B is_inside_component_of A; ex C being Subset of ((TOP-REAL n) | (A`)) st C=B & C is a_component & C is bounded Subset of Euclid n by A5,Th13; hence thesis by A4; end; BDD A=union F0; hence thesis by A3,CONNSP_3:def 2; end; theorem Th21: for A being Subset of TOP-REAL n holds UBD A is a_union_of_components of (TOP-REAL n) | A` proof let A be Subset of TOP-REAL n; {B where B is Subset of TOP-REAL n: B is_outside_component_of A} c= bool (the carrier of ((TOP-REAL n) | A`)) proof let x; assume x in {B where B is Subset of TOP-REAL n: B is_outside_component_of A}; then consider B being Subset of TOP-REAL n such that A1: x=B and A2: B is_outside_component_of A; ex C being Subset of ((TOP-REAL n) | (A`)) st C=B & C is a_component & C is not bounded Subset of Euclid n by A2,Th14; hence thesis by A1; end; then reconsider F0={B where B is Subset of TOP-REAL n: B is_outside_component_of A} as Subset-Family of the carrier of ((TOP-REAL n) | A`); reconsider F0 as Subset-Family of ((TOP-REAL n) | A`); A3: for B0 being Subset of ((TOP-REAL n) | A`) st B0 in F0 holds B0 is a_component proof let B0 be Subset of ((TOP-REAL n) | A`); assume B0 in F0; then consider B being Subset of TOP-REAL n such that A4: B=B0 and A5: B is_outside_component_of A; ex C being Subset of ((TOP-REAL n) | (A`)) st C=B & C is a_component & C is not bounded Subset of Euclid n by A5,Th14; hence thesis by A4; end; UBD A=union F0; hence thesis by A3,CONNSP_3:def 2; end; theorem Th22: for A being Subset of TOP-REAL n, B being Subset of TOP-REAL n st B is_inside_component_of A holds B c= BDD A proof let A be Subset of TOP-REAL n, B be Subset of TOP-REAL n; assume B is_inside_component_of A; then A1: B in {B2 where B2 is Subset of TOP-REAL n: B2 is_inside_component_of A}; let x; assume x in B; hence thesis by A1,TARSKI:def 4; end; theorem Th23: for A being Subset of TOP-REAL n, B being Subset of TOP-REAL n st B is_outside_component_of A holds B c= UBD A proof let A be Subset of TOP-REAL n, B be Subset of TOP-REAL n; assume B is_outside_component_of A; then A1: B in {B2 where B2 is Subset of TOP-REAL n: B2 is_outside_component_of A}; let x; assume x in B; hence thesis by A1,TARSKI:def 4; end; theorem Th24: for A being Subset of TOP-REAL n holds BDD A misses UBD A proof let A be Subset of TOP-REAL n; set x = the Element of (BDD A) /\ (UBD A); assume A1: (BDD A) /\ (UBD A) <>{}; then x in union{B where B is Subset of TOP-REAL n: B is_inside_component_of A } by XBOOLE_0:def 4; then consider y being set such that A2: x in y and A3: y in {B where B is Subset of TOP-REAL n: B is_inside_component_of A} by TARSKI:def 4; x in union{B2 where B2 is Subset of TOP-REAL n: B2 is_outside_component_of A} by A1,XBOOLE_0:def 4; then consider y2 being set such that A4: x in y2 and A5: y2 in {B2 where B2 is Subset of TOP-REAL n: B2 is_outside_component_of A} by TARSKI:def 4; consider B being Subset of TOP-REAL n such that A6: y=B and A7: B is_inside_component_of A by A3; consider B2 being Subset of TOP-REAL n such that A8: y2=B2 and A9: B2 is_outside_component_of A by A5; consider C being Subset of ((TOP-REAL n) | (A`)) such that A10: C=B and A11: C is a_component & C is bounded Subset of Euclid n by A7,Th13; consider C2 being Subset of ((TOP-REAL n) | (A`)) such that A12: C2=B2 and A13: C2 is a_component & C2 is not bounded Subset of Euclid n by A9,Th14; C /\ C2<>{}((TOP-REAL n) | (A`)) by A2,A6,A10,A4,A8,A12,XBOOLE_0:def 4; then C meets C2 by XBOOLE_0:def 7; hence contradiction by A11,A13,CONNSP_1:35; end; theorem Th25: for A being Subset of TOP-REAL n holds BDD A c= A` proof let A be Subset of TOP-REAL n; reconsider D=BDD A as Subset of (TOP-REAL n) | A` by Th20; D c= the carrier of ((TOP-REAL n) | A`); hence thesis by PRE_TOPC:8; end; theorem Th26: for A being Subset of TOP-REAL n holds UBD A c= A` proof let A be Subset of TOP-REAL n; reconsider D=UBD A as Subset of (TOP-REAL n) | A` by Th21; D c= the carrier of ((TOP-REAL n) | A`); hence thesis by PRE_TOPC:8; end; theorem Th27: for A being Subset of TOP-REAL n holds (BDD A) \/ (UBD A) = A` proof let A be Subset of TOP-REAL n; A1: A` c= (BDD A) \/ (UBD A) proof let z be set; assume A2: z in A`; then reconsider p=z as Element of A`; reconsider B=A` as non empty Subset of TOP-REAL n by A2; reconsider q=p as Point of (TOP-REAL n) | A` by PRE_TOPC:8; Component_of q is Subset of [#]((TOP-REAL n) | A`); then Component_of q is Subset of A` by PRE_TOPC:def 5; then reconsider G=Component_of q as Subset of TOP-REAL n by XBOOLE_1:1; A3: (TOP-REAL n) | B is non empty; then A4: q in G by CONNSP_1:38; Component_of q is a_component by A3,CONNSP_1:40; then A5: G is_a_component_of A` by CONNSP_1:def 6; per cases; suppose G is bounded; then G is_inside_component_of A by A5,Def2; then G c= BDD A by Th22; hence thesis by A4,XBOOLE_0:def 3; end; suppose not G is bounded; then G is_outside_component_of A by A5,Def3; then G c= UBD A by Th23; hence thesis by A4,XBOOLE_0:def 3; end; end; (BDD A) c= A` & (UBD A) c= A` by Th25,Th26; then (BDD A) \/ (UBD A) c= A` by XBOOLE_1:8; hence thesis by A1,XBOOLE_0:def 10; end; reserve u for Point of Euclid n; theorem Th28: for P being Subset of TOP-REAL n st P=REAL n holds P is connected proof let P be Subset of TOP-REAL n; assume A1: P=(REAL n); for p1,p2 being Point of TOP-REAL n st p1 in P & p2 in P holds LSeg(p1, p2) c= P proof let p1,p2 be Point of TOP-REAL n; assume that p1 in P and p2 in P; the carrier of TOP-REAL n=REAL n by EUCLID:22; hence thesis by A1; end; then P is convex by JORDAN1:def 1; hence thesis; end; canceled 4; theorem Th33: for W being Subset of Euclid n st n>=1 & W=REAL n holds W is not bounded proof let W be Subset of Euclid n; assume that A1: n>=1 and A2: W=(REAL n); reconsider y0=0.TOP-REAL n as Point of Euclid n by EUCLID:67; assume W is bounded; then consider r being Real such that A3: 0{}; reconsider o=0.TOP-REAL n as Point of Euclid n by EUCLID:67; set x0 = the Element of C; x0 in C by A1; then reconsider x0 as Point of Euclid n; consider r being Real such that 0{}; set x0 = the Element of C; x0 in C by A6; then reconsider x0 as Point of Euclid n; reconsider q0=x0 as Point of TOP-REAL n by TOPREAL3:8; reconsider o=0.TOP-REAL n as Point of Euclid n by EUCLID:67; set R0=r+r; A7: for x,y being Point of (Euclid n) st x in C & y in C holds dist(x,y ) <= R0 proof let x,y be Point of (Euclid n); assume that A8: x in C and A9: y in C; reconsider q2=y as Point of TOP-REAL n by A9; dist(o,y)=|.q2-(0.TOP-REAL n) .| by JGRAPH_1:28 .=|.q2.| by RLVECT_1:13; then A10: dist(o,y) =1 implies not [#](TOP-REAL n) is bounded proof assume A1: n>=1; assume [#](TOP-REAL n) is bounded; then reconsider C=[#](TOP-REAL n) as bounded Subset of Euclid n by Th11; C=REAL n by EUCLID:22; hence contradiction by A1,Th33; end; theorem Th36: n>=1 implies UBD {}(TOP-REAL n)=REAL n proof set A={}(TOP-REAL n); A1: (TOP-REAL n) | [#](TOP-REAL n)=the TopStruct of TOP-REAL n by TSEP_1:93; assume A2: n>=1; A3: now reconsider D1=[#]((TOP-REAL n) | A`) as Subset of Euclid n by A1,TOPREAL3:8; assume for D being Subset of Euclid n st D=[#]((TOP-REAL n) | A`) holds D is bounded; then D1 is bounded; then [#](TOP-REAL n) is bounded by A1,Th11; hence contradiction by A2,Th35; end; [#]((TOP-REAL n) | A`) is a_component by A1,CONNSP_1:45; then [#](TOP-REAL n) is_outside_component_of {}(TOP-REAL n) by A1,A3,Th14; then A4: [#](TOP-REAL n) in {B2 where B2 is Subset of TOP-REAL n: B2 is_outside_component_of {}(TOP-REAL n)}; UBD {}(TOP-REAL n) c= the carrier of TOP-REAL n; hence UBD {}(TOP-REAL n) c= REAL n by EUCLID:22; let x be set; assume x in REAL n; then x in [#](TOP-REAL n) by EUCLID:22; hence thesis by A4,TARSKI:def 4; end; theorem Th37: for w1,w2,w3 being Point of TOP-REAL n, P being non empty Subset of TOP-REAL n, h1,h2 being Function of I[01],(TOP-REAL n) |P st h1 is continuous & w1=h1.0 & w2=h1.1 & h2 is continuous & w2=h2.0 & w3=h2.1 holds ex h3 being Function of I[01],(TOP-REAL n) |P st h3 is continuous & w1=h3.0 & w3=h3.1 proof let w1,w2,w3 be Point of TOP-REAL n, P be non empty Subset of TOP-REAL n, h1 ,h2 be Function of I[01],(TOP-REAL n) |P; assume that A1: h1 is continuous and A2: w1=h1.0 and A3: w2=h1.1 and A4: h2 is continuous and A5: w2=h2.0 and A6: w3=h2.1; 0 in [.0 qua Real,1 qua Real.] & 1 in [.0 qua Real,1 qua Real.] by XXREAL_1:1 ; then reconsider p1=w1,p2=w2,p3=w3 as Point of (TOP-REAL n) |P by A2,A3,A6, BORSUK_1:40,FUNCT_2:5; p2,p3 are_connected by A4,A5,A6,BORSUK_2:def 1; then reconsider P2=h2 as Path of p2,p3 by A4,A5,A6,BORSUK_2:def 2; p1,p2 are_connected by A1,A2,A3,BORSUK_2:def 1; then reconsider P1=h1 as Path of p1,p2 by A1,A2,A3,BORSUK_2:def 2; ex P0 being Path of p1,p3 st P0 is continuous & P0.0=p1 & P0.1=p3 & for t being Point of I[01], t9 being Real st t = t9 holds ( 0 <= t9 & t9 <= 1/2 implies P0.t = P1.(2*t9) ) & ( 1/2 <= t9 & t9 <= 1 implies P0.t = P2.(2*t9-1) ) proof 1/2 in { r : 0 <= r & r <= 1 }; then reconsider pol = 1/2 as Point of I[01] by BORSUK_1:40,RCOMP_1:def 1; reconsider T1 = Closed-Interval-TSpace (0, 1/2), T2 = Closed-Interval-TSpace (1/2, 1) as SubSpace of I[01] by TOPMETR:20,TREAL_1:3; set e2 = P[01](1/2, 1, (#)(0,1), (0,1)(#)); set e1 = P[01](0, 1/2, (#)(0,1), (0,1)(#)); set E1 = P1 * e1; set E2 = P2 * e2; set f = E1 +* E2; A7: dom e1 = the carrier of Closed-Interval-TSpace(0,1/2) by FUNCT_2:def 1 .= [.0,1/2.] by TOPMETR:18; A8: dom e2 = the carrier of Closed-Interval-TSpace(1/2,1) by FUNCT_2:def 1 .= [.1/2,1 qua Real.] by TOPMETR:18; reconsider gg = E2 as Function of T2, ((TOP-REAL n) |P) by TOPMETR:20; reconsider ff = E1 as Function of T1, ((TOP-REAL n) |P) by TOPMETR:20; A9: for t9 being Real st 1/2 <= t9 & t9 <= 1 holds E2.t9 = P2.(2*t9-1) proof reconsider r1 = (#)(0,1), r2 = (0,1)(#) as Real by BORSUK_1:def 14,def 15 ,TREAL_1:5; dom e2 = the carrier of Closed-Interval-TSpace(1/2,1) by FUNCT_2:def 1; then A10: dom e2 = [.1/2,1 qua Real.] by TOPMETR:18 .= {r : 1/2 <= r & r <= 1 } by RCOMP_1:def 1; let t9 be Real; assume 1/2 <= t9 & t9 <= 1; then A11: t9 in dom e2 by A10; then reconsider s = t9 as Point of Closed-Interval-TSpace (1/2,1); e2.s = ((r2 - r1)/(1 - 1/2))*t9 + (1 * r1 - (1/2)*r2)/(1 - 1/2) by TREAL_1:11 .= 2*t9 - 1 by BORSUK_1:def 14,def 15,TREAL_1:5; hence thesis by A11,FUNCT_1:13; end; A12: for t9 being Real st 0 <= t9 & t9 <= 1/2 holds E1.t9 = P1.(2*t9) proof reconsider r1 = (#)(0,1), r2 = (0,1)(#) as Real by BORSUK_1:def 14,def 15 ,TREAL_1:5; dom e1 = the carrier of Closed-Interval-TSpace(0,1/2) by FUNCT_2:def 1; then A13: dom e1 = [.0, 1/2.] by TOPMETR:18 .= {r : 0 <= r & r <= 1/2 } by RCOMP_1:def 1; let t9 be Real; assume 0 <= t9 & t9 <= 1/2; then A14: t9 in dom e1 by A13; then reconsider s = t9 as Point of Closed-Interval-TSpace (0, 1/2); e1.s = ((r2 - r1)/(1/2 - 0))*t9 + ((1/2)*r1 - 0 * r2)/(1/2 - 0) by TREAL_1:11 .= 2*t9 by BORSUK_1:def 14,def 15,TREAL_1:5; hence thesis by A14,FUNCT_1:13; end; then A15: ff.(1/2) = P2.(2*(1/2)-1) by A3,A5 .= gg.pol by A9; [#] T1 = [.0,1/2.] & [#] T2 = [.1/2,1 qua Real.] by TOPMETR:18; then A16: ([#] T1) \/ ([#] T2) = [#] I[01] & ([#] T1) /\ ([#] T2) = {pol} by BORSUK_1:40,XXREAL_1:174,418; rng f c= rng E1 \/ rng E2 by FUNCT_4:17; then A17: rng f c= the carrier of ((TOP-REAL n) |P) by XBOOLE_1:1; A18: T1 is compact & T2 is compact by HEINE:4; dom P1 = the carrier of I[01] by FUNCT_2:def 1; then A19: rng e1 c= dom P1 by TOPMETR:20; dom P2 = the carrier of I[01] & rng e2 c= the carrier of Closed-Interval-TSpace(0,1) by FUNCT_2:def 1; then A20: dom E2 = dom e2 by RELAT_1:27,TOPMETR:20; not 0 in { r : 1/2 <= r & r <= 1 } proof assume 0 in { r : 1/2 <= r & r <= 1 }; then ex rr being Real st rr = 0 & 1/2 <= rr & rr <= 1; hence thesis; end; then not 0 in dom E2 by A8,A20,RCOMP_1:def 1; then A21: f.0 = E1.0 by FUNCT_4:11 .= P1.(2*0) by A12 .= p1 by A2; dom f = dom E1 \/ dom E2 by FUNCT_4:def 1 .= [.0,1/2.] \/ [.1/2,1 qua Real.] by A7,A8,A19,A20,RELAT_1:27 .= the carrier of I[01] by BORSUK_1:40,XXREAL_1:174; then reconsider f as Function of I[01], ((TOP-REAL n) |P) by A17, FUNCT_2:def 1,RELSET_1:4; e1 is continuous & e2 is continuous by TREAL_1:12; then reconsider f as continuous Function of I[01], ((TOP-REAL n) |P) by A1,A4,A15,A16,A18, COMPTS_1:20,TOPMETR:20; 1 in { r : 1/2 <= r & r <= 1 }; then 1 in dom E2 by A8,A20,RCOMP_1:def 1; then A22: f.1 = E2.1 by FUNCT_4:13 .= P2.(2*1-1) by A9 .= p3 by A6; then p1,p3 are_connected by A21,BORSUK_2:def 1; then reconsider f as Path of p1, p3 by A21,A22,BORSUK_2:def 2; for t being Point of I[01], t9 being Real st t = t9 holds ( 0 <= t9 & t9 <= 1/2 implies f.t = P1.(2*t9) ) & ( 1/2 <= t9 & t9 <= 1 implies f.t = P2.(2 *t9-1) ) proof let t be Point of I[01], t9 be Real; assume A23: t = t9; thus 0 <= t9 & t9 <= 1/2 implies f.t = P1.(2*t9) proof assume A24: 0 <= t9 & t9 <= 1/2; then t9 in { r : 0 <= r & r <= 1/2 }; then A25: t9 in [.0,1/2.] by RCOMP_1:def 1; per cases; suppose A26: t9 <> 1/2; not t9 in dom E2 proof assume t9 in dom E2; then t9 in [.0,1/2.] /\ [.1/2,1 qua Real.] by A8,A20,A25, XBOOLE_0:def 4; then t9 in {1/2} by XXREAL_1:418; hence thesis by A26,TARSKI:def 1; end; then f.t = E1.t by A23,FUNCT_4:11 .= P1.(2*t9) by A12,A23,A24; hence thesis; end; suppose A27: t9 = 1/2; 1/2 in { r : 1/2 <= r & r <= 1 }; then 1/2 in [.1/2, 1 qua Real.] by RCOMP_1:def 1; then 1/2 in the carrier of Closed-Interval-TSpace(1/2,1) by TOPMETR:18; then t in dom E2 by A23,A27,FUNCT_2:def 1,TOPMETR:20; then f.t = E2.(1/2) by A23,A27,FUNCT_4:13 .= P1.(2*t9) by A12,A15,A27; hence thesis; end; end; thus 1/2 <= t9 & t9 <= 1 implies f.t = P2.(2*t9-1) proof assume A28: 1/2 <= t9 & t9 <= 1; then t9 in { r : 1/2 <= r & r <= 1 }; then t9 in [.1/2,1 qua Real.] by RCOMP_1:def 1; then f.t = E2.t by A8,A20,A23,FUNCT_4:13 .= P2.(2*t9-1) by A9,A23,A28; hence thesis; end; end; hence thesis by A21,A22; end; hence thesis; end; theorem Th38: for P being Subset of TOP-REAL n, w1,w2,w3 being Point of TOP-REAL n st w1 in P & w2 in P & w3 in P & LSeg(w1,w2) c= P & LSeg(w2,w3) c= P ex h being Function of I[01],(TOP-REAL n) |P st h is continuous & w1=h.0 & w3=h.1 proof let P be Subset of TOP-REAL n, w1,w2,w3 be Point of TOP-REAL n; assume that A1: w1 in P and A2: w2 in P and A3: w3 in P and A4: LSeg(w1,w2) c= P and A5: LSeg(w2,w3) c= P; reconsider Y = P as non empty Subset of TOP-REAL n by A1; per cases; suppose A6: w1<>w2; then LSeg(w1,w2) is_an_arc_of w1,w2 by TOPREAL1:9; then consider f being Function of I[01], (TOP-REAL n) | LSeg(w1,w2) such that A7: f is being_homeomorphism and A8: f.0 = w1 and A9: f.1 = w2 by TOPREAL1:def 1; A10: rng f = [#]((TOP-REAL n) | LSeg(w1,w2)) by A7,TOPS_2:def 5; then A11: rng f c= P by A4,PRE_TOPC:def 5; then [#]((TOP-REAL n) | LSeg(w1,w2)) c= [#]((TOP-REAL n) |P) by A10, PRE_TOPC:def 5; then A12: (TOP-REAL n) | LSeg(w1,w2) is SubSpace of (TOP-REAL n) |P by TOPMETR:3; dom f= ([.0 qua Real ,1 qua Real.]) by BORSUK_1:40,FUNCT_2:def 1; then reconsider g=f as Function of ([.0 qua Real,1 qua Real.]),P by A11, FUNCT_2:2; reconsider gt=g as Function of I[01],(TOP-REAL n) | Y by BORSUK_1:40 ,PRE_TOPC:8; A13: f is continuous by A7,TOPS_2:def 5; now per cases; suppose w2<>w3; then LSeg(w2,w3) is_an_arc_of w2,w3 by TOPREAL1:9; then consider f2 being Function of I[01], (TOP-REAL n) | LSeg(w2,w3) such that A14: f2 is being_homeomorphism and A15: f2.0 = w2 & f2.1 = w3 by TOPREAL1:def 1; A16: rng f2 = [#]((TOP-REAL n) | LSeg(w2,w3)) by A14,TOPS_2:def 5; then A17: rng f2 c= P by A5,PRE_TOPC:def 5; then [#]((TOP-REAL n) | LSeg(w2,w3)) c= [#]((TOP-REAL n) |P) by A16, PRE_TOPC:def 5; then A18: (TOP-REAL n) | LSeg(w2,w3) is SubSpace of (TOP-REAL n) |P by TOPMETR:3; [#]((TOP-REAL n) |P)=P by PRE_TOPC:def 5; then reconsider w19=w1,w29=w2,w39=w3 as Point of (TOP-REAL n) |P by A1,A2,A3; A19: gt is continuous & w29=gt.1 by A9,A13,A12,PRE_TOPC:26; dom f2=[.0 qua Real,1 qua Real.] by BORSUK_1:40,FUNCT_2:def 1; then reconsider g2=f2 as Function of ([.0 qua Real,1 qua Real.]),P by A17,FUNCT_2:2; reconsider gt2=g2 as Function of I[01],(TOP-REAL n) | Y by BORSUK_1:40 ,PRE_TOPC:8; f2 is continuous by A14,TOPS_2:def 5; then gt2 is continuous by A18,PRE_TOPC:26; then ex h being Function of I[01],(TOP-REAL n) | Y st h is continuous & w19=h.0 & w39=h.1 & rng h c= (rng gt) \/ (rng gt2) by A8,A15,A19,BORSUK_2:13; hence thesis; end; suppose A20: w2=w3; then LSeg(w1,w3) is_an_arc_of w1,w3 by A6,TOPREAL1:9; then consider f being Function of I[01], (TOP-REAL n) | LSeg(w1,w3) such that A21: f is being_homeomorphism and A22: f.0 = w1 & f.1 = w3 by TOPREAL1:def 1; A23: rng f = [#]((TOP-REAL n) | LSeg(w1,w3)) by A21,TOPS_2:def 5; then A24: rng f c= P by A4,A20,PRE_TOPC:def 5; then [#]((TOP-REAL n) | LSeg(w1,w3)) c= [#]((TOP-REAL n) |P) by A23, PRE_TOPC:def 5; then A25: (TOP-REAL n) | LSeg(w1,w3) is SubSpace of (TOP-REAL n) |P by TOPMETR:3; dom f=[.0 qua Real ,1 qua Real.] by BORSUK_1:40,FUNCT_2:def 1; then reconsider g=f as Function of ([.0 qua Real,1 qua Real.]),P by A24,FUNCT_2:2; reconsider gt=g as Function of I[01],(TOP-REAL n) | Y by BORSUK_1:40 ,PRE_TOPC:8; f is continuous by A21,TOPS_2:def 5; then gt is continuous by A25,PRE_TOPC:26; hence thesis by A22; end; end; hence thesis; end; suppose A26: w1=w2; now per cases; case w2<>w3; then LSeg(w1,w3) is_an_arc_of w1,w3 by A26,TOPREAL1:9; then consider f being Function of I[01], (TOP-REAL n) | LSeg(w1,w3) such that A27: f is being_homeomorphism and A28: f.0 = w1 & f.1 = w3 by TOPREAL1:def 1; A29: rng f = [#]((TOP-REAL n) | LSeg(w1,w3)) by A27,TOPS_2:def 5; then A30: rng f c= P by A5,A26,PRE_TOPC:def 5; then [#]((TOP-REAL n) | LSeg(w1,w3)) c= [#]((TOP-REAL n) |P) by A29, PRE_TOPC:def 5; then A31: (TOP-REAL n) | LSeg(w1,w3) is SubSpace of (TOP-REAL n) |P by TOPMETR:3; dom f=[.0 qua Real,1 qua Real.] by BORSUK_1:40,FUNCT_2:def 1; then reconsider g=f as Function of [.0 qua Real,1 qua Real.],P by A30, FUNCT_2:2; reconsider gt=g as Function of I[01],(TOP-REAL n) | Y by BORSUK_1:40 ,PRE_TOPC:8; f is continuous by A27,TOPS_2:def 5; then gt is continuous by A31,PRE_TOPC:26; hence thesis by A28; end; case A32: w2=w3; [#]((TOP-REAL n) |P)=P by PRE_TOPC:def 5; then reconsider w19=w1,w39=w3 as Point of (TOP-REAL n) |P by A1,A3; ex f be Function of I[01], (TOP-REAL n) | Y st f is continuous & f. 0 = w19 & f.1 = w39 by A26,A32,BORSUK_2:3; hence thesis; end; end; hence thesis; end; end; theorem Th39: for P being Subset of TOP-REAL n, w1,w2,w3,w4 being Point of TOP-REAL n st w1 in P & w2 in P & w3 in P & w4 in P & LSeg(w1,w2) c= P & LSeg( w2,w3) c= P & LSeg(w3,w4) c= P ex h being Function of I[01],(TOP-REAL n) |P st h is continuous & w1=h.0 & w4=h.1 proof let P be Subset of TOP-REAL n, w1,w2,w3,w4 be Point of TOP-REAL n; assume that A1: w1 in P and A2: w2 in P and A3: w3 in P and A4: w4 in P and A5: LSeg(w1,w2) c= P & LSeg(w2,w3) c= P and A6: LSeg(w3,w4) c= P; reconsider Y = P as non empty Subset of TOP-REAL n by A1; consider h2 being Function of I[01],(TOP-REAL n) |P such that A7: h2 is continuous & w1=h2.0 and A8: w3=h2.1 by A1,A2,A3,A5,Th38; per cases; suppose w3<>w4; then LSeg(w3,w4) is_an_arc_of w3,w4 by TOPREAL1:9; then consider f being Function of I[01], (TOP-REAL n) | LSeg(w3,w4) such that A9: f is being_homeomorphism and A10: f.0 = w3 & f.1 = w4 by TOPREAL1:def 1; A11: rng f = [#]((TOP-REAL n) | LSeg(w3,w4)) by A9,TOPS_2:def 5; then A12: rng f c= P by A6,PRE_TOPC:def 5; then [#]((TOP-REAL n) | LSeg(w3,w4)) c= [#]((TOP-REAL n) |P) by A11, PRE_TOPC:def 5; then A13: (TOP-REAL n) | LSeg(w3,w4) is SubSpace of (TOP-REAL n) |P by TOPMETR:3; [#]((TOP-REAL n) |P)=P by PRE_TOPC:def 5; then reconsider w19=w1,w39=w3,w49=w4 as Point of (TOP-REAL n) |P by A1,A3,A4; A14: w39=h2.1 by A8; dom f=[.0 qua Real,1 qua Real.] by BORSUK_1:40,FUNCT_2:def 1; then reconsider g=f as Function of [.0 qua Real,1 qua Real.],P by A12, FUNCT_2:2; reconsider gt=g as Function of I[01],(TOP-REAL n) | Y by BORSUK_1:40 ,PRE_TOPC:8; f is continuous by A9,TOPS_2:def 5; then gt is continuous by A13,PRE_TOPC:26; then ex h being Function of I[01],(TOP-REAL n) | Y st h is continuous & w19= h.0 & w49=h.1 & rng h c= (rng h2) \/ (rng gt) by A7,A10,A14,BORSUK_2:13; hence thesis; end; suppose w3=w4; hence thesis by A7,A8; end; end; theorem Th40: for P being Subset of TOP-REAL n, w1,w2,w3,w4,w5,w6,w7 being Point of TOP-REAL n st w1 in P & w2 in P & w3 in P & w4 in P & w5 in P & w6 in P & w7 in P & LSeg(w1,w2) c= P & LSeg(w2,w3) c= P & LSeg(w3,w4) c= P & LSeg(w4, w5) c= P & LSeg(w5,w6) c= P & LSeg(w6,w7) c= P ex h being Function of I[01],( TOP-REAL n) |P st h is continuous & w1=h.0 & w7=h.1 proof let P be Subset of TOP-REAL n, w1,w2,w3,w4,w5,w6,w7 be Point of TOP-REAL n; assume that A1: w1 in P and A2: w2 in P & w3 in P & w4 in P & w5 in P & w6 in P & w7 in P & LSeg(w1, w2) c= P & LSeg(w2,w3) c= P & LSeg(w3,w4) c= P & LSeg(w4,w5) c= P & LSeg(w5, w6 ) c= P & LSeg(w6,w7) c= P; ( ex h2 being Function of I[01],(TOP-REAL n) |P st h2 is continuous & w1= h2.0 & w4=h2.1)& ex h4 being Function of I[01],(TOP-REAL n) |P st h4 is continuous & w4=h4.0 & w7=h4.1 by A1,A2,Th39; hence thesis by A1,Th37; end; theorem Th41: for w1,w2 being Point of TOP-REAL n,P being Subset of TopSpaceMetr(Euclid n) st P=LSeg(w1,w2)& not (0.TOP-REAL n) in LSeg(w1,w2) holds ex w0 being Point of TOP-REAL n st w0 in LSeg(w1,w2) & |.w0.|>0 & |.w0.|= (dist_min(P)).(0.TOP-REAL n) proof let w1,w2 be Point of TOP-REAL n,P be Subset of TopSpaceMetr(Euclid n); assume that A1: P=LSeg(w1,w2) and A2: not 0.TOP-REAL n in LSeg(w1,w2); set M=Euclid n; reconsider P0=P as Subset of TopSpaceMetr(M); A3: the TopStruct of TOP-REAL n = TopSpaceMetr M by EUCLID:def 8; then reconsider Q={0.TOP-REAL n} as Subset of TopSpaceMetr(M); P0 is compact by A1,A3,COMPTS_1:23; then consider x1,x2 being Point of M such that A4: x1 in P0 and A5: x2 in Q and A6: dist(x1,x2) = min_dist_min(P0,Q) by A1,A3,WEIERSTR:30; reconsider w01=x1 as Point of TOP-REAL n by EUCLID:67; A7: x2=0.TOP-REAL n by A5,TARSKI:def 1; reconsider o=0.TOP-REAL n as Point of M by EUCLID:67; reconsider o2=0.TOP-REAL n as Point of TopSpaceMetr(M) by A3; for x being set holds x in (dist_min(P0)).:(Q) iff x=(dist_min(P0)).o proof let x be set; hereby assume x in (dist_min(P0)).:(Q); then ex y being set st y in dom(dist_min(P0)) & y in Q & x=( dist_min(P0) ).y by FUNCT_1:def 6; hence x=(dist_min(P0)).o by TARSKI:def 1; end; o2 in the carrier of TopSpaceMetr(M) by A3; then A8: o in Q & o in dom (dist_min(P0)) by FUNCT_2:def 1,TARSKI:def 1; assume x=(dist_min(P0)).o; hence thesis by A8,FUNCT_1:def 6; end; then A9: (dist_min(P0)).:(Q)={(dist_min(P0)).o} by TARSKI:def 1; [#] ((dist_min(P0)).:(Q))=(dist_min(P0)).:(Q) & lower_bound([#] (( dist_min( P0)).:(Q)))=lower_bound((dist_min(P0)).:(Q)) by WEIERSTR:def 1,def 3; then A10: lower_bound((dist_min(P0)).:(Q))=(dist_min(P0)).o by A9,SEQ_4:9; A11: |.w01.|=|.w01-0.TOP-REAL n.| by RLVECT_1:13 .=dist(x1,x2) by A7,JGRAPH_1:28; |.w01.| <> 0 by A1,A2,A4,TOPRNS_1:24; hence thesis by A1,A4,A6,A10,A11,WEIERSTR:def 7; end; theorem Th42: for a being Real, Q being Subset of TOP-REAL n, w1,w4 being Point of TOP-REAL n st Q={q : (|.q.|) > a } & w1 in Q & w4 in Q & not (ex r being Real st w1=r*w4 or w4=r*w1) holds ex w2,w3 being Point of TOP-REAL n st w2 in Q & w3 in Q & LSeg(w1,w2) c=Q & LSeg(w2,w3) c= Q & LSeg(w3,w4) c= Q proof let a be Real, Q be Subset of TOP-REAL n, w1,w4 be Point of TOP-REAL n; the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8; then reconsider P=LSeg(w1,w4) as Subset of TopSpaceMetr(Euclid n); assume A1: Q={q : (|.q.|) > a } & w1 in Q & w4 in Q & not (ex r being Real st w1=r*w4 or w4=r*w1); then not (0.TOP-REAL n) in LSeg(w1,w4) by RLTOPSP1:71; then consider w0 being Point of TOP-REAL n such that w0 in LSeg(w1,w4) and A2: |.w0.|>0 and A3: |.w0.|=(dist_min(P)).(0.TOP-REAL n) by Th41; set l9=(a+1)/|.w0.|; set w2= l9*w1,w3=l9*w4; A4: LSeg(w2,w3)c=Q proof the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8; then reconsider P=LSeg(w1,w4) as Subset of TopSpaceMetr(Euclid n); reconsider o=0.TOP-REAL n as Point of Euclid n by EUCLID:67; let x be set; A5: abs l9 = abs(a+1)/abs |.w0.| by COMPLEX1:67 .=abs(a+1)/|.w0.| by ABSVALUE:def 1; (dist(o)).:(P) c= REAL proof let x be set; assume x in ((dist(o)).:(P)); then consider z being set such that z in dom (dist(o)) and z in P and A6: x=(dist(o)).z by FUNCT_1:def 6; thus thesis by A6; end; then reconsider F=((dist(o)).:(P)) as Subset of REAL; assume x in LSeg(w2,w3); then consider r such that A7: x=(1-r)*w2 + r*w3 and A8: 0 <= r & r <= 1; reconsider w5=(1-r)*w1 + r*w4 as Point of TOP-REAL n; reconsider w59=w5 as Point of Euclid n by TOPREAL3:8; A9: dist(w59,o)=(dist(o)).w59 by WEIERSTR:def 4; 0 is LowerBound of (dist o).:P proof let r be ext-real number; assume r in ((dist(o)).:(P)); then consider x being set such that x in dom (dist(o)) and A10: x in P and A11: r=(dist(o)).x by FUNCT_1:def 6; reconsider w0=x as Point of Euclid n by A10,TOPREAL3:8; r=dist(w0,o) by A11,WEIERSTR:def 4; hence thesis by METRIC_1:5; end; then A12: F is bounded_below by XXREAL_2:def 9; the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8; then w59 in the carrier of TopSpaceMetr(Euclid n); then A13: w59 in dom (dist(o)) by FUNCT_2:def 1; w5 in LSeg(w1,w4) by A8; then dist(w59,o) in ((dist(o)).:(P)) by A13,A9,FUNCT_1:def 6; then lower_bound F <=dist(w59,o) by A12,SEQ_4:def 2; then dist(w59,o)>= lower_bound([#]((dist(o)).:(P))) by WEIERSTR:def 1; then dist(w59,o)>= lower_bound((dist(o)).:(P)) by WEIERSTR:def 3; then dist(w59,o)>=|.w0.| by A3,WEIERSTR:def 6; then |.w5-0.TOP-REAL n.| >=|.w0.| by JGRAPH_1:28; then |.w5.| >=|.w0.| by RLVECT_1:13; then abs(a+1)>=0 & |.w5.|/|.w0.|>=1 by A2,COMPLEX1:46,XREAL_1:181; then abs(a+1)*(|.w5.|/|.w0.|)>=abs(a+1)*1 by XREAL_1:66; then abs(a+1)*(|.w0.|"*|.w5.|)>=abs(a+1) by XCMPLX_0:def 9; then abs(a+1)*|.w0.|"*|.w5.|>=abs(a+1); then A14: abs(a+1)/|.w0.|*|.w5.|>=abs(a+1) by XCMPLX_0:def 9; a+1>a & abs(a+1)>=a+1 by ABSVALUE:4,XREAL_1:29; then abs(a+1)>a by XXREAL_0:2; then abs(a+1)/|.w0.|*|.w5.|>a by A14,XXREAL_0:2; then |.l9*((1-r)*w1 + r*w4).|>a by A5,TOPRNS_1:7; then |.l9*((1-r)*w1) + l9*(r*w4).|>a by EUCLID:32; then |.l9*((1-r)*w1) + (l9*r)*w4.|>a by EUCLID:30; then |.(l9*(1-r))*w1 + (l9*r)*w4.|>a by EUCLID:30; then |.((1-r)*l9)*w1 + r*(l9*w4).|>a by EUCLID:30; then |.(1-r)*w2 + r*w3.|>a by EUCLID:30; hence thesis by A1,A7; end; A15: w3 in LSeg(w2,w3) by RLTOPSP1:68; then A16: w3 in Q by A4; A17: LSeg(w4,w3) c=Q proof let x be set; assume x in LSeg(w4,w3); then consider r such that A18: x=(1-r)*w4 + r*w3 and A19: 0 <= r and A20: r <= 1; now per cases; case A21: a>=0; the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8; then reconsider P=LSeg(w4,w1) as Subset of TopSpaceMetr(Euclid n); reconsider o=0.TOP-REAL n as Point of Euclid n by EUCLID:67; reconsider w5=(1-0)*w4 + 0 * w1 as Point of TOP-REAL n; A22: (1-0)*w4+0 * w1=(1-0)*w4+0.TOP-REAL n by EUCLID:29 .=(1-0)*w4 by EUCLID:27 .=w4 by EUCLID:29; (dist(o)).:(P) c= REAL proof let x be set; assume x in ((dist(o)).:(P)); then consider z being set such that z in dom (dist(o)) and z in P and A23: x=(dist(o)).z by FUNCT_1:def 6; thus thesis by A23; end; then reconsider F=((dist(o)).:(P)) as Subset of REAL; reconsider w59=w5 as Point of Euclid n by TOPREAL3:8; A24: dist(w59,o)=(dist(o)).w59 by WEIERSTR:def 4; 0 is LowerBound of (dist o).:P proof let r be ext-real number; assume r in ((dist(o)).:(P)); then consider x being set such that x in dom (dist(o)) and A25: x in P and A26: r=(dist(o)).x by FUNCT_1:def 6; reconsider w0=x as Point of Euclid n by A25,TOPREAL3:8; r=dist(w0,o) by A26,WEIERSTR:def 4; hence thesis by METRIC_1:5; end; then A27: F is bounded_below by XXREAL_2:def 9; the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8; then w59 in the carrier of TopSpaceMetr(Euclid n); then A28: w59 in dom (dist(o)) by FUNCT_2:def 1; w5 in {(1-r1)*w4 + r1 * w1:0 <= r1 & r1 <= 1}; then dist(w59,o) in ((dist(o)).:(P)) by A28,A24,FUNCT_1:def 6; then lower_bound F <=dist(w59,o) by A27,SEQ_4:def 2; then dist(w59,o)>= lower_bound([#]((dist(o)).:(P))) by WEIERSTR:def 1; then dist(w59,o)>= lower_bound((dist(o)).:(P)) by WEIERSTR:def 3; then dist(w59,o)>=|.w0.| by A3,WEIERSTR:def 6; then |.w5-0.TOP-REAL n.| >=|.w0.| by JGRAPH_1:28; then A29: |.w5.| >=|.w0.| by RLVECT_1:13; r*l9*|.w0.| =r*(a+1)/|.w0.|*|.w0.| by XCMPLX_1:74 .=r*(a+1) by A2,XCMPLX_1:87; then A30: r*l9*|.w4.|>= r*(a+1) by A19,A21,A22,A29,XREAL_1:64; A31: 1-r>=0 by A20,XREAL_1:48; A32: a+r>=a+0 by A19,XREAL_1:6; A33: ex q1 being Point of TOP-REAL n st q1=w4 & |.q1.| > a by A1; now per cases; case 1-r>0; then A34: (1-r)*|.w4.|>(1-r)*a by A33,XREAL_1:68; abs((1-r)+ r*l9)*|.w4.|=((1-r)+ r*l9)*|.w4.| by A19,A21,A31, ABSVALUE:def 1 .= (1-r)*|.w4.|+r*l9*|.w4.|; then abs((1-r)+r*l9)*|.w4.|>r*(a+1)+(1-r)*a by A30,A34,XREAL_1:8; then abs((1-r)+r*l9)*|.w4.|>a by A32,XXREAL_0:2; then |.((1-r)+ r*l9)*w4.|>a by TOPRNS_1:7; then |.(1-r)*w4 + r*l9*w4.|>a by EUCLID:33; hence |.(1-r)*w4 + r*w3.|>a by EUCLID:30; end; case 1-r<=0; then 1-r+r<=0+r by XREAL_1:6; then r=1 by A20,XXREAL_0:1; then A35: (1-r)*w4+r*w3=0.TOP-REAL n +1 * w3 by EUCLID:29 .=0.TOP-REAL n +w3 by EUCLID:29 .=w3 by EUCLID:27; ex q3 being Point of TOP-REAL n st q3=w3 & |.q3.| > a by A1,A16; hence |.(1-r)*w4 + r*w3.|>a by A35; end; end; hence |.(1-r)*w4 + r*w3.|>a; end; case a<0; hence |.(1-r)*w4 + r*w3.|>a; end; end; hence thesis by A1,A18; end; A36: w2 in LSeg(w2,w3) by RLTOPSP1:68; then A37: w2 in Q by A4; LSeg(w1,w2) c=Q proof let x be set; assume x in LSeg(w1,w2); then consider r such that A38: x=(1-r)*w1 + r*w2 and A39: 0 <= r and A40: r <= 1; now per cases; case A41: a>=0; the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8; then reconsider P=LSeg(w1,w4) as Subset of TopSpaceMetr(Euclid n); reconsider o=0.TOP-REAL n as Point of Euclid n by EUCLID:67; reconsider w5=(1-0)*w1 + 0 * w4 as Point of TOP-REAL n; A42: (1-0)*w1+0 * w4=(1-0)*w1+0.TOP-REAL n by EUCLID:29 .=(1-0)*w1 by EUCLID:27 .=w1 by EUCLID:29; ((dist(o)).:(P)) c= REAL proof let x be set; assume x in ((dist(o)).:(P)); then consider z being set such that z in dom (dist(o)) and z in P and A43: x=(dist(o)).z by FUNCT_1:def 6; thus thesis by A43; end; then reconsider F=((dist(o)).:(P)) as Subset of REAL; reconsider w59=w5 as Point of Euclid n by TOPREAL3:8; 0 is LowerBound of (dist o).:P proof let r be ext-real number; assume r in ((dist(o)).:(P)); then consider x being set such that x in dom (dist(o)) and A44: x in P and A45: r=(dist(o)).x by FUNCT_1:def 6; reconsider w0=x as Point of Euclid n by A44,TOPREAL3:8; r=dist(w0,o) by A45,WEIERSTR:def 4; hence thesis by METRIC_1:5; end; then A46: F is bounded_below by XXREAL_2:def 9; the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8; then w59 in the carrier of TopSpaceMetr(Euclid n); then A47: w59 in dom (dist(o)) by FUNCT_2:def 1; w5 in LSeg(w1,w4) & dist(w59,o)=(dist(o)).w59 by WEIERSTR:def 4; then dist(w59,o) in ((dist(o)).:(P)) by A47,FUNCT_1:def 6; then lower_bound F <=dist(w59,o) by A46,SEQ_4:def 2; then dist(w59,o)>= lower_bound([#]((dist(o)).:(P))) by WEIERSTR:def 1; then dist(w59,o)>= lower_bound((dist(o)).:(P)) by WEIERSTR:def 3; then dist(w59,o)>=|.w0.| by A3,WEIERSTR:def 6; then |.w5-0.TOP-REAL n.| >=|.w0.| by JGRAPH_1:28; then A48: |.w5.| >=|.w0.| by RLVECT_1:13; r*l9*|.w0.| =r*(a+1)/|.w0.|*|.w0.| by XCMPLX_1:74 .=r*(a+1) by A2,XCMPLX_1:87; then A49: r*l9*|.w1.|>= r*(a+1) by A39,A41,A42,A48,XREAL_1:64; A50: ex q1 being Point of TOP-REAL n st q1=w1 & |.q1.| > a by A1; A51: a+r>=a+0 by A39,XREAL_1:6; A52: 1-r>=0 by A40,XREAL_1:48; A53: ex q2 being Point of TOP-REAL n st q2=w2 & |.q2.| > a by A1,A37; now per cases; case 1-r>0; then A54: (1-r)*|.w1.|>(1-r)*a by A50,XREAL_1:68; abs((1-r)+ r*l9)*|.w1.|=((1-r)+ r*l9)*|.w1.| by A39,A41,A52, ABSVALUE:def 1 .= (1-r)*|.w1.|+r*l9*|.w1.|; then abs((1-r)+ r*l9)*|.w1.|>r*(a+1)+(1-r)*a by A49,A54,XREAL_1:8; then abs((1-r)+ r*l9)*|.w1.|>a by A51,XXREAL_0:2; then |.((1-r)+ r*l9)*w1.|>a by TOPRNS_1:7; then |.(1-r)*w1 + r*l9*w1.|>a by EUCLID:33; hence |.(1-r)*w1 + r*w2.|>a by EUCLID:30; end; case 1-r<=0; then 1-r+r<=0+r by XREAL_1:6; then r=1 by A40,XXREAL_0:1; then (1-r)*w1+r*w2=0.TOP-REAL n +1 * w2 by EUCLID:29 .=0.TOP-REAL n +w2 by EUCLID:29 .=w2 by EUCLID:27; hence |.(1-r)*w1 + r*w2.|>a by A53; end; end; hence |.(1-r)*w1 + r*w2.|>a; end; case a<0; hence |.(1-r)*w1 + r*w2.|>a; end; end; hence thesis by A1,A38; end; hence thesis by A4,A36,A15,A17; end; theorem Th43: for a being Real, Q being Subset of TOP-REAL n, w1,w4 being Point of TOP-REAL n st Q=(REAL n)\ {q : (|.q.|) < a } & w1 in Q & w4 in Q & not (ex r being Real st w1=r*w4 or w4=r*w1) holds ex w2,w3 being Point of TOP-REAL n st w2 in Q & w3 in Q & LSeg(w1,w2) c=Q & LSeg(w2,w3) c= Q & LSeg(w3,w4) c= Q proof let a be Real, Q be Subset of TOP-REAL n, w1,w4 be Point of TOP-REAL n; the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8; then reconsider P=LSeg(w1,w4) as Subset of TopSpaceMetr(Euclid n); assume A1: Q=(REAL n)\ {q : (|.q.|) < a } & w1 in Q & w4 in Q & not (ex r being Real st w1=r*w4 or w4=r*w1); then not (0.TOP-REAL n) in LSeg(w1,w4) by RLTOPSP1:71; then consider w0 being Point of TOP-REAL n such that w0 in LSeg(w1,w4) and A2: |.w0.|>0 and A3: |.w0.|=(dist_min(P)).(0.TOP-REAL n) by Th41; set l9=a/|.w0.|; set w2= l9*w1,w3=l9*w4; A4: (REAL n)\ {q : (|.q.|) < a } = {q1 : (|.q1.|) >= a } proof thus (REAL n)\ {q : (|.q.|) < a } c= {q1 : (|.q1.|) >= a } proof let z be set; assume A5: z in (REAL n)\ {q : (|.q.|) < a }; then reconsider q2=z as Point of TOP-REAL n by EUCLID:22; not z in {q : (|.q.|) < a } by A5,XBOOLE_0:def 5; then |.q2.| >= a; hence thesis; end; let z be set; assume z in {q1 : (|.q1.|) >= a }; then consider q1 such that A6: z=q1 and A7: (|.q1.|) >= a; q1 in the carrier of TOP-REAL n; then A8: z in REAL n by A6,EUCLID:22; for q st q=z holds (|.q.|) >= a by A6,A7; then not z in {q : (|.q.|) < a }; hence thesis by A8,XBOOLE_0:def 5; end; A9: LSeg(w1,w2) c=Q proof let x be set; assume x in LSeg(w1,w2); then consider r such that A10: x=(1-r)*w1 + r*w2 and A11: 0 <= r and A12: r <= 1; now per cases; case A13: a>0; the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8; then reconsider P=LSeg(w1,w4) as Subset of TopSpaceMetr(Euclid n); reconsider o=0.TOP-REAL n as Point of Euclid n by EUCLID:67; reconsider w5=(1-0)*w1 + 0 * w4 as Point of TOP-REAL n; A14: (1-0)*w1+0 * w4=(1-0)*w1+0.TOP-REAL n by EUCLID:29 .=(1-0)*w1 by EUCLID:27 .=w1 by EUCLID:29; ((dist(o)).:(P)) c= REAL proof let x be set; assume x in ((dist(o)).:(P)); then consider z being set such that z in dom (dist(o)) and z in P and A15: x=(dist(o)).z by FUNCT_1:def 6; thus thesis by A15; end; then reconsider F=((dist(o)).:(P)) as Subset of REAL; reconsider w59=w5 as Point of Euclid n by TOPREAL3:8; 0 is LowerBound of (dist o).:P proof let r be ext-real number; assume r in ((dist(o)).:(P)); then consider x being set such that x in dom (dist(o)) and A16: x in P and A17: r=(dist(o)).x by FUNCT_1:def 6; reconsider w0=x as Point of Euclid n by A16,TOPREAL3:8; r=dist(w0,o) by A17,WEIERSTR:def 4; hence thesis by METRIC_1:5; end; then A18: F is bounded_below by XXREAL_2:def 9; the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8; then w59 in the carrier of TopSpaceMetr(Euclid n); then A19: w59 in dom (dist(o)) by FUNCT_2:def 1; w5 in LSeg(w1,w4) & dist(w59,o)=(dist(o)).w59 by WEIERSTR:def 4; then dist(w59,o) in ((dist(o)).:(P)) by A19,FUNCT_1:def 6; then lower_bound F <=dist(w59,o) by A18,SEQ_4:def 2; then dist(w59,o)>= lower_bound([#]((dist(o)).:(P))) by WEIERSTR:def 1; then dist(w59,o)>= lower_bound((dist(o)).:(P)) by WEIERSTR:def 3; then dist(w59,o)>=|.w0.| by A3,WEIERSTR:def 6; then |.w5-0.TOP-REAL n.| >=|.w0.| by JGRAPH_1:28; then A20: |.w5.| >=|.w0.| by RLVECT_1:13; A21: 1-r>=0 by A12,XREAL_1:48; then A22: abs((1-r)+r*l9)*|.w1.|=((1-r)+ r*l9)*|.w1.| by A11,A13,ABSVALUE:def 1 .= (1-r)*|.w1.|+r*l9*|.w1.|; ex q1 being Point of TOP-REAL n st q1=w1 & |.q1.| >= a by A1,A4; then A23: (1-r)*|.w1.|>=(1-r)*a by A21,XREAL_1:64; r*l9*|.w0.| =r*a/|.w0.|*|.w0.| by XCMPLX_1:74 .=r*a by A2,XCMPLX_1:87; then r*l9*|.w1.|>= r*a by A11,A13,A14,A20,XREAL_1:64; then abs((1-r)+r*l9)*|.w1.|>=r*a+(1-r)*a by A23,A22,XREAL_1:7; then |.((1-r)+ r*l9)*w1.|>=a by TOPRNS_1:7; then |.(1-r)*w1 + r*l9*w1.|>=a by EUCLID:33; hence |.(1-r)*w1 + r*w2.|>=a by EUCLID:30; end; case a<=0; hence |.(1-r)*w1 + r*w2.|>=a; end; end; hence thesis by A1,A4,A10; end; A24: LSeg(w4,w3) c=Q proof let x be set; assume x in LSeg(w4,w3); then consider r such that A25: x=(1-r)*w4 + r*w3 and A26: 0 <= r and A27: r <= 1; now per cases; case A28: a>0; the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8; then reconsider P=LSeg(w4,w1) as Subset of TopSpaceMetr(Euclid n); reconsider o=0.TOP-REAL n as Point of Euclid n by EUCLID:67; reconsider w5=(1-0)*w4 + 0 * w1 as Point of TOP-REAL n; A29: (1-0)*w4+0 * w1=(1-0)*w4+0.TOP-REAL n by EUCLID:29 .=(1-0)*w4 by EUCLID:27 .=w4 by EUCLID:29; ((dist(o)).:(P)) c= REAL proof let x be set; assume x in ((dist(o)).:(P)); then consider z being set such that z in dom (dist(o)) and z in P and A30: x=(dist(o)).z by FUNCT_1:def 6; thus thesis by A30; end; then reconsider F=((dist(o)).:(P)) as Subset of REAL; reconsider w59=w5 as Point of Euclid n by TOPREAL3:8; A31: dist(w59,o)=(dist(o)).w59 by WEIERSTR:def 4; 0 is LowerBound of (dist o).:P proof let r be ext-real number; assume r in ((dist(o)).:(P)); then consider x being set such that x in dom (dist(o)) and A32: x in P and A33: r=(dist(o)).x by FUNCT_1:def 6; reconsider w0=x as Point of Euclid n by A32,TOPREAL3:8; r=dist(w0,o) by A33,WEIERSTR:def 4; hence thesis by METRIC_1:5; end; then A34: F is bounded_below by XXREAL_2:def 9; the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8; then w59 in the carrier of TopSpaceMetr(Euclid n); then A35: w59 in dom (dist(o)) by FUNCT_2:def 1; w5 in {(1-r1)*w4 + r1 * w1:0 <= r1 & r1 <= 1}; then dist(w59,o) in ((dist(o)).:(P)) by A35,A31,FUNCT_1:def 6; then lower_bound F <=dist(w59,o) by A34,SEQ_4:def 2; then dist(w59,o)>= lower_bound([#]((dist(o)).:(P))) by WEIERSTR:def 1; then dist(w59,o)>= lower_bound((dist(o)).:(P)) by WEIERSTR:def 3; then dist(w59,o)>=|.w0.| by A3,WEIERSTR:def 6; then |.w5-0.TOP-REAL n.| >=|.w0.| by JGRAPH_1:28; then A36: |.w5.| >=|.w0.| by RLVECT_1:13; A37: 1-r>=0 by A27,XREAL_1:48; then A38: abs((1-r)+r*l9)*|.w4.|=((1-r)+ r*l9)*|.w4.| by A26,A28,ABSVALUE:def 1 .= (1-r)*|.w4.|+r*l9*|.w4.|; ex q1 being Point of TOP-REAL n st q1=w4 & |.q1.| >= a by A1,A4; then A39: (1-r)*|.w4.|>=(1-r)*a by A37,XREAL_1:64; r*l9*|.w0.| =r*a/|.w0.|*|.w0.| by XCMPLX_1:74 .=r*a by A2,XCMPLX_1:87; then r*l9*|.w4.|>= r*a by A26,A28,A29,A36,XREAL_1:64; then abs((1-r)+r*l9)*|.w4.|>=r*a+(1-r)*a by A39,A38,XREAL_1:7; then |.((1-r)+ r*l9)*w4.|>=a by TOPRNS_1:7; then |.(1-r)*w4 + r*l9*w4.|>=a by EUCLID:33; hence |.(1-r)*w4 + r*w3.|>=a by EUCLID:30; end; case a<=0; hence |.(1-r)*w4 + r*w3.|>=a; end; end; hence thesis by A1,A4,A25; end; A40: LSeg(w2,w3)c=Q proof the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8; then reconsider P=LSeg(w1,w4) as Subset of TopSpaceMetr(Euclid n); reconsider o=0.TOP-REAL n as Point of Euclid n by EUCLID:67; let x be set; A41: abs l9=abs(a)/(abs|.w0.|) by COMPLEX1:67 .=abs(a)/|.w0.| by ABSVALUE:def 1; ((dist(o)).:(P)) c= REAL proof let x be set; assume x in ((dist(o)).:(P)); then consider z being set such that z in dom (dist(o)) and z in P and A42: x=(dist(o)).z by FUNCT_1:def 6; thus thesis by A42; end; then reconsider F=(dist(o)).:(P) as Subset of REAL; assume x in LSeg(w2,w3); then consider r such that A43: x=(1-r)*w2 + r*w3 and A44: 0 <= r & r <= 1; reconsider w5=(1-r)*w1 + r*w4 as Point of TOP-REAL n; reconsider w59=w5 as Point of Euclid n by TOPREAL3:8; A45: dist(w59,o)=(dist(o)).w59 by WEIERSTR:def 4; 0 is LowerBound of (dist o).:P proof let r be ext-real number; assume r in ((dist(o)).:(P)); then consider x being set such that x in dom (dist(o)) and A46: x in P and A47: r=(dist(o)).x by FUNCT_1:def 6; reconsider w0=x as Point of Euclid n by A46,TOPREAL3:8; r=dist(w0,o) by A47,WEIERSTR:def 4; hence thesis by METRIC_1:5; end; then A48: F is bounded_below by XXREAL_2:def 9; the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8; then w59 in the carrier of TopSpaceMetr(Euclid n); then A49: w59 in dom (dist(o)) by FUNCT_2:def 1; w5 in LSeg(w1,w4) by A44; then dist(w59,o) in ((dist(o)).:(P)) by A49,A45,FUNCT_1:def 6; then lower_bound F <=dist(w59,o) by A48,SEQ_4:def 2; then dist(w59,o)>= lower_bound([#]((dist(o)).:(P))) by WEIERSTR:def 1; then dist(w59,o)>= lower_bound((dist(o)).:(P)) by WEIERSTR:def 3; then dist(w59,o)>=|.w0.| by A3,WEIERSTR:def 6; then |.w5-0.TOP-REAL n.| >=|.w0.| by JGRAPH_1:28; then |.w5.| >=|.w0.| by RLVECT_1:13; then abs(a)>=0 & |.w5.|/|.w0.|>=1 by A2,COMPLEX1:46,XREAL_1:181; then abs(a)*(|.w5.|/|.w0.|)>=abs(a)*1 by XREAL_1:66; then abs(a)*(|.w5.|*|.w0.|")>=abs(a) by XCMPLX_0:def 9; then abs(a)*|.w0.|"*|.w5.|>=abs(a); then A50: abs(a)/|.w0.|*|.w5.|>=abs(a) by XCMPLX_0:def 9; abs(a)>=a by ABSVALUE:4; then abs(a)/|.w0.|*|.w5.|>=a by A50,XXREAL_0:2; then |.l9*((1-r)*w1 + r*w4).|>=a by A41,TOPRNS_1:7; then |.l9*((1-r)*w1) + l9*(r*w4).|>=a by EUCLID:32; then |.l9*((1-r)*w1) + (l9*r)*w4.|>=a by EUCLID:30; then |.(l9*(1-r))*w1 + (l9*r)*w4.|>=a by EUCLID:30; then |.((1-r)*l9)*w1 + r*(l9*w4).|>=a by EUCLID:30; then |.(1-r)*w2 + r*w3.|>=a by EUCLID:30; hence thesis by A1,A4,A43; end; w2 in LSeg(w2,w3) & w3 in LSeg(w2,w3) by RLTOPSP1:68; hence thesis by A40,A9,A24; end; theorem for f being FinSequence of REAL holds f is Element of REAL (len f) & f is Point of TOP-REAL (len f) by EUCLID:76; theorem Th45: for x being Element of REAL n,f,g being FinSequence of REAL, r being Real st f=x & g=r*x holds len f=len g & for i being Element of NAT st 1<= i & i<=len f holds g/.i=r*f/.i proof reconsider h2= (id REAL) as Function; let x be Element of REAL n,f,g be FinSequence of REAL,r be Real; assume that A1: f=x and A2: g=r*x; A3: len f=n by A1,CARD_1:def 7; set h1= (dom (id REAL)) --> r; A4: dom (<:h1, h2:>)=dom (h1) /\ dom ((id REAL)) by FUNCT_3:def 7; A5: len g=n by A2,CARD_1:def 7; A6: g= (multreal * (<:h1, h2:>))*x by A2,FUNCOP_1:def 5; for i being Element of NAT st 1<=i & i<=len f holds g/.i=r*f/.i proof let i be Element of NAT; A7: dom h1=dom (id REAL) by FUNCOP_1:13 .=REAL by FUNCT_1:17; dom h2=REAL by FUNCT_1:17; then A8: h1.(x.i) = r by FUNCOP_1:7; A9: h2.(x.i)=x.i by FUNCT_1:17; assume A10: 1<=i & i<=len f; then A11: f.i=f/.i by FINSEQ_4:15; i in Seg len f by A10,FINSEQ_1:1; then i in dom g by A3,A5,FINSEQ_1:def 3; then A12: g.i=(multreal * (<:h1, h2:>)).(x.i) by A6,FUNCT_1:12; A13: dom (<:h1, h2:>)=dom h1 /\ REAL by A4,FUNCT_1:17; then (<:h1, h2:>).(x.i)=[h1.(x.i),h2.(x.i)] by A7,FUNCT_3:def 7; then g.i=multreal.(r,f.i) by A1,A12,A13,A7,A8,A9,FUNCT_1:13; then g.i=r*(f/.i) by A11,BINOP_2:def 11; hence thesis by A3,A5,A10,FINSEQ_4:15; end; hence thesis by A2,A3,CARD_1:def 7; end; theorem Th46: for x being Element of REAL n,f being FinSequence st x<> 0*n & x =f holds ex i being Element of NAT st 1<=i & i<=n & f.i<>0 proof let x be Element of REAL n,f be FinSequence; assume that A1: x<> 0*n and A2: x=f; A3: len f=n by A2,CARD_1:def 7; assume A4: not ex i being Element of NAT st 1<=i & i<=n & f.i<>0; for z being set holds z in f iff ex x,y st x in Seg n & y in {0} & z = [ x,y] proof let z be set; hereby assume A5: z in f; then consider x0,y0 being set such that A6: z = [x0,y0] by RELAT_1:def 1; A7: y0=f.x0 by A5,A6,FUNCT_1:1; A8: x0 in dom f by A5,A6,XTUPLE_0:def 12; then reconsider n1=x0 as Element of NAT; A9: x0 in Seg len f by A8,FINSEQ_1:def 3; then 1<=n1 & n1<=len f by FINSEQ_1:1; then f.n1=0 by A3,A4; then y0 in {0} by A7,TARSKI:def 1; hence ex x,y st x in Seg n & y in {0} & z = [x,y] by A3,A6,A9; end; given x,y such that A10: x in Seg n and A11: y in {0} and A12: z = [x,y]; reconsider n1=x as Element of NAT by A10; A13: n1<=n by A10,FINSEQ_1:1; A14: x in dom f by A3,A10,FINSEQ_1:def 3; y=0 & 1<=n1 by A10,A11,FINSEQ_1:1,TARSKI:def 1; then y=f.x by A4,A13; hence thesis by A12,A14,FUNCT_1:1; end; then f=[:Seg n,{0}:] by ZFMISC_1:def 2; hence contradiction by A1,A2,FUNCOP_1:def 2; end; theorem Th47: for x being Element of REAL n st n>=2 & x<> 0*n holds ex y being Element of REAL n st not ex r being Real st y=r*x or x=r*y proof let x be Element of REAL n; assume that A1: n>=2 and A2: x<> 0*n; reconsider f=x as FinSequence of REAL; consider i2 being Element of NAT such that A3: 1<=i2 and A4: i2<=n and A5: f.i2<>0 by A2,Th46; A6: len f=n by CARD_1:def 7; then A7: 1<=len f by A1,XXREAL_0:2; per cases; suppose A8: i2>1; reconsider g=(<*((f/.1)+1)*>)^mid(f,2,len f) as FinSequence of REAL; A9: len (mid(f,2,len f))=len f-'2+1 by A1,A6,A7,FINSEQ_6:118 .=len f-2+1 by A1,A6,XREAL_1:233; len g=len (<*(f/.1+1)*>) + len (mid(f,2,len f)) by FINSEQ_1:22; then A10: len g=1+(len f-2+1) by A9,FINSEQ_1:39 .=len f; then reconsider y2=g as Element of REAL n by A6,EUCLID:76; A11: len (<*(f/.1+1)*>)=1 by FINSEQ_1:39; now given r being Real such that A12: y2=r*x or x=r*y2; per cases by A12; suppose A13: y2=r*x; i2<=len f-(1+1)+(1+1) by A4,CARD_1:def 7; then A14: i2-1<=len f-(1+1)+1+1-1 by XREAL_1:9; A15: i2-'1=i2-1 & 1<=i2-'1 by A8,NAT_D:49,XREAL_1:233; A16: 1<=len f by A1,A6,XXREAL_0:2; then A17: g/.1=g.1 by A10,FINSEQ_4:15; A18: g/.i2=g.i2 by A3,A4,A6,A10,FINSEQ_4:15; A19: i2-'1+2-'1=i2-'1+1+1-'1 .=i2-'1+1 by NAT_D:34 .=i2-1+1 by A3,XREAL_1:233 .=i2; A20: f/.i2=f.i2 by A3,A4,A6,FINSEQ_4:15; 1+1<=i2 & i2<=1+len (mid(f,2,len f)) by A4,A8,A9,CARD_1:def 7,NAT_1:13 ; then g.i2= (mid(f,2,len f)).(i2-1) by A11,FINSEQ_1:23 .=f.i2 by A1,A6,A9,A16,A15,A14,A19,FINSEQ_6:118; then 1 * f/.i2=r*f/.i2 by A3,A4,A6,A13,A18,A20,Th45; then A21: 1=r by A5,A20,XCMPLX_1:5; g/.1=r*f/.1 by A13,A16,Th45; then f/.1+1=1 * f/.1 by A21,A17,FINSEQ_1:41; hence contradiction; end; suppose A22: x=r*y2; i2<=len f-(1+1)+(1+1) by A4,CARD_1:def 7; then A23: i2-1<=len f-(1+1)+1+1-1 by XREAL_1:9; A24: i2-'1=i2-1 & 1<=i2-'1 by A8,NAT_D:49,XREAL_1:233; A25: 1<=len f by A1,A6,XXREAL_0:2; then A26: g/.1=g.1 by A10,FINSEQ_4:15; A27: g/.i2=g.i2 by A3,A4,A6,A10,FINSEQ_4:15; A28: i2-'1+2-'1=i2-'1+1+1-'1 .=i2-'1+1 by NAT_D:34 .=i2-1+1 by A3,XREAL_1:233 .=i2; A29: f/.i2=f.i2 by A3,A4,A6,FINSEQ_4:15; 1+1<=i2 & i2<=1+len (mid(f,2,len f)) by A4,A8,A9,CARD_1:def 7,NAT_1:13 ; then g.i2= (mid(f,2,len f)).(i2-1) by A11,FINSEQ_1:23 .=f.i2 by A1,A6,A9,A25,A24,A23,A28,FINSEQ_6:118; then 1 * f/.i2=r*f/.i2 by A3,A4,A6,A10,A22,A27,A29,Th45; then A30: 1=r by A5,A29,XCMPLX_1:5; f/.1=r*g/.1 by A10,A22,A25,Th45; then f/.1+1=1 * f/.1 by A30,A26,FINSEQ_1:41; hence contradiction; end; end; hence thesis; end; suppose A31: i2<=1; reconsider g=mid(f,1,len f-'1)^<*(f/.len f+1)*> as FinSequence of REAL; A32: len f-'1<=len f by NAT_D:44; A33: 1+1-1<=len f-1 by A1,A6,XREAL_1:9; A34: len f-'1=len f-1 by A1,A6,XREAL_1:233,XXREAL_0:2; then A35: len f-'1-'1+1=len f-1-1+1 by A33,XREAL_1:233 .=len f-(1+1)+1; then A36: len (mid(f,1,len f-'1)) =len f-1 by A7,A34,A32,A33,FINSEQ_6:118; len (<*(f/.len f+1)*>)=1 & len (mid(f,1,len f-'1))=len f-2+1 by A7,A34,A32 ,A33,A35,FINSEQ_1:39,FINSEQ_6:118; then A37: len g=(len f-2+1)+1 by FINSEQ_1:22 .=len f; then reconsider y2=g as Element of REAL n by A6,EUCLID:76; A38: i2=1 by A3,A31,XXREAL_0:1; now given r being Real such that A39: y2=r*x or x=r*y2; per cases by A39; suppose A40: y2=r*x; A41: g/.i2=g.i2 by A3,A4,A6,A37,FINSEQ_4:15; A42: f/.i2=f.i2 by A3,A4,A6,FINSEQ_4:15; g.i2= (mid(f,1,len f-'1)).i2 by A38,A33,A36,FINSEQ_6:109 .=f.i2 by A38,A34,A32,A33,FINSEQ_6:123; then 1 * f/.i2=r*f/.i2 by A3,A4,A6,A40,A41,A42,Th45; then A43: 1=r by A5,A42,XCMPLX_1:5; A44: g.len f= g.(len f -1+1) .=f/.len f+1 by A36,FINSEQ_1:42; A45: 1<=len f by A1,A6,XXREAL_0:2; then A46: g/.len f=g.len f by A37,FINSEQ_4:15; g/.len f=r*f/.len f by A40,A45,Th45; hence contradiction by A43,A46,A44; end; suppose A47: x=r*y2; A48: g/.i2=g.i2 by A3,A4,A6,A37,FINSEQ_4:15; A49: f/.i2=f.i2 by A3,A4,A6,FINSEQ_4:15; g.i2= (mid(f,1,len f-'1)).i2 by A38,A33,A36,FINSEQ_6:109 .=f.(i2) by A38,A34,A32,A33,FINSEQ_6:123; then 1 * f/.i2=r*f/.i2 by A3,A4,A6,A37,A47,A48,A49,Th45; then A50: 1=r by A5,A49,XCMPLX_1:5; A51: g.len f=g.(len f-1+1) .=f/.len f+1 by A36,FINSEQ_1:42; A52: 1<=len f by A1,A6,XXREAL_0:2; then A53: g/.len f=g.len f by A37,FINSEQ_4:15; f/.len f=r*g/.len f by A37,A47,A52,Th45; hence contradiction by A50,A53,A51; end; end; hence thesis; end; end; theorem Th48: for a being Real, Q being Subset of TOP-REAL n, w1,w7 being Point of TOP-REAL n st n>=2 & Q={q : (|.q.|) > a } & w1 in Q & w7 in Q & (ex r being Real st w1=r*w7 or w7=r*w1) holds ex w2,w3,w4,w5,w6 being Point of TOP-REAL n st w2 in Q & w3 in Q & w4 in Q & w5 in Q & w6 in Q & LSeg(w1,w2) c=Q & LSeg(w2,w3) c= Q & LSeg(w3,w4) c= Q & LSeg(w4,w5) c= Q & LSeg(w5,w6) c=Q & LSeg(w6,w7) c= Q proof let a be Real, Q be Subset of TOP-REAL n, w1,w7 be Point of TOP-REAL n; assume A1: n>=2 & Q={q : (|.q.|) > a } & w1 in Q & w7 in Q; reconsider y1=w1 as Element of REAL n by EUCLID:22; given r8 being Real such that A2: w1=r8*w7 or w7=r8*w1; per cases; suppose A3: a>=0; now assume A4: w1=0.TOP-REAL n; ex q st q=w1 & (|.q.|)>a by A1; hence contradiction by A3,A4,TOPRNS_1:23; end; then w1 <> 0*n by EUCLID:70; then consider y being Element of REAL n such that A5: not ex r being Real st y=r*y1 or y1=r*y by A1,Th47; set y4=((a+1)/|.y.|)*y; reconsider w4=y4 as Point of TOP-REAL n by EUCLID:22; A6: now A7: 0 *y1 = 0 * w1 .= 0.TOP-REAL n by EUCLID:29 .=0*n by EUCLID:70; assume |.y.|=0; hence contradiction by A5,A7,EUCLID:8; end; then A8: (a+1)/|.y.|>0 by A3,XREAL_1:139; A9: now reconsider y9=y,y19=y1 as Element of n-tuples_on REAL; given r being Real such that A10: w1=r*w4 or w4=r*w1; per cases by A10; suppose w1=r*w4; then y1=(r*((a+1)/|.y.|))*y by RVSUM_1:49; hence contradiction by A5; end; suppose w4=r*w1; then ((a+1)/|.y.|)"*((a+1)/|.y.|)*y9=((a+1)/|.y.|)"*(r*y1) by RVSUM_1:49; then ((a+1)/|.y.|)"*((a+1)/|.y.|)*y=((a+1)/|.y.|)"*r*y19 by RVSUM_1:49; then 1 *y=((a+1)/|.y.|)"*r*y1 by A8,XCMPLX_0:def 7; then y=((a+1)/|.y.|)"*r*y1 by RVSUM_1:52; hence contradiction by A5; end; end; A11: |.w4.|=abs((a+1)/|.y.|)*|.y.| by EUCLID:11 .= (a+1)/|.y.|*|.y.| by A3,ABSVALUE:def 1 .=a+1 by A6,XCMPLX_1:87; then |.w4.|>a by XREAL_1:29; then A12: w4 in Q by A1; now given r1 being Real such that A13: w4=r1*w7 or w7=r1*w4; A14: now assume r1=0; then A15: w4=0.TOP-REAL n or w7=0.TOP-REAL n by A13,EUCLID:29; ex q7 being Point of TOP-REAL n st q7=w7 & |.q7.|>a by A1; hence contradiction by A3,A11,A15,TOPRNS_1:23; end; per cases by A2; suppose A16: w1=r8*w7; now per cases by A13; case w4=r1*w7; then r1"*w4=r1"*r1*w7 by EUCLID:30; then r1"*w4=1 *w7 by A14,XCMPLX_0:def 7; then r1"*w4=w7 by EUCLID:29; then w1=r8*r1"*w4 by A16,EUCLID:30; hence contradiction by A9; end; case w7=r1*w4; then r1"*w7=r1"*r1*w4 by EUCLID:30; then r1"*w7=1 *w4 by A14,XCMPLX_0:def 7; then r1"*w7=w4 by EUCLID:29; then r1""*w4=r1""*r1"*w7 by EUCLID:30; then r1""*w4=1 *w7 by A14,XCMPLX_0:def 7; then r1""*w4=w7 by EUCLID:29; then w1=r8*r1""*w4 by A16,EUCLID:30; hence contradiction by A9; end; end; hence contradiction; end; suppose A17: w7=r8*w1; A18: now assume r8=0; then A19: w7=0.TOP-REAL n by A17,EUCLID:29; ex q7 being Point of TOP-REAL n st q7=w7 & |.q7.|>a by A1; hence contradiction by A3,A19,TOPRNS_1:23; end; r8"*w7=r8"*r8*w1 by A17,EUCLID:30; then r8"*w7=1 *w1 by A18,XCMPLX_0:def 7; then A20: r8"*w7=w1 by EUCLID:29; now per cases by A13; case w4=r1*w7; then r1"*w4=r1"*r1*w7 by EUCLID:30; then r1"*w4=1 *w7 by A14,XCMPLX_0:def 7; then r1"*w4=w7 by EUCLID:29; then w1=r8"*r1"*w4 by A20,EUCLID:30; hence contradiction by A9; end; case w7=r1*w4; then r1"*w7=r1"*r1*w4 by EUCLID:30; then r1"*w7=1 *w4 by A14,XCMPLX_0:def 7; then r1"*w7=w4 by EUCLID:29; then r1""*w4=r1""*r1"*w7 by EUCLID:30; then r1""*w4=1 *w7 by A14,XCMPLX_0:def 7; then r1""*w4=w7 by EUCLID:29; then w1=r8"*r1""*w4 by A20,EUCLID:30; hence contradiction by A9; end; end; hence contradiction; end; end; then A21: ex w29,w39 being Point of TOP-REAL n st w29 in Q & w39 in Q & LSeg(w4, w29) c=Q & LSeg(w29,w39) c= Q & LSeg(w39,w7) c= Q by A1,A12,Th42; ex w2,w3 being Point of TOP-REAL n st w2 in Q & w3 in Q & LSeg(w1,w2) c=Q & LSeg(w2,w3) c= Q & LSeg(w3,w4) c= Q by A1,A12,A9,Th42; hence thesis by A12,A21; end; suppose A22: a<0; set w2=0.TOP-REAL n; A23: REAL n c= Q proof let x be set; assume x in REAL n; then reconsider w=x as Point of TOP-REAL n by EUCLID:22; |.w.|>=0; hence thesis by A1,A22; end; the carrier of TOP-REAL n=REAL n by EUCLID:22; then A24: Q=the carrier of TOP-REAL n by A23,XBOOLE_0:def 10; then LSeg(w1,w2) c=Q & LSeg(w2,w7) c=Q; hence thesis by A24; end; end; theorem Th49: for a being Real, Q being Subset of TOP-REAL n, w1,w7 being Point of TOP-REAL n st n>=2 & Q=(REAL n)\ {q : (|.q.|) < a } & w1 in Q & w7 in Q & (ex r being Real st w1=r*w7 or w7=r*w1) holds ex w2,w3,w4,w5,w6 being Point of TOP-REAL n st w2 in Q & w3 in Q & w4 in Q & w5 in Q & w6 in Q & LSeg(w1,w2) c=Q & LSeg(w2,w3) c= Q & LSeg(w3,w4) c= Q & LSeg(w4,w5) c= Q & LSeg(w5,w6) c=Q & LSeg(w6,w7) c= Q proof let a be Real, Q be Subset of TOP-REAL n, w1,w7 be Point of TOP-REAL n; reconsider y1=w1 as Element of REAL n by EUCLID:22; assume A1: n>=2 & Q=(REAL n)\ {q : (|.q.|) < a } & w1 in Q & w7 in Q & ex r being Real st w1=r*w7 or w7=r*w1; then consider r8 being Real such that A2: w1=r8*w7 or w7=r8*w1; per cases; suppose A3: a>0; now assume w1=0.TOP-REAL n; then |.w1.|=0 by TOPRNS_1:23; then w1 in {q : (|.q.|) < a } by A3; hence contradiction by A1,XBOOLE_0:def 5; end; then w1 <> 0*n by EUCLID:70; then consider y being Element of REAL n such that A4: not ex r being Real st y=r*y1 or y1=r*y by A1,Th47; set y4=(a/|.y.|)*y; reconsider w4=y4 as Point of TOP-REAL n by EUCLID:22; A5: now A6: 0 *y1 = 0 * w1 .= 0.TOP-REAL n by EUCLID:29 .=0*n by EUCLID:70; assume |.y.|=0; hence contradiction by A4,A6,EUCLID:8; end; then A7: a/|.y.|>0 by A3,XREAL_1:139; A8: now reconsider y9=y,y19=y1 as Element of n-tuples_on REAL; given r being Real such that A9: w1=r*w4 or w4=r*w1; y1=(r*(a/|.y.|))*y or (a/|.y.|)"*(a/|.y.|)*y9=(a/|.y.|)"*(r*y1) by A9,RVSUM_1:49; then y1=(r*(a/|.y.|))*y or (a/|.y.|)"*(a/|.y.|)*y=(a/|.y.|)"*r*y19 by RVSUM_1:49; then A10: y1=(r*(a/|.y.|))*y9 or 1 *y=(a/|.y.|)"*r*y1 by A7,XCMPLX_0:def 7; per cases by A10,RVSUM_1:52; suppose y1=(r*(a/|.y.|))*y; hence contradiction by A4; end; suppose y=(a/|.y.|)"*r*y1; hence contradiction by A4; end; end; A11: |.w4.|=abs(a/|.y.|)*|.y.| by EUCLID:11 .= a/|.y.|*|.y.| by A3,ABSVALUE:def 1 .=a by A5,XCMPLX_1:87; A12: now assume w4 in {q : (|.q.|) < a }; then ex q st q=w4 & (|.q.|) < a; hence contradiction by A11; end; then A13: w4 in Q by A1,XBOOLE_0:def 5; now given r1 being Real such that A14: w4=r1*w7 or w7=r1*w4; A15: now assume r1=0; then w4=0.TOP-REAL n or w7=0.TOP-REAL n by A14,EUCLID:29; then |.w4.|=0 or |.w7.|=0 by TOPRNS_1:23; then w4 in {q : (|.q.|) < a } or w7 in {q2 where q2 is Point of TOP-REAL n: (|.q2.|) < a } by A3; hence contradiction by A1,A12,XBOOLE_0:def 5; end; now per cases by A2; case A16: w1=r8*w7; now per cases by A14; case w4=r1*w7; then r1"*w4=r1"*r1*w7 by EUCLID:30; then r1"*w4=1 *w7 by A15,XCMPLX_0:def 7; then r1"*w4=w7 by EUCLID:29; then w1=r8*r1"*w4 by A16,EUCLID:30; hence contradiction by A8; end; case w7=r1*w4; then r1"*w7=r1"*r1*w4 by EUCLID:30; then r1"*w7=1 *w4 by A15,XCMPLX_0:def 7; then r1"*w7=w4 by EUCLID:29; then r1""*w4=r1""*r1"*w7 by EUCLID:30; then r1""*w4=1 *w7 by A15,XCMPLX_0:def 7; then r1""*w4=w7 by EUCLID:29; then w1=r8*r1""*w4 by A16,EUCLID:30; hence contradiction by A8; end; end; hence contradiction; end; case A17: w7=r8*w1; A18: now assume r8=0; then w7=0.TOP-REAL n by A17,EUCLID:29; then |.w7.|=0 by TOPRNS_1:23; then w7 in {q : (|.q.|) < a } by A3; hence contradiction by A1,XBOOLE_0:def 5; end; r8"*w7=r8"*r8*w1 by A17,EUCLID:30; then r8"*w7=1 *w1 by A18,XCMPLX_0:def 7; then A19: r8"*w7=w1 by EUCLID:29; now per cases by A14; case w4=r1*w7; then r1"*w4=r1"*r1*w7 by EUCLID:30; then r1"*w4=1 *w7 by A15,XCMPLX_0:def 7; then r1"*w4=w7 by EUCLID:29; then w1=r8"*r1"*w4 by A19,EUCLID:30; hence contradiction by A8; end; case w7=r1*w4; then r1"*w7=r1"*r1*w4 by EUCLID:30; then r1"*w7=1 *w4 by A15,XCMPLX_0:def 7; then r1"*w7=w4 by EUCLID:29; then r1""*w4=r1""*r1"*w7 by EUCLID:30; then r1""*w4=1 *w7 by A15,XCMPLX_0:def 7; then r1""*w4=w7 by EUCLID:29; then w1=r8"*r1""*w4 by A19,EUCLID:30; hence contradiction by A8; end; end; hence contradiction; end; end; hence contradiction; end; then A20: ex w29,w39 being Point of TOP-REAL n st w29 in Q & w39 in Q & LSeg(w4, w29) c=Q & LSeg(w29,w39) c= Q & LSeg(w39,w7) c= Q by A1,A13,Th43; ex w2,w3 being Point of TOP-REAL n st w2 in Q & w3 in Q & LSeg(w1,w2) c=Q & LSeg(w2,w3) c= Q & LSeg(w3,w4) c= Q by A1,A13,A8,Th43; hence thesis by A13,A20; end; suppose A21: a<=0; set w2=0.TOP-REAL n; A22: REAL n c= Q proof let x be set; A23: now assume x in {q : (|.q.|) < a }; then ex q being Point of TOP-REAL n st q=x & (|.q.|) < a; hence contradiction by A21; end; assume x in REAL n; hence thesis by A1,A23,XBOOLE_0:def 5; end; the carrier of TOP-REAL n=REAL n by EUCLID:22; then A24: Q=the carrier of TOP-REAL n by A22,XBOOLE_0:def 10; then LSeg(w1,w2) c=Q & LSeg(w2,w7) c=Q; hence thesis by A24; end; end; theorem Th50: for a being Real st n>=1 holds {q: |.q.| >a} <>{} proof let a be Real; assume A1: n>=1; now abs(a+1)>=0 & sqrt 1<=sqrt n by A1,COMPLEX1:46,SQUARE_1:26; then A2: abs(a+1)*1<=abs(a+1)*sqrt n by SQUARE_1:18,XREAL_1:64; A3: a+1<=abs(a+1) by ABSVALUE:4; assume not (a+1)*(1.REAL n) in {q : |.q.| > a }; then A4: |.(a+1)*(1.REAL n).|<=a; A5: a=2 & P={q : |.q.| > a } holds P is connected proof let a be Real, P be Subset of TOP-REAL n; assume A1: n>=2 & P={q : |.q.| > a }; then reconsider Q=P as non empty Subset of TOP-REAL n by Th50,XXREAL_0:2; for w1,w7 being Point of TOP-REAL n st w1 in Q & w7 in Q & w1<>w7 ex f being Function of I[01],((TOP-REAL n) | Q) st f is continuous & w1=f.0 & w7=f.1 proof let w1,w7 be Point of TOP-REAL n; assume that A2: w1 in Q & w7 in Q and w1<>w7; per cases; suppose not (ex r being Real st w1=r*w7 or w7=r*w1); then ex w2,w3 being Point of TOP-REAL n st w2 in Q & w3 in Q & LSeg(w1,w2) c=Q & LSeg(w2,w3) c= Q & LSeg(w3,w7) c= Q by A1,A2,Th42; hence thesis by A2,Th39; end; suppose ex r being Real st w1=r*w7 or w7=r*w1; then ex w2,w3,w4,w5,w6 being Point of TOP-REAL n st w2 in Q & w3 in Q & w4 in Q & w5 in Q & w6 in Q & LSeg(w1,w2) c=Q & LSeg(w2,w3) c= Q & LSeg(w3,w4) c= Q & LSeg(w4,w5) c= Q & LSeg(w5,w6) c=Q & LSeg(w6,w7) c= Q by A1,A2,Th48; hence thesis by A2,Th40; end; end; hence thesis by JORDAN1:2; end; theorem Th52: for a being Real st n>=1 holds (REAL n) \ {q: |.q.| < a} <> {} proof let a be Real; A1: {q:(|.q.|)>a} c= (REAL n)\{q2:(|.q2.|)a}; then consider q such that A2: q=x and A3: (|.q.|)>a; A4: now assume x in {q2:(|.q2.|)=1; hence thesis by A1,Th50,XBOOLE_1:3; end; theorem Th53: for a being Real,P being Subset of TOP-REAL n st n>=2 & P=(REAL n)\ {q : |.q.| < a } holds P is connected proof let a be Real, P be Subset of TOP-REAL n; assume A1: n>=2 & P=(REAL n)\ {q : |.q.| < a }; then reconsider Q=P as non empty Subset of TOP-REAL n by Th52,XXREAL_0:2; for w1,w7 being Point of TOP-REAL n st w1 in Q & w7 in Q & w1<>w7 ex f being Function of I[01],((TOP-REAL n) | Q) st f is continuous & w1=f.0 & w7=f.1 proof let w1,w7 be Point of TOP-REAL n; assume that A2: w1 in Q & w7 in Q and w1<>w7; per cases; suppose not (ex r being Real st w1=r*w7 or w7=r*w1); then ex w2,w3 being Point of TOP-REAL n st w2 in Q & w3 in Q & LSeg(w1,w2) c=Q & LSeg(w2,w3) c= Q & LSeg(w3,w7) c= Q by A1,A2,Th43; hence thesis by A2,Th39; end; suppose ex r being Real st w1=r*w7 or w7=r*w1; then ex w2,w3,w4,w5,w6 being Point of TOP-REAL n st w2 in Q & w3 in Q & w4 in Q & w5 in Q & w6 in Q & LSeg(w1,w2) c=Q & LSeg(w2,w3) c= Q & LSeg(w3,w4) c= Q & LSeg(w4,w5) c= Q & LSeg(w5,w6) c=Q & LSeg(w6,w7) c= Q by A1,A2,Th49; hence thesis by A2,Th40; end; end; hence thesis by JORDAN1:2; end; theorem Th54: for a being Real,n being Element of NAT, P being Subset of TOP-REAL n st n>=1 & P=(REAL n)\ {q where q is Point of TOP-REAL n: |.q.| < a } holds not P is bounded proof let a be Real,n be Element of NAT,P be Subset of TOP-REAL n; assume that A1: n>=1 and A2: P=(REAL n)\ {q where q is Point of TOP-REAL n : |.q.| < a }; per cases; suppose A3: a>0; now set p = the Element of P; assume P is bounded; then consider r being Real such that A4: for q being Point of TOP-REAL n st q in P holds |.q.|{} by A1,A2,Th52; then p in P; then reconsider p as Point of TOP-REAL n; A6: |.p.|=0 & sqrt 1<=sqrt n by A1,COMPLEX1:46,SQUARE_1:26; then A12: abs(a+r+1)*1<=abs(a+r+1)*sqrt n by SQUARE_1:18,XREAL_1:64; |.(a+r+1)*(1.REAL n).|=abs(a+r+1)*|.(1.REAL n).| by TOPRNS_1:7 .=abs(a+r+1)*(sqrt n) by EUCLID:73; then a+r+1<= |.(a+r+1)*(1.REAL n).| by A12,A10,XXREAL_0:2; hence contradiction by A9,A11,XXREAL_0:2; end; A13: a+r+1<=abs(a+r+1) by ABSVALUE:4; abs(a+r+1)>=0 & sqrt 1<=sqrt n by A1,COMPLEX1:46,SQUARE_1:26; then A14: abs(a+r+1)*1<=abs(a+r+1)*sqrt n by SQUARE_1:18,XREAL_1:64; A15: a+r{}; then d in {q where q is Point of TOP-REAL n: (|.q.|) < a }; then ex q being Point of TOP-REAL n st q=d & (|.q.|) < a; hence contradiction by A17; end; then P=[#](TOP-REAL n) by A2,EUCLID:22; hence thesis by A1,Th35; end; end; theorem Th55: for a being Real,P being Subset of TOP-REAL 1 st P={q where q is Point of TOP-REAL 1: ex r st q=<*r*> & r > a } holds P is convex proof let a be Real,P be Subset of TOP-REAL 1; assume A1: P={q where q is Point of TOP-REAL 1: ex r st q=<*r*> & r > a }; for w1,w2 being Point of TOP-REAL 1 st w1 in P & w2 in P holds LSeg(w1, w2) c= P proof let w1,w2 be Point of TOP-REAL 1; assume that A2: w1 in P and A3: w2 in P; consider q2 being Point of TOP-REAL 1 such that A4: q2=w2 and A5: ex r st q2=<*r*> & r > a by A1,A3; consider q1 being Point of TOP-REAL 1 such that A6: q1=w1 and A7: ex r st q1=<*r*> & r > a by A1,A2; consider r2 such that A8: q2=<*r2*> and A9: r2 > a by A5; consider r1 such that A10: q1=<*r1*> and A11: r1 > a by A7; thus LSeg(w1,w2) c= P proof let x be set; assume x in LSeg(w1,w2); then consider r3 being Real such that A12: x=(1-r3)*w1+r3*w2 and A13: 0<=r3 and A14: r3<=1; A15: 1-r3>=0 by A14,XREAL_1:48; per cases; suppose A16: r3>0; A17: (1-r3)*r1>=(1-r3)*a & (1-r3)*a+r3*a=a by A11,A15,XREAL_1:64; r3*r2>r3*a by A9,A16,XREAL_1:68; then A18: (1-r3)*r1+r3*r2>a by A17,XREAL_1:8; <*(1-r3)*r1+r3*r2*>=|[(1-r3)*r1]|+|[r3*r2]| by JORDAN2B:22 .=(1-r3)*|[r1]|+|[r3*r2]| by JORDAN2B:21 .=(1-r3)*|[r1]|+r3*|[r2]| by JORDAN2B:21; hence thesis by A1,A6,A10,A4,A8,A12,A18; end; suppose r3<=0; then r3=0 by A13; then x=w1+0 *w2 by A12,EUCLID:29 .=w1+0.TOP-REAL 1 by EUCLID:29 .=w1 by EUCLID:27; hence thesis by A2; end; end; end; hence thesis by JORDAN1:def 1; end; theorem Th56: for a being Real,P being Subset of TOP-REAL 1 st P={q where q is Point of TOP-REAL 1 : ex r st q=<*r*> & r < -a } holds P is convex proof let a be Real,P be Subset of TOP-REAL 1; assume A1: P={q where q is Point of TOP-REAL 1 : ex r st q=<*r*> & r < -a }; for w1,w2 being Point of TOP-REAL 1 st w1 in P & w2 in P holds LSeg(w1, w2) c= P proof let w1,w2 be Point of TOP-REAL 1; assume that A2: w1 in P and A3: w2 in P; consider q2 being Point of TOP-REAL 1 such that A4: q2=w2 and A5: ex r st q2=<*r*> & r < -a by A1,A3; consider q1 being Point of TOP-REAL 1 such that A6: q1=w1 and A7: ex r st q1=<*r*> & r < -a by A1,A2; consider r2 such that A8: q2=<*r2*> and A9: r2 < -a by A5; consider r1 such that A10: q1=<*r1*> and A11: r1 < -a by A7; thus LSeg(w1,w2) c= P proof let x be set; assume x in LSeg(w1,w2); then consider r3 being Real such that A12: x=(1-r3)*w1+r3*w2 and A13: 0<=r3 and A14: r3<=1; A15: 1-r3>=0 by A14,XREAL_1:48; per cases; suppose A16: r3>0; A17: (1-r3)*r1<=(1-r3)*(-a) & (1-r3)*(-a)+r3*(-a)=-a by A11,A15,XREAL_1:64; r3*r2=|[(1-r3)*r1]|+|[r3*r2]| by JORDAN2B:22 .=(1-r3)*|[r1]|+|[r3*r2]| by JORDAN2B:21 .=(1-r3)*|[r1]|+r3*|[r2]| by JORDAN2B:21; hence thesis by A1,A6,A10,A4,A8,A12,A18; end; suppose r3<=0; then r3=0 by A13; then x=w1+0 *w2 by A12,EUCLID:29 .=w1+0.TOP-REAL 1 by EUCLID:29 .=w1 by EUCLID:27; hence thesis by A2; end; end; end; hence thesis by JORDAN1:def 1; end; canceled 2; theorem Th59: for W being Subset of Euclid 1,a being Real st W={q where q is Point of TOP-REAL 1 : ex r st q=<*r*> & r > a } holds W is not bounded proof let W be Subset of Euclid 1,a be Real; assume A1: W={q where q is Point of TOP-REAL 1 : ex r st q=<*r*> & r > a }; abs(a)>=0 by COMPLEX1:46; then A2: abs(a)+abs(a)+abs(a)>=0+abs(a) by XREAL_1:6; assume W is bounded; then consider r such that A3: 0 by FINSEQ_2:59 .=<*((r+abs(a))*1)*> by RVSUM_1:47; reconsider z2=(r+abs(a))*(1.REAL 1) as Point of Euclid 1 by FINSEQ_2:131; a<=abs(a) & 0+abs(a) by FINSEQ_2:59 .=<*((3*(r+abs(a)))*1)*> by RVSUM_1:47; reconsider z1=(3*(r+abs(a)))*(1.REAL 1) as Point of Euclid 1 by FINSEQ_2:131; dist(z1,z2)=|.(3*(r+abs(a)))*(1.REAL 1)-((r+abs(a))*(1.REAL 1)).| by JGRAPH_1:28 .=|.((r+abs(a))+(r+abs(a))+(r+abs(a))-(r+abs(a)))*(1.REAL 1).| by EUCLID:50 .=abs((r+abs(a))+(r+abs(a)))*|.(1.REAL 1).| by TOPRNS_1:7 .=abs((r+abs(a))+(r+abs(a)))*(sqrt 1) by EUCLID:73; then A8: (r+abs(a))+(r+abs(a))<= dist(z1,z2) by ABSVALUE:4,SQUARE_1:18; A9: 0<=abs(a) by COMPLEX1:46; then (r+abs(a))+0<(r+abs(a))+(r+abs(a)) by A3,XREAL_1:6; then A10: (r+abs(a))0 by A3,XREAL_1:129; then a<=abs(a) & 0+abs(a)<3*r+3*abs(a) by A2,ABSVALUE:4,XREAL_1:8; then a<3*(r+abs(a)) by XXREAL_0:2; then (3*(r+abs(a)))*(1.REAL 1) in W by A1,A7; hence contradiction by A4,A6,A11; end; theorem Th60: for W being Subset of Euclid 1,a being Real st W={q where q is Point of TOP-REAL 1 : ex r st q=<*r*> & r < -a } holds W is not bounded proof let W be Subset of Euclid 1,a be Real; abs(a)>=0 by COMPLEX1:46; then A1: abs(a)+abs(a)+abs(a)>=0+abs(a) by XREAL_1:6; assume A2: W={q where q is Point of TOP-REAL 1 : ex r st q=<*r*> & r < -a }; assume W is bounded; then consider r such that A3: 0 by FINSEQ_2:59 .=<*((-3*(r+abs(a)))*1)*> by RVSUM_1:47; reconsider z1=(-3*(r+abs(a)))*(1.REAL 1) as Point of Euclid 1 by FINSEQ_2:131; 3*r>0 by A3,XREAL_1:129; then a<=abs(a) & 0+abs(a)<3*r+3*abs(a) by A1,ABSVALUE:4,XREAL_1:8; then a<3*(r+abs(a)) by XXREAL_0:2; then -a> -(3*(r+abs(a))) by XREAL_1:24; then A6: (-3*(r+abs(a)))*(1.REAL 1) in {q where q is Point of TOP-REAL 1: ex r st q=<*r*> & r< -a } by A5; A7: (-(r+abs(a)))*(1.REAL 1) = (-(r+abs(a)))*<* 1 qua Real *> by FINSEQ_2:59 .=<* (-(r+abs(a)))*1 *> by RVSUM_1:47; reconsider z2=(-(r+abs(a)))*(1.REAL 1) as Point of Euclid 1 by FINSEQ_2:131; dist(z1,z2)=|.(-3*(r+abs(a)))*(1.REAL 1)-(-(r+abs(a)))*(1.REAL 1).| by JGRAPH_1:28 .=|.(-3*(r+abs(a))--(r+abs(a)))*(1.REAL 1).| by EUCLID:50 .=|.-((-3*(r+abs(a))--(r+abs(a)))*(1.REAL 1)).| by TOPRNS_1:26 .=|.(-(-3*(r+abs(a))+--(r+abs(a))))*(1.REAL 1).| by EUCLID:40 .=abs((r+abs(a))+(r+abs(a)))*|.(1.REAL 1).| by TOPRNS_1:7 .=abs((r+abs(a))+(r+abs(a)))*(sqrt 1) by EUCLID:73; then A8: (r+abs(a))+(r+abs(a))<= dist(z1,z2) by ABSVALUE:4,SQUARE_1:18; A9: 0<=abs(a) by COMPLEX1:46; then (r+abs(a))+0<(r+abs(a))+(r+abs(a)) by A3,XREAL_1:6; then A10: (r+abs(a)) -(r+abs(a)) by XREAL_1:24; then (-(r+abs(a)))*(1.REAL 1) in W by A2,A7; hence contradiction by A2,A4,A6,A11; end; theorem Th61: for W being Subset of Euclid n,a being Real st n>=2 & W={q : |.q.| > a } holds W is not bounded proof let W be Subset of Euclid n,a be Real; assume A1: n>=2 & W={q : |.q.| > a }; A2: 1<=n by A1,XXREAL_0:2; then A3: 1<=sqrt n by SQUARE_1:18,26; assume W is bounded; then consider r such that A4: 0=0 & 1<=sqrt n by A2,COMPLEX1:46,SQUARE_1:18,26; then A7: abs(r+abs a)*1<=abs(r+abs a)*sqrt n by XREAL_1:64; a<=abs(a) & abs(a)=0 by COMPLEX1:46; then A11: abs(r+abs(a))*1<=abs(r+abs(a))*sqrt n by A3,XREAL_1:64; |.(r+abs(a))*(1.REAL n).|=abs(r+abs(a))*|.(1.REAL n).| by TOPRNS_1:7 .=abs(r+abs(a))*(sqrt n) by EUCLID:73; then (r+abs(a))<= |.(r+abs(a))*(1.REAL n).| by A11,A10,XXREAL_0:2; then a<|.(r+abs(a))*(1.REAL n).| by A8,XXREAL_0:2; then A12: (r+abs(a))*(1.REAL n) in W by A1; then reconsider z1=(r+abs(a))*(1.REAL n) as Point of Euclid n; A13: (r+abs(a))+(r+abs(a))<=abs((r+abs(a))+(r+abs(a))) by ABSVALUE:4; abs((r+abs(a))+(r+abs(a)))>=0 by COMPLEX1:46; then A14: abs((r+abs(a))+(r+abs(a)))*1<=abs((r+abs(a))+(r+abs(a)))*sqrt n by A3, XREAL_1:64; A15: 0<=abs(a) by COMPLEX1:46; then A16: r+0<=r+abs(a) by XREAL_1:6; A17: (r+abs(a))+0<(r+abs(a))+(r+abs(a)) by A4,A15,XREAL_1:6; dist(z1,z2)=|.(r+abs(a))*(1.REAL n)--((r+abs(a))*(1.REAL n)).| by JGRAPH_1:28 .=|.(r+abs(a))*(1.REAL n)+((r+abs(a))*(1.REAL n)).| .=|.((r+abs(a))+(r+abs(a)))*(1.REAL n).| by EUCLID:33 .=abs(((r+abs(a))+(r+abs(a))))*|.(1.REAL n).| by TOPRNS_1:7 .=abs((r+abs(a))+(r+abs(a)))*(sqrt n) by EUCLID:73; then (r+abs(a))+(r+abs(a))<= dist(z1,z2) by A14,A13,XXREAL_0:2; then (r+abs(a))=2 & W=(REAL n)\ {q : (|.q.|) < a } holds W is not bounded proof let W be Subset of Euclid n,a be Real; reconsider 1R = 1.REAL n as Point of TOP-REAL n; assume A1: n>=2 & W=(REAL n)\ {q : (|.q.|) < a }; assume W is bounded; then consider r such that A2: 0=1 by A1,XXREAL_0:2; then A6: 1<=sqrt n by SQUARE_1:18,26; A7: now a<=abs(a) & abs(a)=0 by COMPLEX1:46; then A10: abs(r+abs a)*1<=abs(r+abs a)*sqrt n by A6,XREAL_1:64; A11: (r+abs(a))<=abs(r+abs a) by ABSVALUE:4; |.-((r+abs(a))*(1.REAL n)).| = |.((r+abs(a))*(1.REAL n)).| by TOPRNS_1:26 .=abs(r+abs a)*|.(1.REAL n).| by TOPRNS_1:7 .=abs(r+abs a)*(sqrt n) by EUCLID:73; then (r+abs(a))<= |.-((r+abs(a))*(1.REAL n)).| by A10,A11,XXREAL_0:2; hence contradiction by A9,A8,XXREAL_0:2; end; A12: now a<=abs(a) & abs(a)=0 by COMPLEX1:46; then A15: abs(r+abs a)*1<=abs(r+abs a)*sqrt n by A6,XREAL_1:64; A16: (r+abs(a))<=abs(r+abs a) by ABSVALUE:4; |.(r+abs(a))*(1.REAL n).|=abs(r+abs a)*|.(1.REAL n).| by TOPRNS_1:7 .=abs(r+abs a)*(sqrt n) by EUCLID:73; then (r+abs(a))<= |.(r+abs(a))*(1.REAL n).| by A15,A16,XXREAL_0:2; hence contradiction by A14,A13,XXREAL_0:2; end; reconsider z2=-((r+abs(a))*(1.REAL n)) as Point of Euclid n by EUCLID:22; reconsider z1=(r+abs(a))*(1.REAL n) as Point of Euclid n by EUCLID:22; A17: (r+abs(a))+(r+abs(a))<=abs((r+abs(a))+(r+abs(a))) by ABSVALUE:4; abs(((r+abs(a))+(r+abs(a))))>=0 by COMPLEX1:46; then A18: abs((r+abs(a))+(r+abs(a)))*1<=abs((r+abs(a))+(r+abs(a)))*sqrt n by A6, XREAL_1:64; dist(z1,z2)=|.(r+abs(a))*(1.REAL n)--((r+abs(a))*(1.REAL n)).| by JGRAPH_1:28 .=|.(r+abs a)*1R + --((r+abs a)*1R).| .=|.(r+abs a)*1R+((r+abs a)*1R).| .=|.((r+abs(a))+(r+abs(a)))*1R .| by EUCLID:33 .=|.((r+abs(a))+(r+abs(a)))*(1.REAL n).| .=abs(((r+abs(a))+(r+abs(a))))*|.(1.REAL n).| by TOPRNS_1:7 .=abs(((r+abs(a))+(r+abs(a))))*(sqrt n) by EUCLID:73; then (r+abs(a))+(r+abs(a))<= dist(z1,z2) by A18,A17,XXREAL_0:2; then A19: (r+abs(a)) {}Euclid n by A3; A11: W /\ Q = {} by A5,XBOOLE_0:def 7; now assume Q`={}; then Q=({}(the carrier of TOP-REAL n))`; hence contradiction by A1,A10,A11,XBOOLE_1:28; end; then reconsider Q1=Q` as non empty Subset of TOP-REAL n; (TOP-REAL n) | Q1 is non empty; then Component_of P0 is a_component by A1,A10,A8,CONNSP_3:9; hence thesis by A4,A7,A9,Th14; end; theorem Th64: for A being Subset of Euclid n, B being non empty Subset of Euclid n, C being Subset of (Euclid n) | B st A=C & C is bounded holds A is bounded proof let A be Subset of Euclid n, B be non empty Subset of Euclid n, C be Subset of (Euclid n) | B; assume that A1: A=C and A2: C is bounded; consider r0 being Real such that A3: 0{}; then reconsider A1=A as non empty Subset of Euclid n by TOPREAL3:8; [#]((TOP-REAL n) | A)=A2 by PRE_TOPC:def 5; then [#]((TOP-REAL n) | A) is compact by A1,COMPTS_1:2; then A2: (TOP-REAL n) | A is compact by COMPTS_1:1; TopSpaceMetr((Euclid n) | A1)=(TOP-REAL n) | A by EUCLID:63; then (Euclid n) | A1 is totally_bounded by A2,TBSP_1:9; then A3: (Euclid n) | A1 is bounded by TBSP_1:19; [#]((Euclid n) | A1) =A1 by TOPMETR:def 2; then A1 is bounded by A3,Th64; hence thesis by Th11; end; suppose A={}; hence thesis; end; end; registration let n be Element of NAT; cluster compact -> bounded for Subset of TOP-REAL n; coherence by Th65; end; theorem Th66: for A being Subset of TOP-REAL n st 1<=n & A is bounded holds A` <> {} proof let A be Subset of TOP-REAL n; assume that A1: 1<=n and A2: A is bounded; consider r being Real such that A3: for q being Point of TOP-REAL n st q in A holds |.q.|=0 by COMPLEX1:46; then A4: abs(r)*|.1.REAL n.|>=abs(r)*1 by A1,EUCLID:75,XREAL_1:64; |.r*(1.REAL n).|=abs(r)*|.1.REAL n.| & r<=abs(r) by ABSVALUE:4,TOPRNS_1:7; then not r*(1.REAL n) in A by A3,A4,XXREAL_0:2; hence thesis by XBOOLE_0:def 5; end; theorem Th67: for r being Real holds (ex B being Subset of Euclid n st B={q : (|.q.|) < r }) & for A being Subset of Euclid n st A={q1 : (|.q1.|) < r } holds A is bounded proof let r be Real; A1: {q : (|.q.|) < r } c= the carrier of Euclid n proof let x be set; assume x in {q : (|.q.|) < r }; then ex q being Point of TOP-REAL n st q=x & (|.q.|) < r; then x in the carrier of TOP-REAL n; hence thesis by TOPREAL3:8; end; hence ex B being Subset of Euclid n st B={q : (|.q.|) < r }; reconsider C={q1 : (|.q1.|) < r } as Subset of TOP-REAL n by A1,TOPREAL3:8; let A be Subset of Euclid n; for q being Point of TOP-REAL n st q in C holds |.q.|=2 & A is bounded holds UBD A is_outside_component_of A proof let A be Subset of TOP-REAL n; assume that A1: n>=2 and A2: A is bounded; reconsider C=A as bounded Subset of Euclid n by A2,Th11; per cases; suppose A3: C<>{}; set x0 = the Element of C; A4: x0 in C by A3; then reconsider q1=x0 as Point of TOP-REAL n; reconsider o=0.TOP-REAL n as Point of Euclid n by EUCLID:67; reconsider x0 as Point of Euclid n by A4; consider r being Real such that 0= r+dist(o,x0)+1 by A9; then dist(o,z)>=r+dist(o,x0)+1 by A11,RLVECT_1:13; then r+(dist(o,x0)+1)<=r+dist(o,x0) by A10,XXREAL_0:2; then dist(o,x0)+1<=dist(o,x0)+0 by XREAL_1:6; hence contradiction by XREAL_1:6; end; reconsider P=W as Subset of TOP-REAL n by TOPREAL3:8; reconsider P as Subset of TOP-REAL n; 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; A12: P is connected by A1,Th53; A13: UBD A c= P1 proof A14: (TOP-REAL n) |P is connected by A12,CONNSP_1:def 3; A15: P c= A` by A6,SUBSET_1:23; then Down(P,A`)=P by XBOOLE_1:28; then ((TOP-REAL n) | A`) | Down(P,A`) is connected by A15,A14,PRE_TOPC:7; then A16: Down(P,A`) is connected by CONNSP_1:def 3; reconsider G=A` as non empty Subset of TOP-REAL n by A1,A2,Th66, XXREAL_0:2; let z be set; A17: (TOP-REAL n) | G is non empty TopSpace; assume z in UBD A; then consider y being set such that A18: z in y and A19: y in {B where B is Subset of TOP-REAL n: B is_outside_component_of A} by TARSKI:def 4; consider B being Subset of TOP-REAL n such that A20: y=B and A21: B is_outside_component_of A by A19; consider C2 being Subset of ((TOP-REAL n) | (A`)) such that A22: C2=B and A23: C2 is a_component and A24: C2 is not bounded Subset of Euclid n by A21,Th14; consider D2 being Subset of Euclid n such that A25: D2={q : |.q.| < R0 } by Th67; reconsider D2 as Subset of Euclid n; A26: A c= D2 proof let z be set; A27: |.q1.|=|.q1-0.TOP-REAL n.| by RLVECT_1:13 .=dist(x0,o) by JGRAPH_1:28; assume A28: z in A; then reconsider q2=z as Point of TOP-REAL n; reconsider x1=q2 as Point of Euclid n by TOPREAL3:8; |.q2-q1.|=dist(x1,x0) & dist(x1,x0)<=r by A5,A28,JGRAPH_1:28; then A29: |.q2-q1.|+|.q1.|<=r+dist(o,x0) by A27,XREAL_1:6; A30: r+dist(o,x0){} by A25,A31,XBOOLE_1:3,26; then A35: Down(P,A`) meets C2 by XBOOLE_0:def 7; C2 is connected by A23,CONNSP_1:def 5; then C2 c= Component_of (Down(P,A`)) by A16,A35,A17,CONNSP_3:16; hence thesis by A18,A20,A22; end; W is not bounded by A1,Th62; then P1 is_outside_component_of A & P1 c= UBD A by A12,A6,Th23,Th63; hence thesis by A13,XBOOLE_0:def 10; end; suppose A36: C={}; REAL n c= the carrier of Euclid n; then reconsider W=REAL n as Subset of Euclid n; W /\ A={} by A36; then A37: W misses A by XBOOLE_0:def 7; reconsider P=W as Subset of TOP-REAL n by TOPREAL3:8; reconsider P as Subset of TOP-REAL n; 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; [#](TOP-REAL n) is a_component; then A38: [#](the TopStruct of TOP-REAL n) is a_component by CONNSP_1:45; W is not bounded by A1,Th33,XXREAL_0:2; then A39: P1 is_outside_component_of A by A37,Th28,Th63; A={}(TOP-REAL n) by A36; then A40: UBD A=REAL n by A1,Th36,XXREAL_0:2; [#](TOP-REAL n)=REAL n & (TOP-REAL n) | [#](TOP-REAL n)=the TopStruct of TOP-REAL n by EUCLID:22,TSEP_1:93; hence UBD A is_outside_component_of A by A36,A39,A40,A38,CONNSP_3:7; end; end; theorem Th69: for a being Real, P being Subset of TOP-REAL n st P={q : (|.q.|) < a } holds P is convex proof let a be Real, P be Subset of TOP-REAL n; assume A1: P={q : (|.q.|) < a }; for p1,p2 being Point of TOP-REAL n st p1 in P & p2 in P holds LSeg(p1, p2) c= P proof let p1,p2 be Point of TOP-REAL n; assume that A2: p1 in P and A3: p2 in P; A4: ex q2 st q2=p2 & (|.q2.|) < a by A1,A3; A5: ex q1 st q1=p1 & (|.q1.|) < a by A1,A2; LSeg(p1,p2) c= P proof let x; assume A6: x in LSeg(p1,p2); then consider r such that A7: x=(1-r)*p1+r*p2 and A8: 0<=r and A9: r<=1; A10: |.(1-r)*p1.|=abs(1-r)*|.p1.| by TOPRNS_1:7; reconsider q=x as Point of TOP-REAL n by A6; A11: |.(1-r)*p1+r*p2.|<=|.(1-r)*p1.|+|.r*p2.| by TOPRNS_1:29; A12: 1-r>=0 by A9,XREAL_1:48; then A13: abs(1-r)=1-r by ABSVALUE:def 1; per cases; suppose A14: 1-r>0; A15: |.r*p2.|=abs(r)*|.p2.| & r=abs(r) by A8,ABSVALUE:def 1,TOPRNS_1:7; 0<=abs(r) by COMPLEX1:46; then A16: abs(r)*|.p2.|<=abs(r)*a by A4,XREAL_1:64; abs(1-r)*|.p1.|=0 by A11,XREAL_1:48; then A15: abs(1-r)=1-r by ABSVALUE:def 1; per cases; suppose A16: 1-r>0; A17: |.r*(p-p2).|=abs(r)*|.p-p2.| & r=abs(r) by A10,ABSVALUE:def 1 ,TOPRNS_1:7; 0<=abs(r) by COMPLEX1:46; then A18: abs(r)*|.p-p2.|<=abs(r)*a by A5,XREAL_1:64; abs(1-r)*|.p-p1.| q & p in Ball(u,r) & q in Ball(u,r) implies ex h being Function of I[01],TOP-REAL n st h is continuous & h.0=p & h.1=q & rng h c= Ball (u,r) proof assume that A1: p<>q and A2: p in Ball(u,r) & q in Ball(u,r); reconsider Q=Ball(u,r) as Subset of TOP-REAL n by TOPREAL3:8; Q is convex by Th70; then A3: LSeg(p,q) c= Ball(u,r) by A2,JORDAN1:def 1; reconsider P=LSeg(p,q) as Subset of TOP-REAL n; LSeg(p,q) is_an_arc_of p,q by A1,TOPREAL1:9; then consider f being Function of I[01], (TOP-REAL n) |P such that A4: f is being_homeomorphism and A5: f.0 = p & f.1 = q by TOPREAL1:def 1; reconsider h=f as Function of I[01],TOP-REAL n by JORDAN6:3; take h; rng f = [#]((TOP-REAL n) |P) & f is continuous by A4,TOPS_2:def 5; hence thesis by A3,A5,JORDAN6:3,PRE_TOPC:def 5; end; theorem Th73: for f being Function of I[01],TOP-REAL n st f is continuous & f. 0=p1 & f.1=p2 & p in Ball(u,r) & p2 in Ball(u,r) ex h being Function of I[01], TOP-REAL n st h is continuous & h.0=p1 & h.1=p & rng h c= rng f \/ Ball(u,r) proof let f be Function of I[01],TOP-REAL n; assume that A1: f is continuous & f.0=p1 & f.1=p2 and A2: p in Ball(u,r) & p2 in Ball(u,r); per cases; suppose p2<>p; then LSeg(p2,p) is_an_arc_of p2,p by TOPREAL1:9; then consider f1 being Function of I[01], (TOP-REAL n) | LSeg(p2,p) such that A3: f1 is being_homeomorphism and A4: f1.0 = p2 & f1.1 = p by TOPREAL1:def 1; reconsider f2=f1 as Function of I[01],TOP-REAL n by JORDAN6:3; rng f1 = [#]((TOP-REAL n) | LSeg(p2,p)) by A3,TOPS_2:def 5; then rng f2=LSeg(p2,p) by PRE_TOPC:def 5; then A5: rng f \/ rng f2 c= rng f \/ Ball(u,r) by A2,TOPREAL3:21,XBOOLE_1:9; f1 is continuous by A3,TOPS_2:def 5; then f2 is continuous by JORDAN6:3; then ex h3 being Function of I[01],(TOP-REAL n) st h3 is continuous & p1=h3 .0 & p=h3.1 & rng h3 c= rng f \/ rng f2 by A1,A4,BORSUK_2:13; hence thesis by A5,XBOOLE_1:1; end; suppose p2=p; hence thesis by A1,XBOOLE_1:7; end; end; theorem Th74: for f being Function of I[01],TOP-REAL n st f is continuous & rng f c=P & f.0=p1 & f.1=p2 & p in Ball(u,r) & p2 in Ball(u,r) & Ball(u,r) c= P ex f1 being Function of I[01],TOP-REAL n st f1 is continuous & rng f1 c= P & f1 .0=p1 & f1.1=p proof let f be Function of I[01],TOP-REAL n; assume f is continuous & rng f c= P & f.0=p1 & f.1=p2 & p in Ball(u,r) & p2 in Ball(u,r) & Ball(u,r) c= P; then (ex f3 being Function of I[01],TOP-REAL n st f3 is continuous & f3.0=p1 & f3.1=p & rng f3 c= rng f \/ Ball(u,r) )& rng f \/ Ball(u,r) c= P by Th73, XBOOLE_1:8; hence thesis by XBOOLE_1:1; end; theorem Th75: for p for P being Subset of TOP-REAL n st R is connected & R is open & P = {q: q<>p & q in R & not ex f being Function of I[01],TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q} holds P is open proof let p; let P be Subset of TOP-REAL n; assume that A1: R is connected & R is open and A2: P = {q: q<>p & q in R & not ex f being Function of I[01],TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q}; A3: the TopStruct of TOP-REAL n = TopSpaceMetr(Euclid n) by EUCLID:def 8; then reconsider P9=P as Subset of TopSpaceMetr(Euclid n); A4: P c= R proof let x; assume x in P; then ex q st q=x & q<>p & q in R & not ex f being Function of I[01],TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q by A2; hence thesis; end; now A5: the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8; then reconsider R9=R as Subset of TopSpaceMetr(Euclid n); let u; reconsider p2=u as Point of TOP-REAL n by TOPREAL3:8; assume A6: u in P; R9 is open by A1,A5,PRE_TOPC:30; then consider r be real number such that A7: r>0 and A8: Ball(u,r) c= R9 by A4,A6,TOPMETR:15; take r; thus r>0 by A7; reconsider r9=r as Real by XREAL_0:def 1; A9: p2 in Ball(u,r9) by A7,TBSP_1:11; Ball(u,r) c= P9 proof assume not thesis; then consider x such that A10: x in Ball(u,r) and A11: not x in P by TARSKI:def 3; x in R by A8,A10; then reconsider q=x as Point of TOP-REAL n; per cases by A2,A8,A10,A11; suppose A12: q=p; A13: now assume A14: q=p2; ex p3 st p3=p2 & p3<>p & p3 in R & not ex f1 being Function of I[01],TOP-REAL n st f1 is continuous & rng f1 c= R & f1.0=p & f1.1=p3 by A2,A6; hence contradiction by A12,A14; end; u in Ball(u,r9) by A7,TBSP_1:11; then A15: ex f2 being Function of I[01],TOP-REAL n st f2 is continuous & f2. 0=q & f2.1=p2 & rng f2 c= Ball(u,r9) by A10,A13,Th72; not p2 in P proof assume p2 in P; then ex q4 st q4=p2 & q4<>p & q4 in R & not ex f1 being Function of I[01],TOP-REAL n st f1 is continuous & rng f1 c= R & f1.0=p & f1.1=q4 by A2; hence contradiction by A8,A12,A15,XBOOLE_1:1; end; hence contradiction by A6; end; suppose A16: ex f1 being Function of I[01],TOP-REAL n st f1 is continuous & rng f1 c= R & f1.0=p & f1.1=q; not p2 in P proof assume p2 in P; then ex q4 st q4=p2 & q4<>p & q4 in R & not ex f1 being Function of I[01],TOP-REAL n st f1 is continuous & rng f1 c= R & f1.0=p & f1.1=q4 by A2; hence contradiction by A8,A9,A10,A16,Th74; end; hence contradiction by A6; end; end; hence Ball(u,r) c= P9; end; then P9 is open by TOPMETR:15; hence thesis by A3,PRE_TOPC:30; end; theorem Th76: for P being Subset of TOP-REAL n st R is connected & R is open & p in R & P = {q: q=p or ex f being Function of I[01],TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q} holds P is open proof let P be Subset of TOP-REAL n; assume that A1: R is connected & R is open and A2: p in R and A3: P = {q: q=p or ex f being Function of I[01],TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q}; A4: the TopStruct of TOP-REAL n = TopSpaceMetr(Euclid n) by EUCLID:def 8; then reconsider P9=P as Subset of TopSpaceMetr(Euclid n); reconsider RR=R as Subset of TopSpaceMetr(Euclid n) by A4; now let u; reconsider p2=u as Point of TOP-REAL n by TOPREAL3:8; assume u in P9; then consider q1 such that A5: q1=u and A6: q1=p or ex f being Function of I[01],TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q1 by A3; A7: now per cases by A6; suppose q1=p; hence p2 in R by A2,A5; end; suppose q1<>p & ex f being Function of I[01],TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q1; then consider f2 being Function of I[01],TOP-REAL n such that f2 is continuous and A8: rng f2 c= R and f2.0=p and A9: f2.1=q1; dom f2=[.0 qua Real,1 qua Real.] by BORSUK_1:40,FUNCT_2:def 1; then 1 in dom f2 by XXREAL_1:1; then u in rng f2 by A5,A9,FUNCT_1:def 3; hence p2 in R by A8; end; end; RR is open by A1,A4,PRE_TOPC:30; then consider r be real number such that A10: r>0 and A11: Ball(u,r) c= R by A7,TOPMETR:15; take r; thus r>0 by A10; reconsider r9=r as Real by XREAL_0:def 1; A12: p2 in Ball(u,r9) by A10,TBSP_1:11; thus Ball(u,r) c= P proof let x; assume A13: x in Ball(u,r); then reconsider q=x as Point of TOP-REAL n by A11,TARSKI:def 3; per cases; suppose q=p; hence thesis by A3; end; suppose A14: q<>p; A15: now assume q1=p; then p in Ball(u,r9) by A5,A10,TBSP_1:11; then consider f2 being Function of I[01],TOP-REAL n such that A16: f2 is continuous & f2.0=p & f2.1=q and A17: rng f2 c= Ball(u,r9) by A13,A14,Th72; rng f2 c= R by A11,A17,XBOOLE_1:1; hence thesis by A3,A16; end; now assume q1<>p; then ex f being Function of I[01],TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q by A5,A6,A11,A12,A13,Th74; hence thesis by A3; end; hence thesis by A15; end; end; end; then P9 is open by TOPMETR:15; hence thesis by A4,PRE_TOPC:30; end; theorem Th77: for R being Subset of TOP-REAL n holds p in R & P={q: q=p or ex f being Function of I[01],TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q} implies P c= R proof let R be Subset of TOP-REAL n; assume that A1: p in R and A2: P = {q: q=p or ex f being Function of I[01],TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q}; let x; assume x in P; then consider q such that A3: q=x and A4: q=p or ex f being Function of I[01],TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q by A2; per cases by A4; suppose q=p; hence thesis by A1,A3; end; suppose ex f being Function of I[01],TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q; then consider f1 being Function of I[01],TOP-REAL n such that f1 is continuous and A5: rng f1 c= R and f1.0=p and A6: f1.1=q; reconsider P1=rng f1 as Subset of TOP-REAL n; dom f1=[.0 qua Real,1 qua Real.] by BORSUK_1:40,FUNCT_2:def 1; then 1 in dom f1 by XXREAL_1:1; then q in P1 by A6,FUNCT_1:def 3; hence thesis by A3,A5; end; end; theorem Th78: for R being Subset of TOP-REAL n, p being Point of TOP-REAL n st R is connected & R is open & p in R & P={q: q=p or ex f being Function of I[01] ,TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q} holds R c= P proof let R be Subset of TOP-REAL n, p be Point of TOP-REAL n; assume that A1: R is connected & R is open and A2: p in R and A3: P = {q: q=p or ex f being Function of I[01],TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q}; reconsider R9 = R as non empty Subset of TOP-REAL n by A2; A4: p in P by A3; set P2 = R \ P; reconsider P22=P2 as Subset of TOP-REAL n; A5: [#]((TOP-REAL n) | R) = R by PRE_TOPC:def 5; then reconsider P11 = P, P12 = P22 as Subset of (TOP-REAL n) | R by A2,A3 ,Th77,XBOOLE_1:36; reconsider P11, P12 as Subset of (TOP-REAL n) | R; P \/ (R \ P) = P \/ R by XBOOLE_1:39; then A6: P11 misses P12 & [#]((TOP-REAL n) | R) = P11 \/ P12 by A5,XBOOLE_1:12,79; now let x; A7: now assume A8: x in P2; then reconsider q2=x as Point of TOP-REAL n; not x in P by A8,XBOOLE_0:def 5; then A9: q2<>p & not ex f being Function of I[01],TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q2 by A3; q2 in R by A8,XBOOLE_0:def 5; hence x in {q: q<>p & q in R & not ex f being Function of I[01],TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q} by A9; end; now assume x in {q: q<>p & q in R & not ex f being Function of I[01], TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q}; then A10: ex q3 st q3=x & q3<>p & q3 in R & not ex f being Function of I[01], TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q3; then not ex q st q=x & (q=p or ex f being Function of I[01],TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q); then not x in P by A3; hence x in P2 by A10,XBOOLE_0:def 5; end; hence x in P2 iff x in {q: q<>p & q in R & not ex f being Function of I[01] ,TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q} by A7; end; then P2={q: q<>p & q in R & not ex f being Function of I[01],TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q} by TARSKI:1; then P22 is open by A1,Th75; then A11: P22 in the topology of TOP-REAL n by PRE_TOPC:def 2; reconsider PPP=P as Subset of TOP-REAL n; PPP is open by A1,A2,A3,Th76; then A12: P in the topology of TOP-REAL n by PRE_TOPC:def 2; P11 = P /\ [#]((TOP-REAL n) | R) by XBOOLE_1:28; then P11 in the topology of (TOP-REAL n) | R by A12,PRE_TOPC:def 4; then A13: P11 is open by PRE_TOPC:def 2; P12 = P22 /\ [#]((TOP-REAL n) | R) by XBOOLE_1:28; then P12 in the topology of ( TOP-REAL n) | R by A11,PRE_TOPC:def 4; then A14: P12 is open by PRE_TOPC:def 2; (TOP-REAL n) | R9 is connected by A1,CONNSP_1:def 3; then P11 = {}((TOP-REAL n) | R) or P12 = {}((TOP-REAL n) | R) by A6,A13,A14, CONNSP_1:11; hence thesis by A4,XBOOLE_1:37; end; theorem Th79: for R being Subset of TOP-REAL n, p,q being Point of TOP-REAL n st R is connected & R is open & p in R & q in R & p<>q holds ex f being Function of I[01],TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q proof let R be Subset of TOP-REAL n, p,q be Point of TOP-REAL n; assume that A1: R is connected & R is open & p in R and A2: q in R and A3: p<>q; set RR={q2: q2=p or ex f being Function of I[01],TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q2}; RR c= the carrier of TOP-REAL n proof let x; assume x in RR; then ex q2 st q2=x & (q2=p or ex f being Function of I[01],TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q2); hence thesis; end; then R c= RR by A1,Th78; then q in RR by A2; then ex q2 st q=q2 &(q2=p or ex f being Function of I[01],TOP-REAL n st f is continuous & rng f c= R & f.0=p & f.1=q2); hence thesis by A3; end; theorem Th80: for A being Subset of TOP-REAL n, a being real number st A={q: |.q.|=a} holds A` is open & A is closed proof let A be Subset of TOP-REAL n, a be real number; assume A1: A={q: |.q.|=a}; reconsider a as Real by XREAL_0:def 1; A2: the TopStruct of TOP-REAL n = TopSpaceMetr(Euclid n) by EUCLID:def 8; then reconsider P1=A` as Subset of TopSpaceMetr(Euclid n); for p being Point of Euclid n st p in P1 ex r be real number st r>0 & Ball(p,r) c= P1 proof let p be Point of Euclid n; reconsider q1=p as Point of TOP-REAL n by TOPREAL3:8; assume p in P1; then not p in A by XBOOLE_0:def 5; then A3: |.q1.|<>a by A1; now per cases; case A4: |.q1.|<=a; set r1=(a- |.q1.|)/2; |.q1.|0 by XREAL_1:50; Ball(p,r1) c= P1 proof let x be set; assume A6: x in Ball(p,r1); then reconsider p2=x as Point of Euclid n; reconsider q2=p2 as Point of TOP-REAL n by TOPREAL3:8; dist(p,p2)=|.q2.|- |.q1.| by TOPRNS_1:32; then r1>r1+r1 by A7,A8,XXREAL_0:2; then r1-r1>r1 by XREAL_1:20; hence contradiction by A5; end; hence thesis by XBOOLE_0:def 5; end; hence thesis by A5,XREAL_1:139; end; case A9: |.q1.|>a; set r1=(|.q1.|-a)/2; A10: |.q1.|-a>0 by A9,XREAL_1:50; Ball(p,r1) c= P1 proof let x be set; assume A11: x in Ball(p,r1); then reconsider p2=x as Point of Euclid n; reconsider q2=p2 as Point of TOP-REAL n by TOPREAL3:8; dist(p,p2)=|.q1.|- |.q2.| by TOPRNS_1:32; then r1>r1+r1 by A12,A13,XXREAL_0:2; then r1-r1>r1 by XREAL_1:20; hence contradiction by A10; end; hence thesis by XBOOLE_0:def 5; end; hence thesis by A10,XREAL_1:139; end; end; hence thesis; end; then P1 is open by TOPMETR:15; hence A` is open by A2,PRE_TOPC:30; hence thesis by TOPS_1:3; end; theorem Th81: for B being non empty Subset of TOP-REAL n st B is open holds (TOP-REAL n) | B is locally_connected proof let B be non empty Subset of TOP-REAL n; A1: the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8; assume A2: B is open; for A being non empty Subset of ((TOP-REAL n) | B), C being Subset of (( TOP-REAL n) | B) st A is open & C is_a_component_of A holds C is open proof let A be non empty Subset of (TOP-REAL n) | B, C be Subset of (TOP-REAL n) | B; assume that A3: A is open and A4: C is_a_component_of A; consider C1 being Subset of ((TOP-REAL n) | B) | A such that A5: C1 = C and A6: C1 is a_component by A4,CONNSP_1:def 6; C1 c= [#](((TOP-REAL n) | B) |A); then A7: C1 c= A by PRE_TOPC:def 5; A c= the carrier of (TOP-REAL n) | B; then A c= B by PRE_TOPC:8; then C c= B by A5,A7,XBOOLE_1:1; then reconsider C0=C as Subset of TOP-REAL n by XBOOLE_1:1; reconsider CC = C0 as Subset of TopSpaceMetr Euclid n by A1; for p being Point of Euclid n st p in C0 ex r be real number st r>0 & Ball(p,r) c= C0 proof consider A0 being Subset of TOP-REAL n such that A8: A0 is open and A9: A0 /\ [#]((TOP-REAL n) | B) = A by A3,TOPS_2:24; A10: A0 /\ B=A by A9,PRE_TOPC:def 5; A11: the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8; then reconsider AA=A0 /\ B as Subset of TopSpaceMetr Euclid n; let p be Point of Euclid n; assume A12: p in C0; AA is open by A2,A8,A11,PRE_TOPC:30; then consider r1 being real number such that A13: r1>0 and A14: Ball(p,r1) c= AA by A5,A7,A12,A10,TOPMETR:15; reconsider r1 as Real by XREAL_0:def 1; A15: Ball(p,r1) c= A by A9,A14,PRE_TOPC:def 5; then reconsider BL2=Ball(p,r1) as Subset of (TOP-REAL n) | B by XBOOLE_1:1; Ball(p,r1) c= [#](((TOP-REAL n) | B) |A) by A15,PRE_TOPC:def 5; then reconsider BL=Ball(p,r1) as Subset of ((TOP-REAL n) | B) |A; reconsider BL as Subset of ((TOP-REAL n) | B) |A; reconsider BL2 as Subset of (TOP-REAL n) | B; reconsider BL1=Ball(p,r1) as Subset of TOP-REAL n by TOPREAL3:8; reconsider BL1 as Subset of TOP-REAL n; now p in BL by A13,GOBOARD6:1; then BL /\ C <>{}(((TOP-REAL n) | B) |A) by A12,XBOOLE_0:def 4; then A16: BL meets C by XBOOLE_0:def 7; BL1 is convex by Th70; then A17: BL2 is connected by CONNSP_1:46; assume not Ball(p,r1) c= C0; hence contradiction by A5,A6,A17,A16,CONNSP_1:36,46; end; hence thesis by A13; end; then CC is open by TOPMETR:15; then A18: [#]((TOP-REAL n) | B)=B & C0 is open by A1,PRE_TOPC:30,def 5; C c= the carrier of ((TOP-REAL n) | B); then C c= B by PRE_TOPC:8; then C0 /\ B=C by XBOOLE_1:28; hence thesis by A18,TOPS_2:24; end; hence thesis by CONNSP_2:18; end; theorem Th82: for B being non empty Subset of TOP-REAL n, A being Subset of TOP-REAL n,a being real number st A={q: |.q.|=a} & A`=B holds (TOP-REAL n) | B is locally_connected proof let B be non empty Subset of TOP-REAL n, A be Subset of TOP-REAL n,a be real number; assume A1: A={q: |.q.|=a} & A`=B; then A` is open by Th80; hence thesis by A1,Th81; end; theorem Th83: for f being Function of TOP-REAL n,R^1 st (for q holds f.q=|.q.| ) holds f is continuous proof let f be Function of TOP-REAL n,R^1; A1: the TopStruct of TOP-REAL n = TopSpaceMetr(Euclid n) by EUCLID:def 8; then reconsider f1=f as Function of TopSpaceMetr(Euclid n),TopSpaceMetr(RealSpace ) by TOPMETR:def 6; assume A2: for q holds f.q=|.q.|; now let r be real number,u be Element of Euclid n,u1 be Element of RealSpace; assume that A3: r>0 and A4: u1=f1.u; set s1=r; for w being Element of Euclid n, w1 being Element of RealSpace st w1= f1.w & dist(u,w)0 & for w being Element of Euclid n, w1 being Element of RealSpace st w1=f1.w & dist(u,w) implies |.q.|=abs(r) proof assume A1: q=<*r*>; reconsider xr=<*r*> as Element of REAL 1 by FINSEQ_2:131; len xr=1 by FINSEQ_1:39; then A2: q/.1=xr.1 by A1,FINSEQ_4:15; then len (sqr xr) =1 & (sqr xr).1=(q/.1)^2 by CARD_1:def 7,VALUED_1:11; then A3: sqr xr=<*(q/.1)^2*> by FINSEQ_1:40; sqrt (q/.1)^2 =abs(q/.1) by COMPLEX1:72 .=abs(r) by A2,FINSEQ_1:40; hence thesis by A1,A3,FINSOP_1:11; end; theorem for A being Subset of TOP-REAL n,a being Real st n>=1 & a>0 & A={q: |. q.|=a} holds BDD A is_inside_component_of A proof let A be Subset of TOP-REAL n,a be Real; {q where q is Point of TOP-REAL n: (|.q.|) =1 & a>0 & A={q: |.q.|=a}; A3: P c= A` proof let x; assume A4: x in P; then reconsider q=x as Point of TOP-REAL n; A5: ex q1 st q1=q & |.q1.|{} 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 as Subset of Euclid n; now 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; then consider q such that A14: q in D2 and A15: |.q.|>=a by Th34; A16: A` is open & D2 is connected by A2,A13,Th80,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,Th82; 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; p <> 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=p and A25: f1.1=q by A8,A10,A14,A19,A21,A16,Th79; A26: |.f1/.1.|>=a by A15,A25,BORSUK_1:def 15,FUNCT_2:def 13; |.p.|{}(the carrier of TOP-REAL n) by A17,A28,XBOOLE_0:def 4; then A meets A` by XBOOLE_0:def 7; hence contradiction by XBOOLE_1:79; end; hence thesis by Th11; end; then A29: P1 is_inside_component_of A by A12,Th13; A30: P1 c= union{B where B is Subset of TOP-REAL n: B is_inside_component_of A} proof let x be set; assume A31: x in P1; P1 in {B where B is Subset of TOP-REAL n: B is_inside_component_of A} by A29; hence thesis by A31,TARSKI:def 4; end; now per cases; case A32: n>=2; 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 set; assume x in union{B where B is Subset of TOP-REAL n: B is_inside_component_of A}; 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,Th13; 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 by XXREAL_0:1; now per cases by A38; case A39: p in {q: |.q.|>a}; {q: |.q.|>a} c= A` proof let z be set; assume z in {q: |.q.|>a}; then consider q such that A40: q=z and A41: |.q.|>a; now assume q in A; then ex q2 st q2=q & |.q2.|=a by A2; hence contradiction by A41; end; hence thesis by A40,XBOOLE_0:def 5; end; then reconsider Q={q: |.q.|>a} as Subset of (TOP-REAL n) | A` by PRE_TOPC:8; reconsider Q as Subset of (TOP-REAL n) | A`; {q: |.q.|>a} c= the carrier of TOP-REAL n proof let z be set; assume z in {q: |.q.|>a}; then ex q st q=z & |.q.|>a; hence thesis; end; then reconsider P2={q: |.q.|>a} as Subset of TOP-REAL n; P2 is Subset of Euclid n by TOPREAL3:8; then reconsider W2={q: |.q.|>a} as Subset of Euclid n; P2 is connected by A32,Th51; then A42: (TOP-REAL n) |P2 is connected by CONNSP_1:def 3; A43: not W2 is bounded by A32,Th61; A44: now assume W2 meets A; then consider z being set such that A45: z in W2 & z in A by XBOOLE_0:3; ( ex q st q=z & |.q.|>a)& ex q2 st q2=z & |.q2.|=a by A2,A45; hence contradiction; end; then W2 /\ A``={} by XBOOLE_0:def 7; 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 ,Th51,Th63; then A47: Component_of Q c= UBD A by Th23; (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,Th22; then p in (BDD A) /\ (UBD A) by A33,A35,A47,A48,XBOOLE_0:def 4; then (BDD A) meets (UBD A) by XBOOLE_0:4; hence thesis by Th24; end; case A49: p in {q1: |.q1.|a by A2; then A57: |.q2.|a by XXREAL_0:1; now per cases by A57; case p in {q: |.q.|>a}; 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 Real such that A60: q0=<*r0*> by A51,FINSEQ_2:97; A61: |.q0.|=abs r0 by A60,Th87; A62: now per cases; suppose r0>=0; then r0=abs r0 by ABSVALUE:def 1; hence p in {q:ex r st q=<*r*> & r>a} or p in {q1:ex r1 st q1=<* r1*> & r1< -a} by A58,A59,A60,A61; end; suppose r0<0; then -r0>a by A59,A61,ABSVALUE:def 1; then --r0< -a by XREAL_1:24; hence p in {q:ex r st q=<*r*> & r>a} or p in {q1:ex r1 st q1=<* r1*> & r1< -a} by A58,A60; end; end; now per cases by A62; suppose A63: p in {q:ex r st q=<*r*> & r>a}; {q:ex r st q=<*r*> & r>a} c= A` proof let z be set; assume z in {q:ex r st q=<*r*> & r>a}; then consider q such that A64: q=z and A65: ex r st q=<*r*> & r>a; consider r such that A66: q=<*r*> and A67: r>a by A65; n=1 by A2,A50,XXREAL_0:1; then reconsider xr=<*r*> as Element of REAL n by FINSEQ_2:131; 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) =abs(q/.1) by COMPLEX1:72 .=abs(r) by A68,FINSEQ_1:40; len sqr xr =1 by A51,CARD_1:def 7; then sqr xr=<*(q/.1)^2*> by A69,FINSEQ_1:40; then A71: |.q.|=abs(r) by A66,A70,FINSOP_1:11 .=r by A2,A67,ABSVALUE:def 1; now assume q in A; then ex q2 st q2=q & |.q2.|=a by A2; hence contradiction by A67,A71; end; hence thesis by A64,XBOOLE_0:def 5; end; then reconsider Q={q:ex r st q=<*r*> & r>a} as Subset of (TOP-REAL n) |A` by PRE_TOPC:8; {q:ex r st q=<*r*> & r>a} c= the carrier of TOP-REAL n proof let z be set; assume z in {q:ex r st q=<*r*> & r>a}; then ex q st q=z & ex r st q=<*r*> & r>a; hence thesis; end; then reconsider P3={q: ex r st q=<*r*> & r>a} as Subset of TOP-REAL n; reconsider W3=P3 as Subset of Euclid n by TOPREAL3:8; reconsider Q as Subset of (TOP-REAL n) | A`; {q: |.q.|>a} c= the carrier of TOP-REAL n proof let z be set; assume z in {q: |.q.|>a}; then ex q st q=z & |.q.|>a; hence thesis; end; then reconsider P2={q: |.q.|>a} as Subset of TOP-REAL n; P2 is Subset of Euclid n by TOPREAL3:8; then reconsider W2={q: |.q.|>a} as Subset of Euclid n; A72: W3 c= W2 proof let z be set; assume z in W3; then consider q such that A73: q=z and A74: ex r st q=<*r*> & r>a; consider r such that A75: q=<*r*> and A76: r>a by A74; A77: r=abs(r) by A2,A76,ABSVALUE:def 1; n=1 by A2,A50,XXREAL_0:1; then reconsider xr=<*r*> as Element of REAL n by FINSEQ_2:131; 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; len sqr xr =1 by A51,CARD_1:def 7; then A80: sqr xr=<*(q/.1)^2*> by A79,FINSEQ_1:40; sqrt (q/.1)^2 =abs(q/.1) by COMPLEX1:72 .=abs(r) by A78,FINSEQ_1:40; then |.q.|=abs(r) by A75,A80,FINSOP_1:11; hence thesis by A73,A76,A77; end; A81: now set z = the Element of W2 /\ A; assume A82: not W2 /\ A={}; then z in W2 by XBOOLE_0:def 4; then A83: ex q st q=z & |.q.|>a; z in A by A82,XBOOLE_0:def 4; then ex q2 st q2=z & |.q2.|=a by A2; hence contradiction by A83; end; then W3 /\ A={} by A72,XBOOLE_1:3,26; then A84: W3 misses A by XBOOLE_0:def 7; W3 /\ A``={} by A81,A72,XBOOLE_1:3,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,Th55; 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,Th59; then Up(Component_of Q) is_outside_component_of A by A87,A84,A89,Th63; then A90: Component_of Q c= UBD A by Th23; B c= BDD A by A55,Th22; then (BDD A) /\ (UBD A)<>{} by A52,A54,A90,A88,XBOOLE_0:def 4; then (BDD A) meets (UBD A) by XBOOLE_0:def 7; hence thesis by Th24; end; suppose A91: p in {q1:ex r1 st q1=<*r1*> & r1< -a}; {q:ex r st q=<*r*> & r< -a} c= A` proof let z be set; assume z in {q:ex r st q=<*r*> & r< -a}; then consider q such that A92: q=z and A93: ex r st q=<*r*> & r< -a; consider r such that A94: q=<*r*> and A95: r< -a by A93; A96: r< -0 by A2,A95; n=1 by A2,A50,XXREAL_0:1; then reconsider xr=<*r*> as Element of REAL n by FINSEQ_2:131; 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; len (sqr xr) =1 by A51,CARD_1:def 7; then A99: sqr xr=<*(q/.1)^2*> by A98,FINSEQ_1:40; sqrt (q/.1)^2 =abs(q/.1) by COMPLEX1:72 .=abs(r) by A97,FINSEQ_1:40; then A100: |.q.|=abs(r) by A94,A99,FINSOP_1:11 .=-r by A96,ABSVALUE:def 1; now assume q in A; then ex q2 st q2=q & |.q2.|=a by A2; hence contradiction by A95,A100; end; hence thesis by A92,XBOOLE_0:def 5; end; then reconsider Q={q:ex r st q=<*r*> & r< -a} as Subset of ( TOP-REAL n) |A` by PRE_TOPC:8; {q:ex r st q=<*r*> & r< -a} c= the carrier of TOP-REAL n proof let z be set; assume z in {q:ex r st q=<*r*> & r< -a}; then ex q st q=z & ex r st q=<*r*> & r< -a; hence thesis; end; then reconsider P3={q: ex r st q=<*r*> & r< -a} as Subset of TOP-REAL n; reconsider W3=P3 as Subset of Euclid n by TOPREAL3:8; reconsider Q as Subset of (TOP-REAL n) | A`; {q: |.q.|>a} c= the carrier of TOP-REAL n proof let z be set; assume z in {q: |.q.|>a}; then ex q st q=z & |.q.|>a; hence thesis; end; then reconsider P2={q: |.q.|>a} as Subset of TOP-REAL n; P2 is Subset of Euclid n by TOPREAL3:8; then reconsider W2={q: |.q.|>a} as Subset of Euclid n; A101: W3 c= W2 proof let z be set; assume z in W3; then consider q such that A102: q=z and A103: ex r st q=<*r*> & r< -a; consider r such that A104: q=<*r*> and A105: r< -a by A103; A106: r< -0 & -r>--a by A2,A105,XREAL_1:24; n=1 by A2,A50,XXREAL_0:1; then reconsider xr=<*r*> as Element of REAL n by FINSEQ_2:131; 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; len sqr xr =1 by A51,CARD_1:def 7; then A109: sqr xr=<*(q/.1)^2*> by A108,FINSEQ_1:40; sqrt (q/.1)^2 =abs(q/.1) by COMPLEX1:72 .=abs(r) by A107,FINSEQ_1:40; then |.q.|=abs(r) by A104,A109,FINSOP_1:11; then |.q.|>a by A106,ABSVALUE:def 1; hence thesis by A102; end; A110: now set z = the Element of W2 /\ A; assume A111: not W2 /\ A={}; then z in W2 by XBOOLE_0:def 4; then A112: ex q st q=z & |.q.|>a; z in A by A111,XBOOLE_0:def 4; then ex q2 st q2=z & |.q2.|=a by A2; hence contradiction by A112; end; then W3 /\ A={} by A101,XBOOLE_1:3,26; then A113: W3 misses A by XBOOLE_0:def 7; W3 /\ A``={} by A110,A101,XBOOLE_1:3,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,Th56; 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,Th63,A51,Th60; then A119: Component_of Q c= UBD A by Th23; B c= BDD A by A55,Th22; then p in (BDD A) /\ (UBD A) by A52,A54,A119,A117, XBOOLE_0:def 4; then (BDD A) meets (UBD A) by XBOOLE_0:def 7; hence thesis by Th24; end; end; hence thesis; end; case A120: p in {q1: |.q1.|len (GoB f1) +1 by A27,GOBOARD2:13,XREAL_1:29; 2 in dom (Y_axis(f1)) by A18,SPRECT_2:16; then (Y_axis(f1)).2=(f1/.2)`2 by GOBOARD1:def 2; then A31: (Y_axis(f1)).2=N-bound L~f1 by A28,EUCLID:52; f1/.5=f1/.1 by A4,FINSEQ_6:def 1; then A32: (Y_axis(f1)).5=N-bound L~f1 by A14,A6,EUCLID:52; A33: rng (Y_axis(f1)) c= {S-bound L~f1,N-bound L~f1} proof let z be set; assume z in rng (Y_axis(f1)); then consider u being set such that A34: u in dom (Y_axis(f1)) and A35: z=(Y_axis(f1)).u by FUNCT_1:def 3; reconsider mu=u as Element of NAT by A34; u in dom f1 by A34,SPRECT_2:16; then u in Seg len f1 by FINSEQ_1:def 3; then 1<=mu & mu<=5 by A4,FINSEQ_1:1; then A36: mu=1 or mu=1+1 or mu=1+2 or mu=1+3 or mu=1+4 by NAT_1:58; per cases by A36; suppose mu=1; hence thesis by A23,A35,TARSKI:def 2; end; suppose mu=2; hence thesis by A31,A35,TARSKI:def 2; end; suppose mu=3; hence thesis by A10,A35,TARSKI:def 2; end; suppose mu=4; hence thesis by A8,A35,TARSKI:def 2; end; suppose mu=5; hence thesis by A32,A35,TARSKI:def 2; end; end; {S-bound L~f1,N-bound L~f1} c= rng (Y_axis(f1)) proof let z be set; assume A37: z in {S-bound L~f1,N-bound L~f1}; per cases by A37,TARSKI:def 2; suppose A38: z=S-bound L~f1; 4 in dom (Y_axis(f1)) by A7,SPRECT_2:16; hence thesis by A8,A38,FUNCT_1:def 3; end; suppose A39: z=N-bound L~f1; 2 in dom (Y_axis(f1)) by A18,SPRECT_2:16; hence thesis by A31,A39,FUNCT_1:def 3; end; end; then A40: S-bound L~f1 < N-bound L~f1 & rng (Y_axis(f1))={S-bound L~f1,N-bound L~ f1} by A33,SPRECT_1:32,XBOOLE_0:def 10; A41: width GoB(f1) = card rng Y_axis(f1) by GOBOARD2:13 .=1+1 by A40,CARD_2:57; then A42: width GoB f1 in Seg (width GoB f1) by FINSEQ_1:1; f1/.(1+1) = E-max L~f1 by SPRECT_1:84; then A43: f/.2=|[(E-max L~f)`1,(N-max L~f)`2]| by A28,EUCLID:53; A44: f1/.1 = W-max L~f1 by SPRECT_1:83; then f/.1=|[(W-max L~f)`1,(N-min L~f)`2]| by A14,EUCLID:53; then f/.1+f/.2=|[(W-max L~f)`1 +(E-max L~f)`1, (N-min L~f)`2+(N-max L~f)`2 ]| by A43,EUCLID:56; then (1/2)*(f/.1+f/.2)= |[1/2*((W-max L~f)`1 +(E-max L~f)`1),N-bound L~f]| by A3,EUCLID:58; then A45: q1=|[0+1/2*((W-max L~f)`1 +(E-max L~f)`1),r1+r+1+(N-bound L~f)]| by EUCLID:56 .=|[1/2*((W-max L~f)`1 +(E-max L~f)`1),r1+r+1+(N-bound L~f)]|; (W-max L~f)`1=W-bound L~f by EUCLID:52; then A46: (W-max L~f)`1<(E-max L~f)`1 by A1,EUCLID:52; A47: f1/.1=W-max L~f1 by SPRECT_1:83; then A48: (GoB f1)*(1,1)`1<=(W-max L~f)`1 by A4,A41,JORDAN5D:5; then (GoB f1)*(1,1)`1<(E-max L~f)`1 by A46,XXREAL_0:2; then (GoB f1)*(1,1)`1 +(GoB f1)*(1,1)`1<(W-max L~f)`1+(E-max L~f)`1 by A48, XREAL_1:8; then A49: 1/2*(2*((GoB f1)*(1,1)`1))<1/2*((W-max L~f)`1+(E-max L~f)`1) by XREAL_1:68 ; 1 in dom (X_axis(f1)) by A22,SPRECT_2:15; then (X_axis(f1)).1=(f1/.1)`1 by GOBOARD1:def 1; then A50: (X_axis(f1)).1=W-bound L~f1 by A47,EUCLID:52; f1/.5=W-max L~f1 by A4,A44,FINSEQ_6:def 1; then A51: (X_axis(f1)).5=W-bound L~f1 by A12,EUCLID:52; A52: rng (X_axis(f1)) c= {W-bound L~f1,E-bound L~f1} proof let z be set; assume z in rng (X_axis(f1)); then consider u being set such that A53: u in dom (X_axis(f1)) and A54: z=(X_axis(f1)).u by FUNCT_1:def 3; reconsider mu=u as Element of NAT by A53; u in dom f1 by A53,SPRECT_2:15; then u in Seg len f1 by FINSEQ_1:def 3; then 1<=mu & mu<=5 by A4,FINSEQ_1:1; then A55: mu=1 or mu=1+1 or mu=1+2 or mu=1+3 or mu=1+4 by NAT_1:58; per cases by A55; suppose mu=1; hence thesis by A50,A54,TARSKI:def 2; end; suppose mu=2; hence thesis by A20,A54,TARSKI:def 2; end; suppose mu=3; hence thesis by A11,A54,TARSKI:def 2; end; suppose mu=4; hence thesis by A15,A54,TARSKI:def 2; end; suppose mu=5; hence thesis by A51,A54,TARSKI:def 2; end; end; {W-bound L~f1,E-bound L~f1} c= rng (X_axis(f1)) proof let z be set; assume A56: z in {W-bound L~f1,E-bound L~f1}; per cases by A56,TARSKI:def 2; suppose A57: z=W-bound L~f1; 1 in dom (X_axis(f1)) by A22,SPRECT_2:15; hence thesis by A50,A57,FUNCT_1:def 3; end; suppose A58: z=E-bound L~f1; 2 in dom (X_axis(f1)) by A18,SPRECT_2:15; hence thesis by A20,A58,FUNCT_1:def 3; end; end; then A59: rng (X_axis(f1))={W-bound L~f1,E-bound L~f1} by A52,XBOOLE_0:def 10; A60: len GoB(f1) = card rng X_axis(f1) by GOBOARD2:13 .=1+1 by A1,A59,CARD_2:57; then A61: (GoB f1)*(1+1,1)`1>=(E-max L~f)`1 by A4,A17,A41,JORDAN5D:5; then (W-max L~f)`1 <(GoB f1)*(1+1,1)`1 by A46,XXREAL_0:2; then (W-max L~f)`1+(E-max L~f)`1< (GoB f1)*(1+1,1)`1 +(GoB f1)*(1+1,1)`1 by A61,XREAL_1:8; then A62: 1/2*((W-max L~f)`1+(E-max L~f)`1)< 1/2*(2*((GoB f1)*(1+1,1)`1)) by XREAL_1:68; A63: card rng (X_axis(f1))=2 by A1,A59,CARD_2:57; for p being FinSequence of the carrier of TOP-REAL 2 st p in rng GoB f1 holds len p = 2 proof len GoB(Incr(X_axis(f1)),Incr(Y_axis(f1)) ) =len (Incr(X_axis(f1))) by GOBOARD2:def 1 .=2 by A63,SEQ_4:def 21; then consider s1 being FinSequence such that A64: s1 in rng GoB(Incr(X_axis(f1)),Incr(Y_axis(f1)) ) and A65: len s1 = width GoB(Incr(X_axis(f1)),Incr(Y_axis(f1))) by MATRIX_1:def 3; let p be FinSequence of the carrier of TOP-REAL 2; consider n being Nat such that A66: for x st x in rng GoB f1 ex s being FinSequence st s=x & len s = n by MATRIX_1:def 1; assume p in rng GoB f1; then A67: ex s2 being FinSequence st s2=p & len s2 = n by A66; ex s being FinSequence st s=s1 & len s = n by A16,A64,A66; hence thesis by A41,A65,A67,GOBOARD2:def 2; end; then A68: GoB f1 is Matrix of 2,2,the carrier of TOP-REAL 2 by A60,MATRIX_1:def 2; len GoB f1 in Seg len GoB f1 by A60,FINSEQ_1:1; then [len GoB f1,width GoB f1] in [:Seg (len GoB f1),Seg (width GoB f1):] by A42,ZFMISC_1:87; then A69: [len GoB f1,width GoB f1] in Indices GoB f1 by A60,A41,A68,MATRIX_1:24; 1 in Seg len GoB f1 by A60,FINSEQ_1:1; then [1,width GoB f1] in [:Seg (len GoB f1),Seg (width GoB f1):] by A42, ZFMISC_1:87; then A70: [1,width GoB f1] in Indices GoB f1 by A60,A41,A68,MATRIX_1:24; card rng X_axis(f1) >1 by A27,A29,XXREAL_0:2; then A71: 1=|.(|[0,r1+r+1]|).|-r1 & r width (GoB f1)+1; f1/.(1+1)=(GoB f1)*(len (GoB f1),width (GoB f1)) by A60,A41,Th89; then left_cell(f1,1) = cell(GoB(f1),1,width GoB(f1)) by A4,A70,A69,A72,A30 ,A76,GOBOARD5:def 7; then A77: Int (left_cell(f1,1))= { |[r2,s]| : (GoB f1)*(1,1)`1 < r2 & r2 < (GoB f1)*(1+1,1)`1 & (GoB f1)*(1,width (GoB f1))`2 < s } by A71,GOBOARD6:25; A78: |.q4.|=r1 by A2,Th34; A7: now assume q4 in {q where q is Point of TOP-REAL 2: (|.q.|) =r1 by Th34; A15: now assume q3 in {q where q is Point of TOP-REAL 2: (|.q.|) {} & UBD (L~SpStSeq D) is_outside_component_of (L~SpStSeq D) & BDD (L~SpStSeq D)<>{} & BDD (L~SpStSeq D) is_inside_component_of (L~SpStSeq D) proof set f=SpStSeq D; A1: UBD (L~SpStSeq D)=LeftComp (SpStSeq D) by Th95; hence UBD (L~SpStSeq D)<>{}; LeftComp f is_a_component_of (L~f)` & not LeftComp f is bounded by Th90, GOBOARD9:def 1; hence UBD (L~SpStSeq D) is_outside_component_of (L~SpStSeq D) by A1,Def3; A2: BDD (L~SpStSeq D)=RightComp (SpStSeq D) by Th95; hence BDD (L~SpStSeq D)<>{}; RightComp (SpStSeq D) is_a_component_of (L~f)` & RightComp (SpStSeq D) is bounded by Th94,GOBOARD9:def 2; hence thesis by A2,Def2; end; begin :: Jordan property and boundary property theorem Th97: for G being non empty TopSpace, A being Subset of G st A`<>{} holds A is boundary iff for x being set,V being Subset of G st x in A & x in V & V is open ex B being Subset of G st B is_a_component_of A` & V meets B proof let G be non empty TopSpace,A be Subset of G; assume A1: A`<>{}; hereby reconsider A1=A` as non empty Subset of G by A1; reconsider A2=A` as Subset of G; assume A is boundary; then A` is dense by TOPS_1:def 4; then A2: Cl (A`)=[#] G by TOPS_1:def 3; let x be set,V be Subset of G; assume that x in A and A3: x in V & V is open; A2 meets V by A3,A2,PRE_TOPC:def 7; then consider z being set such that A4: z in A` and A5: z in V by XBOOLE_0:3; reconsider p=z as Point of G|A` by A4,PRE_TOPC:8; Component_of p c= the carrier of G|A`; then Component_of p c= A` by PRE_TOPC:8; then reconsider B0=Component_of p as Subset of G by XBOOLE_1:1; A6: G|A1 is non empty; then p in Component_of p by CONNSP_1:38; then p in V /\ B0 by A5,XBOOLE_0:def 4; then A7: V meets B0 by XBOOLE_0:4; Component_of p is a_component by A6,CONNSP_1:40; then B0 is_a_component_of A` by CONNSP_1:def 6; hence ex B being Subset of G st B is_a_component_of A` & V meets B by A7; end; assume A8: for x being set,V being Subset of G st x in A & x in V & V is open ex B being Subset of G st B is_a_component_of A` & V meets B; the carrier of G c= Cl (A`) proof let z be set; assume A9: z in the carrier of G; per cases; suppose A10: z in A; for G1 being Subset of G st G1 is open holds z in G1 implies (A`) meets G1 proof let G1 be Subset of G; assume A11: G1 is open; assume z in G1; then consider B being Subset of G such that A12: B is_a_component_of A` and A13: G1 meets B by A8,A10,A11; A14: G1 /\ B <> {} by A13,XBOOLE_0:def 7; consider B1 being Subset of G|A` such that A15: B1 = B and B1 is a_component by A12,CONNSP_1:def 6; B1 c= the carrier of (G|A`); then B1 c= A` by PRE_TOPC:8; then (A`) /\ G1 <> {}G by A15,A14,XBOOLE_1:3,26; hence thesis by XBOOLE_0:def 7; end; hence thesis by A9,PRE_TOPC:def 7; end; suppose A16: not z in A; A17: A` c= Cl(A`) by PRE_TOPC:18; z in (the carrier of G) \ A by A9,A16,XBOOLE_0:def 5; hence thesis by A17; end; end; then Cl (A`)=[#] G by XBOOLE_0:def 10; then A` is dense by TOPS_1:def 3; hence thesis by TOPS_1:def 4; end; theorem Th98: for A being Subset of TOP-REAL 2 st A`<>{} holds A is boundary & A is Jordan iff ex A1,A2 being Subset of TOP-REAL 2 st A` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A=(Cl A1) \ A1 & for C1,C2 being Subset of (TOP-REAL 2) | A` st C1 = A1 & C2 = A2 holds C1 is a_component & C2 is a_component proof let A be Subset of TOP-REAL 2; assume A1: A`<>{}; hereby assume that A2: A is boundary and A3: A is Jordan; consider A1,A2 being Subset of TOP-REAL 2 such that A4: A` = A1 \/ A2 and A5: A1 misses A2 and A6: (Cl A1) \ A1 = (Cl A2) \ A2 and A7: for C1,C2 being Subset of (TOP-REAL 2) | A` st C1 = A1 & C2 = A2 holds C1 is a_component & C2 is a_component by A3,JORDAN1:def 2; A=(A1 \/ A2)` by A4; then A8: A=A1` /\ A2` by XBOOLE_1:53; A2 c= A` by A4,XBOOLE_1:7; then reconsider D2=A2 as Subset of (TOP-REAL 2) | A` by PRE_TOPC:8; A1 c= A` by A4,XBOOLE_1:7; then reconsider D1=A1 as Subset of (TOP-REAL 2) | A` by PRE_TOPC:8; D2=A2; then A9: D1 is a_component by A7; A10: A c= (Cl A1) \ A1 proof let z be set; assume A11: z in A; for G being Subset of (TOP-REAL 2) st G is open holds z in G implies (A1 \/ A2) meets G proof let G be Subset of (TOP-REAL 2); assume A12: G is open; hereby assume z in G; then consider B being Subset of TOP-REAL 2 such that A13: B is_a_component_of A` and A14: G meets B by A1,A2,A11,A12,Th97; consider B1 being Subset of (TOP-REAL 2) | A` such that A15: B1 = B and A16: B1 is a_component by A13,CONNSP_1:def 6; A17: now per cases by A9,A16,CONNSP_1:34; case B1=D1; hence B1 c= A1 \/ A2 by XBOOLE_1:7; end; case B1,D1 are_separated; then A18: Cl B1 misses D1 or B1 misses Cl D1 by CONNSP_1:def 1; B1 is closed & D1 is closed by A9,A16,CONNSP_1:33; then B1 misses D1 by A18,PRE_TOPC:22; then A19: B1 /\ D1={} by XBOOLE_0:def 7; B1 c= the carrier of (TOP-REAL 2) | A`; then B1 c= A` by PRE_TOPC:8; then B1 = B1 /\ A` by XBOOLE_1:28 .=B1 /\ A1 \/ B1 /\ A2 by A4,XBOOLE_1:23 .= B1 /\ A2 by A19; then A20: B1 c= A2 by XBOOLE_1:17; A2 c= A1 \/ A2 by XBOOLE_1:7; hence B1 c= A1 \/ A2 by A20,XBOOLE_1:1; end; end; G /\ B <> {} by A14,XBOOLE_0:def 7; then (A1 \/ A2) /\ G <> {} by A15,A17,XBOOLE_1:3,26; hence (A1 \/ A2) meets G by XBOOLE_0:def 7; end; end; then z in Cl (A1 \/ A2) by A11,PRE_TOPC:def 7; then z in (Cl A1) \/ Cl A2 by PRE_TOPC:20; then A21: z in Cl A1 or z in Cl A2 by XBOOLE_0:def 3; not z in A` by A11,XBOOLE_0:def 5; then ( not z in A1)& not z in A2 by A4,XBOOLE_0:def 3; hence thesis by A6,A21,XBOOLE_0:def 5; end; (Cl A1) \A1 c= A1` & (Cl A2) \A2 c= A2` by XBOOLE_1:33; then (Cl A1) \A1 c= A by A6,A8,XBOOLE_1:19; then A=Cl A1 \ A1 by A10,XBOOLE_0:def 10; hence ex A1,A2 being Subset of TOP-REAL 2 st A` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A=(Cl A1) \ A1 & for C1,C2 being Subset of (TOP-REAL 2) | A` st C1 = A1 & C2 = A2 holds C1 is a_component & C2 is a_component by A4,A5,A6,A7; end; hereby assume ex A1,A2 being Subset of TOP-REAL 2 st A` = A1 \/ A2 & A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 & A=(Cl A1) \ A1 & for C1,C2 being Subset of (TOP-REAL 2) | A` st C1 = A1 & C2 = A2 holds C1 is a_component & C2 is a_component; then consider A1,A2 being Subset of TOP-REAL 2 such that A22: A` = A1 \/ A2 and A23: A1 misses A2 & (Cl A1) \ A1 = (Cl A2) \ A2 and A24: A=(Cl A1) \ A1 and A25: for C1,C2 being Subset of (TOP-REAL 2) | A` st C1 = A1 & C2 = A2 holds C1 is a_component & C2 is a_component; for x being set,V being Subset of TOP-REAL 2 st x in A & x in V & V is open ex B being Subset of TOP-REAL 2 st B is_a_component_of A` & V meets B proof A2 c= A` by A22,XBOOLE_1:7; then reconsider D2=A2 as Subset of (TOP-REAL 2) | A` by PRE_TOPC:8; A1 c= A` by A22,XBOOLE_1:7; then reconsider D1=A1 as Subset of (TOP-REAL 2) | A` by PRE_TOPC:8; let x be set,V be Subset of TOP-REAL 2; assume that A26: x in A and A27: x in V & V is open; D2=A2; then D1 is a_component by A25; then A28: A1 is_a_component_of A` by CONNSP_1:def 6; x in Cl A1 by A24,A26,XBOOLE_0:def 5; then A1 meets V by A27,PRE_TOPC:def 7; hence thesis by A28; end; hence A is boundary & A is Jordan by A1,A22,A23,A25,Th97,JORDAN1:def 2; end; end; theorem Th99: for p being Point of TOP-REAL n, P being Subset of TOP-REAL n st n>=1 & P={p} holds P is boundary proof let p be Point of TOP-REAL n, P be Subset of TOP-REAL n; assume that A1: n>=1 and A2: P={p}; the carrier of (TOP-REAL n) c= Cl (P`) proof let z be set; assume A3: z in the carrier of TOP-REAL n; per cases; suppose A4: z=p; reconsider ez=z as Point of Euclid n by A3,TOPREAL3:8; for G1 being Subset of (TOP-REAL n) st G1 is open holds z in G1 implies (P`) meets G1 proof let G1 be Subset of TOP-REAL n; assume A5: G1 is open; thus z in G1 implies (P`) meets G1 proof A6: the TopStruct of TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8; then reconsider GG = G1 as Subset of TopSpaceMetr Euclid n; assume A7: z in G1; GG is open by A5,A6,PRE_TOPC:30; then consider r be real number such that A8: r>0 and A9: Ball(ez,r) c= GG by A7,TOPMETR:15; reconsider r as Real by XREAL_0:def 1; set p2=p-(r/2/sqrt n)*(1.REAL n); reconsider ep2=p2 as Point of Euclid n by TOPREAL3:8; A10: 00 by A8,XREAL_1:139; then p<>p2 by A11,TOPRNS_1:28; then not p2 in P by A2,TARSKI:def 1; then A12: p2 in P` by XBOOLE_0:def 5; r/2p; then not z in P by A2,TARSKI:def 1; then A13: z in P` by A3,XBOOLE_0:def 5; P` c= Cl(P`) by PRE_TOPC:18; hence thesis by A13; end; end; then Cl (P`)=[#] (TOP-REAL n) by XBOOLE_0:def 10; then P` is dense by TOPS_1:def 3; hence thesis by TOPS_1:def 4; end; theorem Th100: for p,q being Point of TOP-REAL 2,r st p`1=q`2 & -p`2=q`1 & p=r *q holds p`1=0 & p`2=0 & p=0.TOP-REAL 2 proof let p,q be Point of TOP-REAL 2,r; A1: 1+r*r>0+0 by XREAL_1:8,63; assume p`1=q`2 & -p`2=q`1 & p=r*q; then A2: p=|[r*(-p`2),r*(p`1)]| by EUCLID:57; then p`2=r*(p`1) by EUCLID:52; then p`1=-(r*(r*(p`1))) by A2,EUCLID:52 .=-(r*r*(p`1)); then (1+r*r)*p`1=0; hence A3: p`1=0 by A1,XCMPLX_1:6; p`1=r*(-p`2) by A2,EUCLID:52; then p`2=-(r*r*(p`2)) by A2,EUCLID:52; then (1+r*r)*p`2=0; hence p`2=0 by A1,XCMPLX_1:6; hence thesis by A3,EUCLID:53,54; end; theorem Th101: for q1,q2 being Point of TOP-REAL 2 holds LSeg(q1,q2) is boundary proof let q1,q2 be Point of TOP-REAL 2; per cases; suppose q1=q2; then LSeg(q1,q2)={q1} by RLTOPSP1:70; hence thesis by Th99; end; suppose A1: q1<>q2; set P=LSeg(q1,q2); the carrier of (TOP-REAL 2) c= Cl (P`) proof let z be set; assume A2: z in the carrier of TOP-REAL 2; per cases; suppose A3: z in P; reconsider ez=z as Point of Euclid 2 by A2,TOPREAL3:8; set p1=q1-q2; consider s being Real such that A4: z=(1-s)*q1+s*q2 and 0<=s and s<=1 by A3; set p=(1-s)*q1+s*q2; A5: now assume |.p1.|=0; then p1=0.TOP-REAL 2 by TOPRNS_1:24; hence contradiction by A1,EUCLID:43; end; for G1 being Subset of (TOP-REAL 2) st G1 is open holds z in G1 implies (P`) meets G1 proof let G1 be Subset of TOP-REAL 2; assume A6: G1 is open; thus z in G1 implies (P`) meets G1 proof A7: the TopStruct of TOP-REAL 2 = TopSpaceMetr Euclid 2 by EUCLID:def 8 ; then reconsider GG = G1 as Subset of TopSpaceMetr Euclid 2; assume A8: z in G1; GG is open by A6,A7,PRE_TOPC:30; then consider r be real number such that A9: r>0 and A10: Ball(ez,r) c= G1 by A8,TOPMETR:15; reconsider r as Real by XREAL_0:def 1; A11: r/20 by A5; then |[-p1`2,p1`1]|=0.TOP-REAL 2 by A9,A14,A15,EUCLID:31 ,XCMPLX_1:6; then A16: (0.TOP-REAL 2)`1=-p1`2 & (0.TOP-REAL 2)`2=p1`1 by EUCLID:52; (0.TOP-REAL 2)`1=0 & (0.TOP-REAL 2)`2=0 by EUCLID:52,54; hence contradiction by A1,A16,EUCLID:43,53,54; end; A17: p2-p = (r/2/|.p1.|)*|[-p1`2,p1`1]| by EUCLID:48; p2-p=(1-s2)*q1+s2*q2 -(1-s)*q1-s*q2 by A12,EUCLID:46 .=(1-s2)*q1-(1-s)*q1+s2*q2 -s*q2 by EUCLID:26 .=((1-s2)-(1-s))*q1+s2*q2 -s*q2 by EUCLID:50 .=(s-s2)*q1+(s2*q2 -s*q2) by EUCLID:45 .=(s-s2)*q1+(s2-s)*q2 by EUCLID:50 .=(s-s2)*q1+(-(s-s2))*q2 .=(s-s2)*q1-(s-s2)*q2 by EUCLID:40 .=(s-s2)*p1 by EUCLID:49; then 1/(s-s2)*(s-s2)*p1= 1/(s-s2)*((r/2/|.p1.|)*|[- p1`2,p1`1]| ) by A17,EUCLID:30; then 1 *p1= 1/(s-s2)*((r/2/|.p1.|)*|[-p1`2,p1`1]|) by A13, XCMPLX_1:106; then p1= 1/(s-s2)*((r/2/|.p1.|)*|[-p1`2,p1`1]|) by EUCLID:29; then A18: p1= 1/(s-s2)*(r/2/|.p1.|)*|[-p1`2,p1`1]| by EUCLID:30; p1`1=(|[-p1`2,p1`1]|)`2 & -p1`2=(|[-p1`2,p1`1]|)`1 by EUCLID:52; then p1=0.TOP-REAL 2 by A18,Th100; hence contradiction by A1,EUCLID:43; end; then A19: p2 in (the carrier of TOP-REAL 2) \P by XBOOLE_0:def 5; reconsider ep2=p2 as Point of Euclid 2 by TOPREAL3:8; A20: p+-(r/2/|.p1.|)*|[-p1`2,p1`1]| -p = -(r/2/|.p1.|)*|[-p1`2,p1 `1]| by EUCLID:48; A21: |[-p1`2,p1`1]|`1=-p1`2 & |[-p1`2,p1`1]|`2=p1`1 by EUCLID:52; |.p-p2.|=|.p-(r/2/|.p1.|)*|[-p1`2,p1`1]| -p.| by EUCLID:46 .=|.-(r/2/|.p1.|)*|[-p1`2,p1`1]|.| by A20 .=|.(r/2/|.p1.|)*|[-p1`2,p1`1]|.| by TOPRNS_1:26 .=abs(r/2/|.p1.|)*|.|[-p1`2,p1`1]|.| by TOPRNS_1:7 .=abs(r/2/|.p1.|)*(sqrt ((-p1`2)^2+(p1`1)^2)) by A21,JGRAPH_1:30 .=abs(r/2/|.p1.|)*(sqrt ((p1`1)^2+(p1`2)^2)) .=abs(r/2/|.p1.|)*|.p1.| by JGRAPH_1:30 .=abs(r/2)/(abs(|.p1.|))*|.p1.| by COMPLEX1:67 .=abs(r/2)/(|.p1.|)*|.p1.| by ABSVALUE:def 1 .=abs (r/2) by A5,XCMPLX_1:87 .=r/2 by A9,ABSVALUE:def 1; then dist(ez,ep2) boundary; coherence by Th101; end; theorem Th102: for f being FinSequence of TOP-REAL 2 holds L~f is boundary proof let f be FinSequence of TOP-REAL 2; A1: L~f=union { LSeg(f,i) : 1 <= i & i+1 <= len f } by TOPREAL1:def 4; defpred P[Element of NAT] means for R1 being Subset of TOP-REAL 2 st R1= union { LSeg(f,i) : 1 <= i & i+1 <= $1 } holds R1 is boundary; A2: for k being Element of NAT st P[k] holds P[k+1] proof let k be Element of NAT; A3: now per cases; case 1<=k & k+1<=len f; then LSeg(f,k)=LSeg(f/.k,f/.(k+1)) by TOPREAL1:def 3; hence LSeg(f,k) is boundary; end; case not(1<=k & k+1<=len f); then LSeg(f,k)={} by TOPREAL1:def 3; hence LSeg(f,k) is boundary; end; end; union { LSeg(f,i2) : 1 <= i2 & i2+1 <= k } c= the carrier of TOP-REAL 2 proof let z be set; assume z in union { LSeg(f,i2) : 1 <= i2 & i2+1 <= k }; then consider x such that A4: z in x & x in { LSeg(f,i) : 1 <= i & i+1 <= k } by TARSKI:def 4; ex i st x=LSeg(f,i) & 1 <= i & i+1 <= k by A4; hence thesis by A4; end; then reconsider R3=union { LSeg(f,i2) : 1 <= i2 & i2+1 <= k } as Subset of TOP-REAL 2; assume for R1 being Subset of TOP-REAL 2 st R1=union { LSeg(f,i) : 1 <= i & i+1 <= k } holds R1 is boundary; then A5: R3 is boundary; thus for R2 being Subset of TOP-REAL 2 st R2=union { LSeg(f,i2) : 1 <= i2 & i2+1 <= k+1 } holds R2 is boundary proof let R2 be Subset of TOP-REAL 2; assume A6: R2=union { LSeg(f,i2) : 1 <= i2 & i2+1 <= k+1 }; A7: R3 \/ LSeg(f,k) c= R2 proof let z be set; assume A8: z in R3 \/ LSeg(f,k); per cases by A8,XBOOLE_0:def 3; suppose z in R3; then consider x such that A9: z in x & x in { LSeg(f,i2) : 1 <= i2 & i2+1 <= k } by TARSKI:def 4; consider i2 such that A10: x=LSeg(f,i2) & 1 <= i2 and A11: i2+1 <= k by A9; i2+1k; then k+1<=i2+1 by NAT_1:13; then i2+1=k+1 by A16,XXREAL_0:1; hence z in R3 or z in LSeg(f,k) by A13,A14; end; end; hence thesis by XBOOLE_0:def 3; end; then R2=R3 \/ LSeg(f,k) by A7,XBOOLE_0:def 10; hence thesis by A5,A3,TOPS_1:49; end; end; union { LSeg(f,i) : 1 <= i & i+1 <= 0 } c= {} proof let z be set; assume z in union { LSeg(f,i) : 1 <= i & i+1 <= 0 }; then consider x such that A17: z in x & x in { LSeg(f,i) : 1 <= i & i+1 <= 0 } by TARSKI:def 4; ex i st x=LSeg(f,i) & 1 <= i & i+1 <= 0 by A17; hence thesis; end; then A18: P[0]; for j holds P[j] from NAT_1:sch 1(A18,A2); hence thesis by A1; end; registration let f be FinSequence of TOP-REAL 2; cluster L~f -> boundary; coherence by Th102; end; theorem Th103: for ep being Point of Euclid n,p,q being Point of TOP-REAL n st p=ep & q in Ball(ep,r) holds |.p-q.|0 & p in L~SpStSeq D holds ex q being Point of TOP-REAL 2 st q in UBD (L~SpStSeq D) & |.p-q.|0 and A2: p in L~SpStSeq D; set q1 = the Element of UBD (L~SpStSeq D); set A=L~SpStSeq D; A`<>{} by SPRECT_1:def 3; then consider A1,A2 being Subset of TOP-REAL 2 such that A3: A` = A1 \/ A2 and A1 misses A2 and A4: (Cl A1) \ A1 = (Cl A2) \ A2 and A5: A=(Cl A1) \ A1 and A6: for C1,C2 being Subset of (TOP-REAL 2) | A` st C1 = A1 & C2 = A2 holds C1 is a_component & C2 is a_component by Th98; A7: Down(A2,A`)=A2 by A3,XBOOLE_1:21; UBD A is_outside_component_of A by Th68; then UBD (L~SpStSeq D) is_a_component_of A` by Def3; then consider B1 being Subset of (TOP-REAL 2) | A` such that A8: B1 = UBD (L~SpStSeq D) and A9: B1 is a_component by CONNSP_1:def 6; B1 c= [#]((TOP-REAL 2) | A`); then A10: UBD (L~SpStSeq D) c= A1 \/ A2 by A3,A8,PRE_TOPC:def 5; A11: Down(A1,A`)=A1 by A3,XBOOLE_1:21; then A12: Down(A1,A`) is a_component by A6,A7; A13: Down(A2,A`) is a_component by A6,A11,A7; A14: UBD (L~SpStSeq D) <>{} by Th96; then A15: q1 in UBD (L~SpStSeq D); per cases by A10,A15,XBOOLE_0:def 3; suppose q1 in A1; then B1 /\ Down(A1,A`)<>{}((TOP-REAL 2) | A`) by A11,A8,A14,XBOOLE_0:def 4; then B1 meets Down(A1,A`) by XBOOLE_0:def 7; then B1=Down(A1,A`) by A12,A9,CONNSP_1:35; then A16: p in Cl(UBD (L~SpStSeq D)) by A2,A5,A11,A8,XBOOLE_0:def 5; reconsider ep=p as Point of Euclid 2 by TOPREAL3:8; reconsider G2=Ball(ep,a) as Subset of TOP-REAL 2 by TOPREAL3:8; the distance of Euclid 2 is Reflexive by METRIC_1:def 6; then dist(ep,ep)=0 by METRIC_1:def 2; then A17: p in Ball(ep,a) by A1,METRIC_1:11; G2 is open by GOBOARD6:3; then (UBD (L~SpStSeq D)) meets G2 by A16,A17,PRE_TOPC:def 7; then consider t2 being set such that A18: t2 in UBD (L~SpStSeq D) and A19: t2 in G2 by XBOOLE_0:3; reconsider qt2=t2 as Point of TOP-REAL 2 by A18; |.p-qt2.|{}((TOP-REAL 2) | A`) by A7,A8,A14,XBOOLE_0:def 4; then B1 meets Down(A2,A`) by XBOOLE_0:def 7; then B1=Down(A2,A`) by A13,A9,CONNSP_1:35; then A20: p in Cl(UBD (L~SpStSeq D)) by A2,A4,A5,A7,A8,XBOOLE_0:def 5; reconsider ep=p as Point of Euclid 2 by TOPREAL3:8; reconsider G2=Ball(ep,a) as Subset of TOP-REAL 2 by TOPREAL3:8; (the distance of (Euclid 2)) is Reflexive by METRIC_1:def 6; then dist(ep,ep)=0 by METRIC_1:def 2; then A21: p in Ball(ep,a) by A1,METRIC_1:11; G2 is open by GOBOARD6:3; then (UBD (L~SpStSeq D)) meets G2 by A20,A21,PRE_TOPC:def 7; then consider t2 being set such that A22: t2 in (UBD (L~SpStSeq D)) and A23: t2 in G2 by XBOOLE_0:3; reconsider qt2=t2 as Point of TOP-REAL 2 by A22; |.p-qt2.|=1; set a=r; reconsider P=(REAL n)\ {q : (|.q.|) < a } as Subset of TOP-REAL n by EUCLID:22; A3: P c= A` proof let z; assume A4: z in P; then reconsider q0=z as Point of TOP-REAL n; not z in {q : (|.q.|) < a } by A4,XBOOLE_0:def 5; then (|.q0.|) >= a; then not q0 in A by A1; hence thesis by XBOOLE_0:def 5; end; then A5: Down(P,A`)=P by XBOOLE_1:28; now per cases; suppose n>=2; then A6: P is connected by Th53; now assume not BDD A is bounded; then consider q being Point of TOP-REAL n such that A7: q in BDD A and A8: not |.q.|= a by A8; then not q in {q2 where q2 is Point of TOP-REAL n: (|.q2.|) < a }; 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,CONNSP_1:36,46; B3 is bounded by A12,Def2; hence contradiction by A2,A14,A16,Th54,RLTOPSP1:42; end; hence thesis; end; suppose A17: n<2; {q where q is Point of TOP-REAL n: for r2 being Real st q=|[r2]| holds r2>=a} c= the carrier of TOP-REAL n proof let z; assume z in {q where q is Point of TOP-REAL n: for r2 being Real st q=|[r2]| holds r2>=a}; then ex q being Point of TOP-REAL n st q=z & for r2 being Real st q= |[r2]| holds r2>=a; hence thesis; end; then reconsider P2={q where q is Point of TOP-REAL n: for r2 being Real st q=|[r2]| holds r2>=a} as Subset of TOP-REAL n; {q where q is Point of TOP-REAL n: for r2 being Real st q=|[r2]| holds r2<=-a} c= the carrier of TOP-REAL n proof let z; assume z in {q where q is Point of TOP-REAL n: for r2 being Real st q=|[r2]| holds r2<=-a}; then ex q being Point of TOP-REAL n st q=z & for r2 being Real st q= |[r2]| holds r2<=-a; hence thesis; end; then reconsider P1={q where q is Point of TOP-REAL n: for r2 being Real st q=|[r2]| holds r2<=-a} as Subset of TOP-REAL n; n<1+1 by A17; then n<=1 by NAT_1:13; then A18: n=1 by A2,XXREAL_0:1; A19: P c= P1 \/ P2 proof let z; assume A20: z in P; then reconsider q0=z as Point of TOP-REAL n; consider r3 being Real such that A21: q0=<*r3*> by A18,JORDAN2B:20; not z in {q : (|.q.|) < a } by A20,XBOOLE_0:def 5; then (|.q0.|) >= a; then A22: abs r3>=a by A21,Th10; per cases by A22,SEQ_2:1; suppose -a>=r3; then for r2 being Real st q0=|[r2]| holds r2<=-a by A21,JORDAN2B:23 ; then q0 in P1; hence thesis by XBOOLE_0:def 3; end; suppose r3>=a; then for r2 being Real st q0=|[r2]| holds r2>=a by A21,JORDAN2B:23; then q0 in P2; hence thesis by XBOOLE_0:def 3; end; end; P1 \/ P2 c= P proof let z; assume A23: z in P1 \/ P2; per cases by A23,XBOOLE_0:def 3; suppose A24: z in P1; then A25: ex q being Point of TOP-REAL n st q=z & for r2 being Real st q =|[r2]| holds r2<=-a; for q2 being Point of TOP-REAL n st q2=z holds |.q2.| >= a proof let q2 be Point of TOP-REAL n; consider r3 being Real such that A26: q2=<*r3*> by A18,JORDAN2B:20; assume A27: q2=z; then A28: r3<=-a by A25,A26; now per cases; case a<0; hence abs r3 >=a by COMPLEX1:46; end; case a>=0; then -a<=-0; then abs r3=-r3 by A28,ABSVALUE:30; hence abs r3>=a by A25,A27,A26,XREAL_1:25; end; end; hence thesis by A26,Th10; end; then A29: not z in {q2 where q2 is Point of TOP-REAL n: |.q2.| < a }; z in the carrier of TOP-REAL n by A24; then z in REAL n by EUCLID:22; hence thesis by A29,XBOOLE_0:def 5; end; suppose A30: z in P2; then A31: ex q being Point of TOP-REAL n st q=z & for r2 being Real st q =|[r2]| holds r2>=a; for q2 being Point of TOP-REAL n st q2=z holds |.q2.| >= a proof let q2 be Point of TOP-REAL n; consider r3 being Real such that A32: q2=<*r3*> by A18,JORDAN2B:20; assume q2=z; then A33: r3>=a by A31,A32; now per cases; suppose a<0; hence abs r3>=a by COMPLEX1:46; end; suppose a>=0; hence abs r3 >=a by A33,ABSVALUE:def 1; end; end; hence thesis by A32,Th10; end; then A34: not z in {q2 where q2 is Point of TOP-REAL n: |.q2.| < a }; z in the carrier of TOP-REAL n by A30; then z in REAL n by EUCLID:22; hence thesis by A34,XBOOLE_0:def 5; end; end; then A35: P=P1 \/ P2 by A19,XBOOLE_0:def 10; then P2 c= P by XBOOLE_1:7; then A36: Down(P2,A`)=P2 by A3,XBOOLE_1: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; assume that A37: w1 in P2 and A38: w2 in P2; A39: ex q2 being Point of TOP-REAL n st q2=w2 & for r2 being Real st q2=|[r2]| holds r2>=a by A38; consider r3 being Real such that A40: w1=<*r3*> by A18,JORDAN2B:20; consider r4 being Real such that A41: w2=<*r4*> by A18,JORDAN2B:20; A42: ex q1 being Point of TOP-REAL n st q1=w1 & for r2 being Real st q1=|[r2]| holds r2>=a by A37; thus LSeg(w1,w2) c= P2 proof let z; assume z in LSeg(w1,w2); then consider r2 such that A43: z=(1-r2)*w1 + r2*w2 and A44: 0 <= r2 and A45: r2 <= 1; reconsider q4=z as Point of TOP-REAL n by A43; (1-r2)*w1=|[(1-r2)*r3]| & r2*w2=|[r2*r4]| by A18,A40,A41, JORDAN2B:21; then A46: z=|[(1-r2)*r3+r2*r4]| by A18,A43,JORDAN2B:22; for r5 being Real st q4=|[r5]| holds r5>=a proof let r5 be Real; assume q4=|[r5]|; then A47: r5=(1-r2)*r3+r2*r4 by A46,JORDAN2B:23; 1-r2>=0 by A45,XREAL_1:48; then A48: (1-r2)*r3>=(1-r2)*(a) by A42,A40,XREAL_1:64; r2*r4>=r2*(a) & (1-r2)*(a)+r2*(a)=a by A39,A41,A44,XREAL_1:64; hence thesis by A47,A48,XREAL_1:7; end; hence thesis; end; end; then P2 is convex by JORDAN1:def 1; then A49: Down(P2,A`) is connected by A36,CONNSP_1:46; P1 c= P by A35,XBOOLE_1:7; then A50: Down(P1,A`)=P1 by A3,XBOOLE_1:1,28; A51: now assume P2 is bounded; then consider r being Real such that A52: for q being Point of TOP-REAL n st q in P2 holds |.q.|=a proof let r5 be Real; assume p3=|[r5]|; then A55: r5=(abs(r)+abs(a)) by JORDAN2B:23; a<=abs(a) & abs(a)<=abs(a)+abs(r) by ABSVALUE:4,COMPLEX1:46 ,XREAL_1:31; hence thesis by A55,XXREAL_0:2; end; then A56: p3 in P2 by A18; |.p3.|=abs((abs(r)+abs(a))) & r<=abs(r) by Th10,ABSVALUE:4; hence contradiction by A52,A56,A53,A54,XXREAL_0:2; end; A57: now assume P1 is bounded; then consider r being Real such that A58: for q being Point of TOP-REAL n st q in P1 holds |.q.|= -(abs(a)+abs(r)) by XREAL_1:24; assume p3=|[r5]|; then r5=-(abs(r)+abs(a)) by JORDAN2B:23; hence thesis by A61,A62,XXREAL_0:2; end; then A63: p3 in P1 by A18; |.p3.|=abs(-(abs(r)+abs(a))) by Th10 .=abs ((abs(r)+abs(a))) by COMPLEX1:52; hence contradiction by A58,A63,A59,A60,XXREAL_0:2; 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; assume that A64: w1 in P1 and A65: w2 in P1; consider r4 being Real such that A66: w2=<*r4*> by A18,JORDAN2B:20; ex q2 being Point of TOP-REAL n st q2=w2 & for r2 being Real st q2=|[r2]| holds r2<=-a by A65; then A67: r4<=-a by A66; consider r3 being Real such that A68: w1=<*r3*> by A18,JORDAN2B:20; ex q1 being Point of TOP-REAL n st q1=w1 & for r2 being Real st q1=|[r2]| holds r2<=-a by A64; then A69: r3<=-a by A68; thus LSeg(w1,w2) c= P1 proof let z; assume z in LSeg(w1,w2); then consider r2 such that A70: z=(1-r2)*w1 + r2*w2 and A71: 0 <= r2 and A72: r2 <= 1; reconsider q4=z as Point of TOP-REAL n by A70; A73: r2*w2=|[r2*r4]| by A18,A66,JORDAN2B:21; (1-r2)*w1 = (1-r2)*|[r3]| by A68 .=|[(1-r2)*r3]| by JORDAN2B:21; then A74: z=|[(1-r2)*r3+r2*r4]| by A18,A70,A73,JORDAN2B:22; for r5 being Real st q4=|[r5]| holds r5<=-a proof let r5 be Real; assume q4=|[r5]|; then A75: r5=(1-r2)*r3+r2*r4 by A74,JORDAN2B:23; 1-r2>=0 by A72,XREAL_1:48; then A76: (1-r2)*r3<=(1-r2)*(-a) by A69,XREAL_1:64; r2*r4<=r2*(-a) & (1-r2)*(-a)+r2*(-a)=-a by A67,A71,XREAL_1:64; hence thesis by A75,A76,XREAL_1:7; end; hence thesis; end; end; then P1 is convex by JORDAN1:def 1; then A77: Down(P1,A`) is connected by A50,CONNSP_1:46; now assume not BDD A is bounded; then consider q being Point of TOP-REAL n such that A78: q in BDD A and A79: not |.q.|= a by A79; then not q in {q2 where q2 is Point of TOP-REAL n: |.q2.| < a }; then A85: q in P by A84,XBOOLE_0:def 5; B3 is_a_component_of A` by A83,Def2; then consider B4 being Subset of (TOP-REAL n) | A` such that A86: B4 = B3 and A87: B4 is a_component by CONNSP_1:def 6; per cases by A19,A85,XBOOLE_0:def 3; suppose q in P1; then P1 /\ B4<>{}((TOP-REAL n) | A`) by A80,A82,A86,XBOOLE_0:def 4; then A88: P1 meets B4 by XBOOLE_0:def 7; B3 is bounded by A83,Def2; hence contradiction by A50,A57,A77,A86,A87,A88,CONNSP_1:36,RLTOPSP1:42; end; suppose q in P2; then P2 /\ B4<>{}((TOP-REAL n) | A`) by A80,A82,A86,XBOOLE_0:def 4; then A89: P2 meets B4 by XBOOLE_0:def 7; B3 is bounded by A83,Def2; hence contradiction by A36,A51,A49,A86,A87,A89,CONNSP_1:36,RLTOPSP1:42; end; end; hence thesis; end; end; hence thesis; end; suppose n<1; then n<0+1; then A90: n=0 by NAT_1:13; for q2 being Point of TOP-REAL n holds |.q2.|<1 proof let q2 be Point of TOP-REAL n; q2=0.TOP-REAL n by A90,EUCLID:77; hence thesis by TOPRNS_1:23; 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 Th34; hence thesis by RLTOPSP1:42; end; end; theorem Th107: for G being non empty TopSpace,A,B,C,D being Subset of G st B is a_component & C is a_component & A \/ B=the carrier of G & C misses A holds C=B proof let G be non empty TopSpace,A,B,C,D be Subset of G; assume that A1: B is a_component and A2: C is a_component and A3: A \/ B=the carrier of G and A4: C misses A; now C /\ (the carrier of G)=C by XBOOLE_1:28; then A5: C /\ A \/ C /\ B=C by A3,XBOOLE_1:23; assume C misses B; then A6: C /\ B = {} by XBOOLE_0:def 7; C <> {}G by A2,CONNSP_1:32; hence contradiction by A4,A6,A5,XBOOLE_0:def 7; end; hence thesis by A1,A2,CONNSP_1:35; end; theorem Th108: for A being Subset of TOP-REAL 2 st A is bounded & A is Jordan holds BDD A is_inside_component_of A proof let A be Subset of TOP-REAL 2; assume that A1: A is bounded and A2: A is Jordan; reconsider D=A` as non empty Subset of TOP-REAL 2 by A2,JORDAN1:def 2; consider A1,A2 being Subset of TOP-REAL 2 such that A3: A` = A1 \/ A2 and A4: A1 misses A2 and (Cl A1) \ A1 = (Cl A2) \ A2 and A5: for C1,C2 being Subset of (TOP-REAL 2) | A` st C1 = A1 & C2 = A2 holds C1 is a_component & C2 is a_component by A2,JORDAN1:def 2; A6: UBD A is_outside_component_of A by A1,Th68; then UBD A is_a_component_of A` by Def3; then consider B1 being Subset of (TOP-REAL 2) | A` such that A7: B1 = UBD A and A8: B1 is a_component by CONNSP_1:def 6; A9: Down(A1,A`)=A1 by A3,XBOOLE_1:21; A10: Down(A2,A`)=A2 by A3,XBOOLE_1:21; then A11: Down(A2,A`) is a_component by A5,A9; then A12: A2 is_a_component_of A` by A10,CONNSP_1:def 6; A13: (TOP-REAL 2) | D is non empty; then A14: Down(A2,A`)<>{}((TOP-REAL 2) | A`) by A11,CONNSP_1:32; A15: Down(A1,A`) is a_component by A5,A9,A10; then A16: A1 is_a_component_of A` by A9,CONNSP_1:def 6; per cases by A9,A15,A8,CONNSP_1:35; suppose A17: B1=A1; A18: now assume not BDD A c= A2; then consider x such that A19: x in BDD A and A20: not x in A2 by TARSKI:def 3; consider y such that A21: x in y and A22: y in {B3 where B3 is Subset of TOP-REAL 2: B3 is_inside_component_of A} by A19,TARSKI:def 4; consider B3 being Subset of TOP-REAL 2 such that A23: y=B3 and A24: B3 is_inside_component_of A by A22; A25: B3 is_a_component_of A` by A24,Def2; then consider B4 being Subset of (TOP-REAL 2) | A` such that A26: B4 = B3 and A27: B4 is a_component by CONNSP_1:def 6; A28: B3<>{}((TOP-REAL 2) | A`) by A13,A26,A27,CONNSP_1:32; now assume B4=Down(A1,A`); then UBD A is bounded by A9,A7,A17,A24,A26,Def2; hence contradiction by A6,Def3; end; then A29: B3 misses A1 by A9,A15,A26,A27,CONNSP_1:35; B4=Down(A2,A`) or B4 misses Down(A2,A`) by A11,A27,CONNSP_1:35; then A30: B4=Down(A2,A`) or B4 /\ Down(A2,A`)={}((TOP-REAL 2) | A`) by XBOOLE_0:def 7; B3=B3 /\ (A1 \/ A2) by A3,A25,SPRECT_1:5,XBOOLE_1:28 .=(B3 /\ A1) \/ (B3 /\ A2 ) by XBOOLE_1:23 .={} by A10,A20,A21,A23,A26,A30,A29,XBOOLE_0:def 7; hence contradiction by A28; end; now assume not A2 is bounded; then A2 is_outside_component_of A by A12,Def3; then A2 /\ UBD A <> {} by A10,A14,Th23,XBOOLE_1:28; hence contradiction by A4,A7,A17,XBOOLE_0:def 7; end; then A31: A2 is_inside_component_of A by A12,Def2; then A2 c= BDD A by Th22; hence thesis by A31,A18,XBOOLE_0:def 10; end; suppose A32: B1 misses Down(A1,A`); set E1=Down(A1,A`), E2=Down(A2,A`); E1 \/ E2=[#]((TOP-REAL 2) | A`) by A3,A9,A10,PRE_TOPC:def 5; then A33: UBD A=A2 by A10,A11,A13,A7,A8,A32,Th107; A34: BDD A \/ UBD A=A` by Th27; A35: BDD A misses UBD A by Th24; A36: BDD A c= A1 proof let z; assume z in BDD A; then z in A` & not z in UBD A by A35,A34,XBOOLE_0:3,def 3; hence thesis by A3,A33,XBOOLE_0:def 3; end; A37: BDD A is bounded by A1,Th106; A1 c= BDD A proof let z; assume z in A1; then z in A` & not z in UBD A by A3,A4,A33,XBOOLE_0:3,def 3; hence thesis by A34,XBOOLE_0:def 3; end; then BDD A = A1 by A36,XBOOLE_0:def 10; hence thesis by A16,A37,Def2; end; end; theorem for a being Real,p being Point of TOP-REAL 2 st a>0 & p in (L~SpStSeq D) holds ex q being Point of TOP-REAL 2 st q in BDD (L~SpStSeq D) & |.p-q.|0 and A2: p in (L~SpStSeq D); set q1 = the Element of BDD (L~SpStSeq D); set A=L~SpStSeq D; A`<>{} by SPRECT_1:def 3; then consider A1,A2 being Subset of TOP-REAL 2 such that A3: A` = A1 \/ A2 and A1 misses A2 and A4: (Cl A1) \ A1 = (Cl A2) \ A2 and A5: A=(Cl A1) \ A1 and A6: for C1,C2 being Subset of (TOP-REAL 2) | A` st C1 = A1 & C2 = A2 holds C1 is a_component & C2 is a_component by Th98; A7: Down(A2,A`)=A2 by A3,XBOOLE_1:21; BDD A is_inside_component_of A by Th108; then BDD (L~SpStSeq D) is_a_component_of A` by Def2; then consider B1 being Subset of (TOP-REAL 2) | A` such that A8: B1 = BDD (L~SpStSeq D) and A9: B1 is a_component by CONNSP_1:def 6; B1 c= the carrier of (TOP-REAL 2) | A`; then A10: BDD (L~SpStSeq D) c= A1 \/ A2 by A3,A8,PRE_TOPC:8; A11: Down(A1,A`)=A1 by A3,XBOOLE_1:21; then A12: Down(A1,A`) is a_component by A6,A7; A13: Down(A2,A`) is a_component by A6,A11,A7; A14: BDD (L~SpStSeq D) <>{} by Th96; then A15: q1 in BDD (L~SpStSeq D); per cases by A10,A15,XBOOLE_0:def 3; suppose q1 in A1; then B1 /\ Down(A1,A`)<>{}((TOP-REAL 2) | A`) by A11,A8,A14,XBOOLE_0:def 4; then B1 meets Down(A1,A`) by XBOOLE_0:def 7; then B1=Down(A1,A`) by A12,A9,CONNSP_1:35; then A16: p in Cl(BDD (L~SpStSeq D)) by A2,A5,A11,A8,XBOOLE_0:def 5; reconsider ep=p as Point of Euclid 2 by TOPREAL3:8; reconsider G2=Ball(ep,a) as Subset of TOP-REAL 2 by TOPREAL3:8; (the distance of (Euclid 2)) is Reflexive by METRIC_1:def 6; then dist(ep,ep)=0 by METRIC_1:def 2; then A17: p in Ball(ep,a) by A1,METRIC_1:11; G2 is open by GOBOARD6:3; then (BDD (L~SpStSeq D)) meets G2 by A16,A17,PRE_TOPC:def 7; then consider t2 being set such that A18: t2 in (BDD (L~SpStSeq D)) and A19: t2 in G2 by XBOOLE_0:3; reconsider qt2=t2 as Point of TOP-REAL 2 by A18; |.p-qt2.|{}((TOP-REAL 2) | A`) by A7,A8,A14,XBOOLE_0:def 4; then B1 meets Down(A2,A`) by XBOOLE_0:def 7; then B1=Down(A2,A`) by A13,A9,CONNSP_1:35; then A20: p in Cl(BDD (L~SpStSeq D)) by A2,A4,A5,A7,A8,XBOOLE_0:def 5; reconsider ep=p as Point of Euclid 2 by TOPREAL3:8; reconsider G2=Ball(ep,a) as Subset of TOP-REAL 2 by TOPREAL3:8; (the distance of (Euclid 2)) is Reflexive by METRIC_1:def 6; then dist(ep,ep)=0 by METRIC_1:def 2; then A21: p in Ball(ep,a) by A1,METRIC_1:11; G2 is open by GOBOARD6:3; then (BDD (L~SpStSeq D)) meets G2 by A20,A21,PRE_TOPC:def 7; then consider t2 being set such that A22: t2 in (BDD (L~SpStSeq D)) and A23: t2 in G2 by XBOOLE_0:3; reconsider qt2=t2 as Point of TOP-REAL 2 by A22; |.p-qt2.| E-bound ( L~f) holds p in LeftComp f proof let p be Point of TOP-REAL 2; assume that A1: f/.1 = N-min L~f and A2: p`1> E-bound(L~f); set g=SpStSeq L~f; A3: LeftComp g c= LeftComp f by A1,SPRECT_3:41; E-bound L~ g=E-bound L~f by SPRECT_1:61; then p in LeftComp g by A2,SPRECT_3:40; hence thesis by A3; end; theorem for p being Point of TOP-REAL 2 st f/.1 = N-min L~f & p`2 < S-bound ( L~f) holds p in LeftComp f proof let p be Point of TOP-REAL 2; assume that A1: f/.1 = N-min L~f and A2: p`2< S-bound(L~f); set g=SpStSeq L~f; A3: LeftComp g c= LeftComp f by A1,SPRECT_3:41; S-bound L~ g=S-bound L~f by SPRECT_1:59; then p in LeftComp g by A2,SPRECT_3:40; hence thesis by A3; end; theorem for p being Point of TOP-REAL 2 st f/.1 = N-min L~f & p`2 > N-bound ( L~f) holds p in LeftComp f proof let p be Point of TOP-REAL 2; assume that A1: f/.1 = N-min L~f and A2: p`2>N-bound(L~f); set g=SpStSeq L~f; A3: LeftComp g c= LeftComp f by A1,SPRECT_3:41; N-bound L~ g=N-bound L~f by SPRECT_1:60; then p in LeftComp g by A2,SPRECT_3:40; hence thesis by A3; end; :: Moved from GOBRD14, AK, 22.02.2006 theorem for T being TopSpace, A being Subset of T, B being Subset of T st B is_a_component_of A holds B is connected proof let T be TopSpace, A be Subset of T, B be Subset of T; assume B is_a_component_of A; then consider C being Subset of T|A such that A1: C = B and A2: C is a_component by CONNSP_1:def 6; C is connected by A2,CONNSP_1:def 5; hence thesis by A1,CONNSP_1:23; end; theorem for A being Subset of TOP-REAL n, B being Subset of TOP-REAL n st B is_inside_component_of A holds B is connected proof let A be Subset of TOP-REAL n, B be Subset of TOP-REAL n; assume B is_inside_component_of A; then consider C being Subset of (TOP-REAL n) | A` such that A1: C = B and A2: C is a_component and C is bounded Subset of Euclid n by Th13; C is connected by A2,CONNSP_1:def 5; hence thesis by A1,CONNSP_1:23; end; theorem Th116: for A being Subset of TOP-REAL n, B being Subset of TOP-REAL n st B is_outside_component_of A holds B is connected proof let A be Subset of TOP-REAL n, B be Subset of TOP-REAL n; assume B is_outside_component_of A; then consider C being Subset of (TOP-REAL n) | A` such that A1: C = B and A2: C is a_component and not C is bounded Subset of Euclid n by Th14; C is connected by A2,CONNSP_1:def 5; hence thesis by A1,CONNSP_1:23; end; theorem for A being Subset of TOP-REAL n, B being Subset of TOP-REAL n st B is_a_component_of A` holds A misses B proof let A be Subset of TOP-REAL n, B be Subset of TOP-REAL n; assume B is_a_component_of A`; then B c= A` by SPRECT_1:5; then A misses B by SUBSET_1:23; hence A /\ B = {} by XBOOLE_0:def 7; end; theorem P is_outside_component_of Q & R is_inside_component_of Q implies P misses R proof assume A1: P is_outside_component_of Q; assume A2: R is_inside_component_of Q; (BDD Q) misses (UBD Q) by Th24; then P misses BDD Q by A1,Th23,XBOOLE_1:63; hence thesis by A2,Th22,XBOOLE_1:63; end; theorem 2 <= n implies for A, B, P being Subset of TOP-REAL n st P is bounded & A is_outside_component_of P & B is_outside_component_of P holds A = B proof assume A1: 2 <= n; let A, B, P be Subset of TOP-REAL n such that A2: P is bounded and A3: A is_outside_component_of P and A4: B is_outside_component_of P; A5: B is_a_component_of P` by A4,Def3; UBD P is_outside_component_of P by A1,A2,Th68; then A6: UBD P is_a_component_of P` by Def3; A7: P` is non empty by A1,A2,Th66,XXREAL_0:2; A8: B <> {} by A4,Def3; A9: B c= UBD P by A4,Th23; A10: A c= UBD P by A3,Th23; A11: A is_a_component_of P` by A3,Def3; then A <> {} by A7,SPRECT_1:4; then A = UBD P by A11,A6,A10,GOBOARD9:1,XBOOLE_1:69; hence thesis by A5,A8,A6,A9,GOBOARD9:1,XBOOLE_1:69; end; registration let C be closed Subset of TOP-REAL 2; cluster BDD C -> open; coherence proof set F = {B where B is Subset of TOP-REAL 2: B is_inside_component_of C}; F c= bool the carrier of TOP-REAL 2 proof let f be set; assume f in F; then ex B being Subset of TOP-REAL 2 st f = B & B is_inside_component_of C; hence thesis; end; then reconsider F as Subset-Family of TOP-REAL 2; F is open proof let P be Subset of TOP-REAL 2; assume P in F; then consider B being Subset of TOP-REAL 2 such that A1: P = B and A2: B is_inside_component_of C; B is_a_component_of C` by A2,Def2; hence thesis by A1,SPRECT_3:8; end; hence thesis by TOPS_2:19; end; cluster UBD C -> open; coherence proof set F = {B where B is Subset of TOP-REAL 2: B is_outside_component_of C}; F c= bool the carrier of TOP-REAL 2 proof let f be set; assume f in F; then ex B being Subset of TOP-REAL 2 st f = B & B is_outside_component_of C; hence thesis; end; then reconsider F as Subset-Family of TOP-REAL 2; F is open proof let P be Subset of TOP-REAL 2; assume P in F; then consider B being Subset of TOP-REAL 2 such that A3: P = B and A4: B is_outside_component_of C; B is_a_component_of C` by A4,Def3; hence thesis by A3,SPRECT_3:8; end; hence thesis by TOPS_2:19; end; end; registration let C be compact Subset of TOP-REAL 2; cluster UBD C -> connected; coherence by Th68,Th116; end; :: Moved from JORDAN1C, AK, 22.02.2006 reserve p for Point of TOP-REAL 2; theorem Th120: west_halfline p is non bounded proof set Wp = west_halfline p; set p11 = p`1, p12 = p`2; assume Wp is bounded; then reconsider C = Wp as bounded Subset of Euclid 2 by Th11; consider r being Real such that A1: 0 < r and A2: for x,y being Point of Euclid 2 st x in C & y in C holds dist(x,y) <= r by TBSP_1:def 7; set EX1 = p`1-2*r; reconsider p1 = p, EX = |[p`1-2*r, p`2]| as Point of Euclid 2 by EUCLID:67; 0 + p`1 <= 2*r + p`1 by A1,XREAL_1:6; then p`1 - 2*r <= p`1 by XREAL_1:20; then A3: |[p`1-2*r, p`2]|`1 <= p`1 by EUCLID:52; then A4: p1 in Wp by TOPREAL1:def 13; |[p`1-2*r, p`2]|`2 = p`2 by EUCLID:52; then A5: EX in Wp by A3,TOPREAL1:def 13; p = |[p11,p12]| by EUCLID:53; then dist (p1, EX) = sqrt ((p11 - EX1)^2 + (p12 - p`2)^2) by GOBOARD6:6 .= 2*r by A1,SQUARE_1:22; hence thesis by A1,A2,A5,A4,XREAL_1:155; end; theorem Th121: east_halfline p is non bounded proof set Wp = east_halfline p; set p11 = p`1, p12 = p`2; assume Wp is bounded; then reconsider C = Wp as bounded Subset of Euclid 2 by Th11; consider r being Real such that A1: 0 < r and A2: for x,y being Point of Euclid 2 st x in C & y in C holds dist(x,y) <= r by TBSP_1:def 7; set EX1 = p`1+2*r, EX2 = p`2; reconsider p1 = p, EX = |[p`1+2*r, p`2]| as Point of Euclid 2 by EUCLID:67; 0 + p`1 <= 2*r + p`1 by A1,XREAL_1:6; then A3: |[EX1, p`2]|`1 >= p`1 by EUCLID:52; then A4: p1 in Wp by TOPREAL1:def 11; |[EX1, p`2]|`2 = p`2 by EUCLID:52; then A5: EX in Wp by A3,TOPREAL1:def 11; p = |[p11,p12]| by EUCLID:53; then dist (p1, EX) = sqrt ((p11 - EX1)^2 + (p12 - EX2)^2) by GOBOARD6:6 .= sqrt ((EX1 - p11)^2 + 0) .= 2*r by A1,SQUARE_1:22; hence thesis by A1,A2,A5,A4,XREAL_1:155; end; theorem Th122: north_halfline p is non bounded proof set Wp = north_halfline p; set p11 = p`1, p12 = p`2; assume Wp is bounded; then reconsider C = Wp as bounded Subset of Euclid 2 by Th11; consider r being Real such that A1: 0 < r and A2: for x,y being Point of Euclid 2 st x in C & y in C holds dist(x,y) <= r by TBSP_1:def 7; set EX2 = p`2+2*r, EX1 = p`1; reconsider p1 = p, EX = |[p`1, p`2+2*r]| as Point of Euclid 2 by EUCLID:67; A3: |[p`1, EX2]|`1 = p`1 by EUCLID:52; then A4: p1 in Wp by TOPREAL1:def 10; 0 + p`2 <= 2*r + p`2 by A1,XREAL_1:6; then |[p`1, EX2]|`2 >= p`2 by EUCLID:52; then A5: EX in Wp by A3,TOPREAL1:def 10; p = |[p11,p12]| by EUCLID:53; then dist (p1, EX) = sqrt ((p11 - EX1)^2 + (p12 - EX2)^2) by GOBOARD6:6 .= sqrt ((EX2 - p12)^2 + 0) .= 2*r by A1,SQUARE_1:22; hence thesis by A1,A2,A5,A4,XREAL_1:155; end; theorem Th123: south_halfline p is non bounded proof set Wp = south_halfline p; set p11 = p`1, p12 = p`2; assume Wp is bounded; then reconsider C = Wp as bounded Subset of Euclid 2 by Th11; consider r being Real such that A1: 0 < r and A2: for x,y being Point of Euclid 2 st x in C & y in C holds dist(x,y) <= r by TBSP_1:def 7; set EX2 = p`2-2*r, EX1 = p`1; reconsider p1 = p, EX = |[p`1, p`2-2*r]| as Point of Euclid 2 by EUCLID:67; p = |[p11,p12]| by EUCLID:53; then A3: dist (p1, EX) = sqrt ((p11 - EX1)^2 + (p12 - EX2)^2) by GOBOARD6:6 .= 2*r by A1,SQUARE_1:22; A4: |[p`1, EX2]|`1 = p`1 by EUCLID:52; then A5: p1 in Wp by TOPREAL1:def 12; 0 + p`2 <= 2*r + p`2 by A1,XREAL_1:6; then p`2 - 2*r <= p`2 by XREAL_1:20; then |[p`1, EX2]|`2 <= p`2 by EUCLID:52; then EX in Wp by A4,TOPREAL1:def 12; hence thesis by A1,A2,A5,A3,XREAL_1:155; end; registration let C be compact Subset of TOP-REAL 2; cluster UBD C -> non empty; coherence proof A1: UBD C is_outside_component_of C by Th68; thus thesis by A1,Def3; end; end; theorem Th124: for C being compact Subset of TOP-REAL 2 holds UBD C is_a_component_of C` proof let C be compact Subset of TOP-REAL 2; UBD C is_outside_component_of C by Th68; hence thesis by Def3; end; theorem Th125: for C being compact Subset of TOP-REAL 2 for WH being connected Subset of TOP-REAL 2 st WH is non bounded & WH misses C holds WH c= UBD C proof let C be compact Subset of TOP-REAL 2; let WH be connected Subset of TOP-REAL 2; assume that A1: WH is non bounded and A2: WH misses C; A3: WH meets UBD C proof (BDD C) \/ (UBD C) = C` & [#]the carrier of TOP-REAL 2 = C \/ C` by Th27, SUBSET_1:10; then A4: WH c= (UBD C) \/ BDD C by A2,XBOOLE_1:73; assume A5: WH misses UBD C; BDD C is bounded by Th106; hence thesis by A1,A5,A4,RLTOPSP1:42,XBOOLE_1:73; end; WH c= C` by A2,SUBSET_1:23; hence thesis by A3,Th124,GOBOARD9:4; end; theorem for C being compact Subset of TOP-REAL 2 for p being Point of TOP-REAL 2 st west_halfline p misses C holds west_halfline p c= UBD C proof let C be compact Subset of TOP-REAL 2; let p be Point of TOP-REAL 2; set WH = west_halfline p; assume A1: WH misses C; WH is non bounded non empty connected by Th120; hence thesis by A1,Th125; end; theorem for C being compact Subset of TOP-REAL 2 for p being Point of TOP-REAL 2 st east_halfline p misses C holds east_halfline p c= UBD C proof let C be compact Subset of TOP-REAL 2; let p be Point of TOP-REAL 2; set WH = east_halfline p; assume A1: WH misses C; WH is non bounded non empty connected by Th121; hence thesis by A1,Th125; end; theorem for C being compact Subset of TOP-REAL 2 for p being Point of TOP-REAL 2 st south_halfline p misses C holds south_halfline p c= UBD C proof let C be compact Subset of TOP-REAL 2; let p be Point of TOP-REAL 2; set WH = south_halfline p; assume A1: WH misses C; WH is non bounded non empty connected by Th123; hence thesis by A1,Th125; end; theorem for C being compact Subset of TOP-REAL 2 for p being Point of TOP-REAL 2 st north_halfline p misses C holds north_halfline p c= UBD C proof let C be compact Subset of TOP-REAL 2; let p be Point of TOP-REAL 2; set WH = north_halfline p; assume A1: WH misses C; WH is non bounded non empty connected by Th122; hence thesis by A1,Th125; end; theorem for n being Nat, r being Real st r > 0 for x,y,z being Element of Euclid n st x = 0*n for p being Element of TOP-REAL n st p = y & r*p = z holds r*dist(x,y) = dist(x,z) by Lm1; theorem for n being Nat, r,s being Real st r > 0 for x being Element of Euclid n st x = 0*n for A being Subset of TOP-REAL n st A = Ball(x,s) holds r*A = Ball(x,r*s) by Lm2; theorem for n being Nat, r,s,t be Real st 0 < s & s <= t for x being Element of Euclid n st x = 0*n for BA being Subset of TOP-REAL n st BA = Ball(x,r) holds s*BA c= t*BA by Lm3;