### Compactness of the Bounded Closed Subsets of $\cal E^2_\rm T$

by
Artur Kornilowicz

Copyright (c) 1999 Association of Mizar Users

MML identifier: TOPREAL6
[ MML identifier index ]

environ

vocabulary ARYTM, METRIC_1, PRE_TOPC, EUCLID, SQUARE_1, ARYTM_1, ARYTM_3,
RELAT_1, ABSVALUE, FINSEQ_2, FINSEQ_1, FUNCT_1, GROUP_1, RVSUM_1,
RCOMP_1, ORDINAL2, SEQ_2, LATTICES, FINSET_1, PCOMPS_1, RELAT_2,
SUBSET_1, BOOLE, CONNSP_1, COMPTS_1, T_0TOPSP, TOPS_2, SETFAM_1, TARSKI,
CARD_3, FUNCOP_1, CAT_1, COMPLEX1, RLVECT_1, MCART_1, TOPREAL1, PSCOMP_1,
JORDAN1, SPPOL_1, TOPREAL4, TOPREAL2, SPRECT_1, FUNCT_5, JORDAN2C, SEQ_1,
TOPMETR, CONNSP_2, TOPS_1, BORSUK_1, PARTFUN1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
FUNCT_3, BINOP_1, FINSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1,
SQUARE_1, NAT_1, ABSVALUE, BINARITH, CQC_LANG, FUNCT_4, SEQ_1, SEQ_2,
SEQ_4, STRUCT_0, GROUP_1, METRIC_1, TBSP_1, FINSEQ_1, FINSEQ_2, RVSUM_1,
NEWTON, CARD_3, FINSEQ_4, RCOMP_1, PRE_TOPC, TOPS_1, TOPS_2, CONNSP_1,
CONNSP_2, COMPTS_1, BORSUK_1, PCOMPS_1, EUCLID, WEIERSTR, TOPMETR,
TOPREAL1, TOPREAL2, T_0TOPSP, JORDAN1, TOPREAL4, PSCOMP_1, SPPOL_1,
JGRAPH_1, SPRECT_1, JORDAN2C;
constructors BINARITH, BORSUK_3, CARD_4, COMPTS_1, CONNSP_1, FINSEQOP,
FINSEQ_4, GOBOARD9, JORDAN1, JORDAN2C, LIMFUNC1, PSCOMP_1, RCOMP_1,
REAL_1, REALSET1, SPPOL_1, SPRECT_1, TBSP_1, TOPGRP_1, TOPREAL2,
TOPREAL4, TOPS_1, TOPS_2, WAYBEL_3, WEIERSTR, CQC_LANG, TOPRNS_1,
MEMBERED, PARTFUN1;
clusters SUBSET_1, XREAL_0, BORSUK_1, BORSUK_3, FUNCT_4, EUCLID, FINSET_1,
GOBOARD9, METRIC_1, PCOMPS_1, PRE_TOPC, PSCOMP_1, RCOMP_1, RELSET_1,
SPRECT_1, SPRECT_2, STRUCT_0, TEX_4, TOPGRP_1, TOPMETR, TOPS_1, WAYBEL_2,
WAYBEL12, YELLOW13, ARYTM_3, SQUARE_1, FINSEQ_5, MEMBERED, ZFMISC_1,
NUMBERS, ORDINAL2;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, FUNCT_1, PRE_TOPC, TOPS_2, CONNSP_1, CONNSP_2, BORSUK_1,
GROUP_1, JORDAN1, JORDAN2C, SEQ_4, METRIC_6, PSCOMP_1, SPPOL_1, T_0TOPSP,
TOPREAL2, XBOOLE_0;
theorems ABSVALUE, AXIOMS, BORSUK_1, BORSUK_3, CARD_3, FUNCT_4, CATALG_1,
COMPTS_1, CONNSP_1, CONNSP_2, EUCLID, FINSEQ_1, FINSEQ_2, FINSEQ_3,
FUNCT_1, FUNCT_2, FUNCT_3, GOBOARD6, GOBOARD7, GOBOARD9, GROUP_7, HEINE,
JGRAPH_1, JORDAN1, JORDAN2C, JORDAN3, JORDAN4, JORDAN5A, JORDAN6,
METRIC_1, METRIC_6, NEWTON, NAT_1, PCOMPS_1, PRE_TOPC, PREPOWER,
PSCOMP_1, RCOMP_1, REAL_1, REAL_2, RELAT_1, RVSUM_1, SEQ_2, SEQ_4,
SPPOL_1, SPRECT_1, SQUARE_1, SUBSET_1, TARSKI, TBSP_1, TOPMETR, TOPREAL1,
TOPREAL3, TOPREAL4, TOPS_1, TOPS_2, WEIERSTR, YELLOW12, ZFMISC_1,
XREAL_0, AMI_1, CQC_LANG, TOPREAL5, SETFAM_1, XBOOLE_0, XBOOLE_1,
XCMPLX_0, XCMPLX_1;
schemes FINSET_1, NAT_1, FUNCT_2;

begin  :: Real numbers

reserve a, b for real number,
r for Real,
i, j, n for Nat,
M for non empty MetrSpace,
p, q, s for Point of TOP-REAL 2,
e for Point of Euclid 2,
w for Point of Euclid n,
z for Point of M,
A, B for Subset of TOP-REAL n,
P for Subset of TOP-REAL 2,
D for non empty Subset of TOP-REAL 2;

Lm1: sqrt 2 > 0 by AXIOMS:22,SQUARE_1:84;

Lm2: Euclid 2 = MetrStruct(#REAL 2,Pitag_dist 2#) by EUCLID:def 7;

canceled 5;

theorem Th6:
0 <= a & 0 <= b implies sqrt(a+b) <= sqrt a + sqrt b
proof
assume
A1:   0 <= a & 0 <= b;
then A2: 0 + 0 <= a + b by REAL_1:55;
0 <= sqrt a & 0 <= sqrt b by A1,SQUARE_1:def 4;
then A3: 0 + 0 <= sqrt a + sqrt b by REAL_1:55;
A4: sqrt(a + 2*sqrt a*sqrt b + b)
= sqrt((sqrt a)^2 + 2*sqrt a*sqrt b + b) by A1,SQUARE_1:def 4
.= sqrt((sqrt a)^2 + 2*sqrt a*sqrt b + (sqrt b)^2) by A1,SQUARE_1:def 4
.= sqrt((sqrt a + sqrt b)^2) by SQUARE_1:63
.= sqrt a + sqrt b by A3,SQUARE_1:89;
0 <= a*b by A1,REAL_2:121;
then 0 <= sqrt(a*b) by SQUARE_1:def 4;
then 0 <= sqrt a*sqrt b by A1,SQUARE_1:97;
then 0 <= 2*(sqrt a*sqrt b) by REAL_2:121;
then 0 <= 2*sqrt a*sqrt b by XCMPLX_1:4;
then a + 0 <= a + 2*sqrt a*sqrt b by AXIOMS:24;
then a + b <= a + 2*sqrt a*sqrt b + b by AXIOMS:24;
hence thesis by A2,A4,SQUARE_1:94;
end;

theorem Th7:
0 <= a & a <= b implies abs(a) <= abs(b)
proof
assume
A1:   0 <= a & a <= b;
then abs(a) = a & abs(b) = b by ABSVALUE:def 1;
hence abs(a) <= abs(b) by A1;
end;

theorem Th8:
b <= a & a <= 0 implies abs(a) <= abs(b)
proof
assume that
A1:   b <= a and
A2:   a <= 0;
per cases by A2;
suppose a = 0;
then abs(a) = 0 by ABSVALUE:7;
hence thesis by ABSVALUE:5;
suppose
A3:   a < 0;
then b < 0 by A1;
then abs(a) = -a & abs(b) = -b by A3,ABSVALUE:def 1;
hence abs(a) <= abs(b) by A1,REAL_1:50;
end;

theorem
Product(0|->r) = 1 by FINSEQ_2:72,RVSUM_1:124;

theorem Th10:
Product(1|->r) = r
proof
thus Product(1|->r) = Product<*r*> by FINSEQ_2:73
.= r by RVSUM_1:125;
end;

theorem
Product(2|->r) = r * r
proof
thus Product(2|->r) = Product<*r,r*> by FINSEQ_2:75
.= r * r by RVSUM_1:129;
end;

theorem Th12:
Product((n+1)|->r) = (Product(n|->r))*r
proof
thus Product((n+1)|->r) = (Product(n|->r))*(Product(1|->r)) by RVSUM_1:134
.= (Product(n|->r))*r by Th10;
end;

theorem Th13:
j <> 0 & r = 0 iff Product(j|->r) = 0
proof
set f = j|->r;
A1: dom f = Seg j by FINSEQ_2:68;
hereby
assume that
A2:     j <> 0 and
A3:     r = 0;
consider n such that
A4:     j = n + 1 by A2,NAT_1:22;
1 <= j by A4,NAT_1:29;
then A5:   1 in Seg j by FINSEQ_1:3;
then f.1 = 0 by A3,FINSEQ_2:70;
hence Product f = 0 by A1,A5,RVSUM_1:133;
end;
assume Product f = 0;
then consider n such that
A6:   n in dom f & f.n = 0 by RVSUM_1:133;
thus thesis by A1,A6,FINSEQ_1:4,FINSEQ_2:70;
end;

theorem Th14:
r <> 0 & j <= i implies Product((i-'j)|->r) = Product(i|->r) / Product(j|->r)
proof
assume that
A1:   r <> 0 and
A2:   j <= i;
A3: Product(j|->r) <> 0 by A1,Th13;
defpred P[Nat] means j <= $1 implies Product(($1-'j)|->r) =
Product($1|->r) / Product(j|->r); A4: P[0] proof assume j <= 0; then A5: j = 0 by NAT_1:19; hence Product((0-'j)|->r) = Product(0|->r) / Product<*>REAL by JORDAN3:2,RVSUM_1:124 .= Product(0|->r) / Product(j|->r) by A5,FINSEQ_2:72; end; A6: for n being Nat st P[n] holds P[n+1] proof let n be Nat; assume that A7: P[n] and A8: j <= n+1; per cases by A8,NAT_1:26; suppose A9: j <= n; Product((n-'j+1)|->r) = Product((n-'j)|->r)*Product(1|->r) by RVSUM_1: 134 .= Product(n|->r) / Product(j|->r) * r by A7,A9,Th10 .= Product(n|->r) * r / Product(j|->r) by XCMPLX_1:75 .= Product((n+1)|->r) / Product(j|->r) by Th12; hence Product(((n+1)-'j)|->r) = Product((n+1)|->r) / Product(j|->r) by A9,JORDAN4:3; suppose A10: j = n+1; hence Product(((n+1)-'j)|->r) = Product(0|->r) by GOBOARD9:1 .= 1 by FINSEQ_2:72,RVSUM_1:124 .= Product((n+1)|->r) / Product(j|->r) by A3,A10,XCMPLX_1:60; end; for n being Nat holds P[n] from Ind(A4,A6); hence thesis by A2; end; theorem r <> 0 & j <= i implies r|^(i-'j) = r|^i / r|^j proof assume A1: r <> 0 & j <= i; thus r|^i / r|^j = (Product(i |-> r)) / r|^j by NEWTON:def 1 .= (Product(i |-> r)) / (Product(j |-> r)) by NEWTON:def 1 .= Product((i-'j) |-> r) by A1,Th14 .= r|^(i-'j) by NEWTON:def 1; end; reserve a, b for Real; theorem Th16: sqr <*a,b*> = <*a^2,b^2*> proof dom sqrreal = REAL by FUNCT_2:def 1; then A1: rng <*a,b*> c= dom sqrreal by FINSEQ_1:def 4; A2: dom sqr <*a,b*> = dom (sqrreal*<*a,b*>) by RVSUM_1:def 8 .= dom <*a,b*> by A1,RELAT_1:46 .= {1,2} by FINSEQ_1:4,FINSEQ_3:29; A3: dom <*a^2,b^2*> = {1,2} by FINSEQ_1:4,FINSEQ_3:29; for i being set st i in dom <*a^2,b^2*> holds (sqr <*a,b*>).i = <*a^2,b^2 *>.i proof let i be set; assume A4: i in dom <*a^2,b^2*>; A5: <*a,b*>.1 = a & <*a,b*>.2 = b by FINSEQ_1:61; per cases by A3,A4,TARSKI:def 2; suppose A6: i = 1; hence (sqr <*a,b*>).i = a^2 by A5,RVSUM_1:78 .= <*a^2,b^2*>.i by A6,FINSEQ_1:61; suppose A7: i = 2; hence (sqr <*a,b*>).i = b^2 by A5,RVSUM_1:78 .= <*a^2,b^2*>.i by A7,FINSEQ_1:61; end; hence thesis by A2,A3,FUNCT_1:9; end; theorem Th17: for F being FinSequence of REAL st i in dom abs F & a = F.i holds (abs F).i = abs(a) proof let F be FinSequence of REAL such that A1: i in dom abs F and A2: a = F.i; abs F = absreal*F & i in dom abs F by A1,EUCLID:def 3; then (abs F).i = absreal.a by A2,FUNCT_1:22; hence thesis by EUCLID:def 2; end; theorem abs <*a,b*> = <*abs(a),abs(b)*> proof dom absreal = REAL by FUNCT_2:def 1; then A1: rng <*a,b*> c= dom absreal by FINSEQ_1:def 4; A2: dom abs <*a,b*> = dom (absreal*<*a,b*>) by EUCLID:def 3 .= dom <*a,b*> by A1,RELAT_1:46 .= {1,2} by FINSEQ_1:4,FINSEQ_3:29; A3: dom <*abs(a),abs(b)*> = {1,2} by FINSEQ_1:4,FINSEQ_3:29; for i being set st i in dom <*abs(a),abs(b)*> holds (abs <*a,b*>).i = <*abs(a),abs(b)*>.i proof let i be set; assume A4: i in dom <*abs(a),abs(b)*>; A5: <*a,b*>.1 = a & <*a,b*>.2 = b by FINSEQ_1:61; A6: 1 in {1,2} & 2 in {1,2} by TARSKI:def 2; per cases by A3,A4,TARSKI:def 2; suppose A7: i = 1; hence (abs <*a,b*>).i = abs(a) by A2,A5,A6,Th17 .= <*abs(a),abs(b)*>.i by A7,FINSEQ_1:61; suppose A8: i = 2; hence (abs <*a,b*>).i = abs(b) by A2,A5,A6,Th17 .= <*abs(a),abs(b)*>.i by A8,FINSEQ_1:61; end; hence thesis by A2,A3,FUNCT_1:9; end; theorem for a, b, c, d being real number st a <= b & c <= d holds abs(b-a) + abs(d-c) = (b-a) + (d-c) proof let a, b, c, d be real number; assume a <= b & c <= d; then a - a <= b - a & c - c <= d - c by REAL_1:92; then 0 <= b - a & 0 <= d - c by XCMPLX_1:14; then abs(b-a) = b - a & abs(d-c) = d - c by ABSVALUE:def 1; hence thesis; end; theorem Th20: for a, r being real number holds r > 0 implies a in ].a-r,a+r.[ proof let a, r be real number; assume A1: r > 0; abs(a-a) = abs(0) by XCMPLX_1:14; then abs(a-a) < r by A1,ABSVALUE:def 1; hence thesis by RCOMP_1:8; end; theorem for a, r being real number holds r >= 0 implies a in [.a-r,a+r.] proof let a, r be real number; assume A1: r >= 0; reconsider a, r as Real by XREAL_0:def 1; A2: [.a-r,a+r.] = {b : a-r <= b & b <= a+r} by RCOMP_1:def 1; a-r <= a-0 & a+0 <= a+r by A1,REAL_1:55,92; hence thesis by A2; end; theorem Th22: for a, b being real number holds a < b implies inf ].a,b.[ = a & sup ].a,b.[ = b proof let a, b be real number; assume A1: a < b; set X = ].a,b.[; reconsider a, b as Real by XREAL_0:def 1; A2: ex p being real number st for r being real number st r in X holds p <= r proof take a; let r be real number; assume r in X; then r in { l where l is Real : a < l & l < b } by RCOMP_1:def 2; then consider r1 being Real such that A3: r1 = r & a < r1 & r1 < b; thus thesis by A3; end; A4: ex p be real number st for r being real number st r in X holds p >= r proof take b; let r be real number; assume r in X; then r in { l where l is Real : a < l & l < b } by RCOMP_1:def 2; then consider r1 being Real such that A5: r1 = r & a < r1 & r1 < b; thus thesis by A5; end; A6:a < (a+b)/2 & (a+b)/2 < b by A1,TOPREAL3:3; then A7: (a+b)/2 in { l where l is Real : a < l & l < b }; then A8: (a+b)/2 in X by RCOMP_1:def 2; then A9: (ex r being real number st r in X) & X is bounded_below by A2,SEQ_4: def 2; A10: (ex r being real number st r in X) & X is bounded_above by A4,A8,SEQ_4:def 1; A11:for r being real number st r in X holds a <= r proof let r be real number; assume r in X; then r in { l where l is Real : a < l & l < b } by RCOMP_1:def 2; then consider r1 being Real such that A12: r1 = r & a < r1 & r1 < b; thus thesis by A12; end; A13:for s being real number st 0 < s ex r being real number st r in X & r < a+s proof let s be real number such that A14: 0 < s and A15: for r being real number st r in X holds r >= a+s; reconsider s as Real by XREAL_0:def 1; per cases; suppose a + s >= b; then (a+b)/2 in X & (a+b)/2 < a+s by A6,A7,AXIOMS:22,RCOMP_1:def 2; hence thesis by A15; suppose A16: a + s < b; A17: a < a + s by A14,REAL_1:69; then A18: a < (a+(a+s))/2 by TOPREAL3:3; A19: (a+(a+s))/2 < a+s by A17,TOPREAL3:3; then (a+(a+s))/2 < b by A16,AXIOMS:22; then (a+(a+s))/2 in {r : a < r & r < b } by A18; then (a+(a+s))/2 in X by RCOMP_1:def 2; hence thesis by A15,A19; end; A20:for r being real number st r in X holds b >= r proof let r be real number; assume r in X; then r in { l where l is Real : a < l & l < b } by RCOMP_1:def 2; then consider r1 being Real such that A21: r1 = r & a < r1 & r1 < b; thus thesis by A21; end; for s being real number st 0 < s ex r being real number st r in X & b-s < r proof let s be real number such that A22: 0 < s and A23: for r being real number st r in X holds r <= b-s; reconsider s as Real by XREAL_0:def 1; per cases; suppose b - s <= a; then (a+b)/2 in X & (a+b)/2 > b-s by A6,A7,AXIOMS:22,RCOMP_1:def 2; hence thesis by A23; suppose A24: b - s > a; A25: b - s < b - 0 by A22,REAL_1:92; then b-s < (b+(b-s))/2 by TOPREAL3:3; then A26: a < (b+(b-s))/2 by A24,AXIOMS:22; A27: (b+(b-s))/2 > b-s by A25,TOPREAL3:3; (b+(b-s))/2 < b by A25,TOPREAL3:3; then (b+(b-s))/2 in {r : a < r & r < b } by A26; then (b+(b-s))/2 in X by RCOMP_1:def 2; hence thesis by A23,A27; end; hence thesis by A9,A10,A11,A13,A20,SEQ_4:def 4,def 5; end; canceled; theorem Th24: for A being bounded Subset of REAL holds A c= [.inf A,sup A.] proof let A be bounded Subset of REAL; let a be set; assume A1: a in A; then reconsider r = a as Real; inf A <= r & r <= sup A by A1,SEQ_4:def 4,def 5; hence a in [.inf A,sup A.] by TOPREAL5:1; end; begin :: Topological preliminaries definition let T be TopStruct, A be finite Subset of T; cluster T|A -> finite; coherence proof thus the carrier of T|A is finite by JORDAN1:1; end; end; definition cluster finite non empty strict TopSpace; existence proof take 1TopSp {0}; thus thesis; end; end; definition let T be TopStruct; cluster empty -> connected Subset of T; coherence proof let C be Subset of T; assume C is empty; then reconsider D = C as empty Subset of T; let A, B be Subset of T|C such that A1: [#](T|C) = A \/ B and A,B are_separated; [#](T|D) = {}; hence A = {}(T|C) or B = {}(T|C) by A1,XBOOLE_1:15; end; end; definition let T be TopSpace; cluster finite -> compact Subset of T; coherence proof let A be Subset of T; assume A is finite; then reconsider B = A as finite Subset of T; A1: T|B is compact; B = {} or B <> {}; hence thesis by A1,COMPTS_1:12; end; end; theorem Th25: for S, T being TopSpace st S, T are_homeomorphic & S is connected holds T is connected proof let S, T be TopSpace; given f being map of S,T such that A1: f is_homeomorphism; assume A2: S is connected; A3: f is continuous by A1,TOPS_2:def 5; dom f = [#]S & rng f = [#]T by A1,TOPS_2:def 5; then f.:[#]S = [#]T by RELAT_1:146; hence T is connected by A2,A3,CONNSP_1:15; end; theorem for T being TopSpace, F being finite Subset-Family of T st for X being Subset of T st X in F holds X is compact holds union F is compact proof let T be TopSpace, F be finite Subset-Family of T such that A1: for X being Subset of T st X in F holds X is compact; defpred P[set] means ex A being Subset of T st A = union$1 & A is compact;
A2: F is finite;
A3: P[{}]
proof
take {}T;
thus thesis by ZFMISC_1:2;
end;
A4: for x, B being set st x in F & B c= F & P[B] holds P[B \/ {x}]
proof
let x, B be set such that
A5:     x in F and
A6:     B c= F;
given A being Subset of T such that
A7:     A = union B and
A8:     A is compact;
reconsider X = x as Subset of T by A5;
B c= bool the carrier of T
proof
let b be set;
assume b in B;
then b in F by A6;
hence thesis;
end;
then B is Subset-Family of T by SETFAM_1:def 7;
then reconsider C = B as Subset-Family of T;
set K = union C \/ X;
take K;
union {x} = x by ZFMISC_1:31;
hence K = union (B \/ {x}) by ZFMISC_1:96;
X is compact by A1,A5;
hence K is compact by A7,A8,COMPTS_1:19;
end;
P[F] from Finite(A2,A3,A4);
hence thesis;
end;

begin

canceled 2;

theorem Th29:
for A, B, C, D, a, b being set st A c= B & C c= D holds
product ((a,b) --> (A,C)) c= product ((a,b) --> (B,D))
proof
let A, B, C, D, a, b be set such that
A1:   A c= B & C c= D;
set f = (a,b) --> (A,C),
g = (a,b) --> (B,D);
A2: dom f = {a,b} & dom g = {a,b} by FUNCT_4:65;
for x being set st x in dom f holds f.x c= g.x
proof
let x be set;
assume x in dom f;
then A3:   x = a or x = b by A2,TARSKI:def 2;
per cases;
suppose a <> b;
then f.a = A & f.b = C & g.a = B & g.b = D by FUNCT_4:66;
hence thesis by A1,A3;
suppose
A4:     a = b;
then f = a .--> C & g = a .--> D by AMI_1:20;
then f.a = C & f.b = C & g.b = D & g.b = D by A4,CQC_LANG:6;
hence thesis by A1,A3,A4;
end;
hence product f c= product g by A2,CARD_3:38;
end;

theorem Th30:
for A, B being Subset of REAL holds
product ((1,2) --> (A,B)) is Subset of TOP-REAL 2
proof
let A, B be Subset of REAL;
set f = (1,2) --> (A,B);
product f c= the carrier of TOP-REAL 2
proof
let a be set;
assume a in product f;
then consider g being Function such that
A1:     a = g and
A2:     dom g = dom f and
A3:     for x being set st x in dom f holds g.x in f.x by CARD_3:def 5;
A4:   dom f = {1,2} by FUNCT_4:65;
then A5:   1 in dom f & 2 in dom f by TARSKI:def 2;
f.1 = A & f.2 = B by FUNCT_4:66;
then g.1 in A & g.2 in B by A3,A5;
then reconsider m = g.1, n = g.2 as Real;
A6:   dom <*g.1,g.2*> = {1,2} by FINSEQ_1:4,FINSEQ_3:29;
now
let k be set;
assume k in dom g;
then k = 1 or k = 2 by A2,A4,TARSKI:def 2;
hence g.k = <*g.1,g.2*>.k by FINSEQ_1:61;
end;
then a = <*g.1,g.2*> by A1,A2,A4,A6,FUNCT_1:9;
then a = |[m,n]| by EUCLID:def 16;
hence thesis;
end;
hence thesis;
end;

theorem
|.|[0,a]|.| = abs(a) & |.|[a,0]|.| = abs(a)
proof
A1: <*0,a*> = |[0,a]| by EUCLID:def 16;
A2: <*a,0 *> = |[a,0]| by EUCLID:def 16;
A3: the carrier of TOP-REAL 2 = REAL 2 by EUCLID:25;
|.<*0,a*>.|
= sqrt Sum sqr <*0,a*> by EUCLID:def 5
.= sqrt Sum <*0^2,a^2*> by Th16
.= sqrt (0+a^2) by RVSUM_1:107,SQUARE_1:60
.= abs(a) by SQUARE_1:91;
hence |.|[0,a]|.| = abs(a) by A1,A3,JGRAPH_1:def 5;
|.<*a,0 *>.|
= sqrt Sum sqr <*a,0 *> by EUCLID:def 5
.= sqrt Sum <*a^2,0^2 *> by Th16
.= sqrt (a^2+0) by RVSUM_1:107,SQUARE_1:60
.= abs a by SQUARE_1:91;
hence thesis by A2,A3,JGRAPH_1:def 5;
end;

theorem Th32:
for p being Point of Euclid 2, q being Point of TOP-REAL 2 st
p = 0.REAL 2 & p = q holds q = <* 0,0 *> & q1 = 0 & q2 = 0
proof
let p be Point of Euclid 2,
q be Point of TOP-REAL 2 such that
A1:   p = 0.REAL 2 and
A2:   p = q;
A3: p = 0*2 by A1,EUCLID:def 9
.= 2 |-> (0 qua Real) by EUCLID:def 4
.= <*0,0 *> by FINSEQ_2:75;
then p = |[ 0,0 ]| by EUCLID:def 16;
hence thesis by A2,A3,EUCLID:56;
end;

theorem
for p, q being Point of Euclid 2, z being Point of TOP-REAL 2 st
p = 0.REAL 2 & q = z holds dist(p,q) = |.z.|
proof
let p, q be Point of Euclid 2,
z be Point of TOP-REAL 2 such that
A1:   p = 0.REAL 2 and
A2:   q = z;
reconsider P = p as Point of TOP-REAL 2 by TOPREAL3:13;
A3: P1 = 0 & P2 = 0 by A1,Th32;
dist(p,q) = (Pitag_dist 2).(p,q) by Lm2,METRIC_1:def 1
.= sqrt ((P1 - z1)^2 + (P2 - z2)^2) by A2,TOPREAL3:12
.= sqrt ((- z1)^2 + (P2 - z2)^2) by A3,XCMPLX_1:150
.= sqrt ((- z1)^2 + (- z2)^2) by A3,XCMPLX_1:150
.= sqrt ((z1)^2 + (- z2)^2) by SQUARE_1:61
.= sqrt ((z1)^2 + (z2)^2) by SQUARE_1:61;
hence dist(p,q) = |.z.| by JGRAPH_1:47;
end;

theorem Th34:
r*p = |[r*p1,r*p2]|
proof
p = |[p1,p2]| by EUCLID:57;
hence thesis by EUCLID:62;
end;

theorem Th35:
s = (1-r)*p + r*q & s <> p & 0 <= r implies 0 < r
proof
assume that
A1:   s = (1-r)*p + r*q and
A2:   s <> p and
A3:   0 <= r;
assume
A4:   r <= 0;
then s = (1-0)*p + r*q by A1,A3,REAL_1:def 5
.= (1-0)*p + 0 * q by A3,A4,REAL_1:def 5
.= 1 * p + 0.REAL 2 by EUCLID:33
.= 1 * p by EUCLID:31
.= p by EUCLID:33;
hence thesis by A2;
end;

theorem Th36:
s = (1-r)*p + r*q & s <> q & r <= 1 implies r < 1
proof
assume that
A1:   s = (1-r)*p + r*q and
A2:   s <> q and
A3:   r <= 1;
assume
A4:   r >= 1;
then s = (1-1)*p + r*q by A1,A3,REAL_1:def 5
.= 0 * p + 1 * q by A3,A4,REAL_1:def 5
.= 0.REAL 2 + 1 * q by EUCLID:33
.= 1 * q by EUCLID:31
.= q by EUCLID:33;
hence thesis by A2;
end;

theorem
s in LSeg(p,q) & s <> p & s <> q & p1 < q1 implies p1 < s1 & s1 < q1
proof
assume that
A1:   s in LSeg(p,q) and
A2:   s <> p & s <> q and
A3:   p1 < q1;
LSeg(p,q) = { (1-r)*p + r*q : 0 <= r & r <= 1 } by TOPREAL1:def 4;
then consider r such that
A4:   s = (1-r)*p + r*q and
A5:   0 <= r & r <= 1 by A1;
(1-r)*p = |[(1-r)*p1,(1-r)*p2]| & r*q = |[r*q1,r*q2]| by Th34;
then A6: ((1-r)*p)1 = (1-r)*p1 & (r*q)1 = r*q1 by EUCLID:56;
s = |[((1-r)*p)1 + (r*q)1,((1-r)*p)2 + (r*q)2]| by A4,EUCLID:59;
then A7: s1 = (1-r)*p1 + r*q1 by A6,EUCLID:56;
then A8: q1 - s1 = 1 * q1 - r*q1 - (1-r)*p1 by XCMPLX_1:36
.= (1-r)*q1 - (1-r)*p1 by XCMPLX_1:40
.= (1-r)*(q1-p1) by XCMPLX_1:40;
A9: p1 - s1 = 1 * p1 - (1-r)*p1 - r*q1 by A7,XCMPLX_1:36
.= (1-(1-r))*p1 - r*q1 by XCMPLX_1:40
.= (1-1+r)*p1 - r*q1 by XCMPLX_1:37
.= r*(p1-q1) by XCMPLX_1:40;
A10: q1-p1 > 0 & p1-q1 < 0 by A3,REAL_2:105,SQUARE_1:11;
r < 1 by A2,A4,A5,Th36;
then 1-r > 0 & r > 0 by A2,A4,A5,Th35,SQUARE_1:11;
then q1 - s1 > 0 & p1 - s1 < 0 by A8,A9,A10,REAL_2:129,SQUARE_1:24;
hence thesis by REAL_2:106,SQUARE_1:12;
end;

theorem
s in LSeg(p,q) & s <> p & s <> q & p2 < q2 implies p2 < s2 & s2 < q2
proof
assume that
A1:   s in LSeg(p,q) and
A2:   s <> p & s <> q and
A3:   p2 < q2;
LSeg(p,q) = { (1-r)*p + r*q : 0 <= r & r <= 1 } by TOPREAL1:def 4;
then consider r such that
A4:   s = (1-r)*p + r*q and
A5:   0 <= r & r <= 1 by A1;
(1-r)*p = |[(1-r)*p1,(1-r)*p2]| & r*q = |[r*q1,r*q2]| by Th34;
then A6: ((1-r)*p)2 = (1-r)*p2 & (r*q)2 = r*q2 by EUCLID:56;
s = |[((1-r)*p)1 + (r*q)1,((1-r)*p)2 + (r*q)2]| by A4,EUCLID:59;
then A7: s2 = (1-r)*p2 + r*q2 by A6,EUCLID:56;
then A8: q2 - s2 = 1 * q2 - r*q2 - (1-r)*p2 by XCMPLX_1:36
.= (1-r)*q2 - (1-r)*p2 by XCMPLX_1:40
.= (1-r)*(q2-p2) by XCMPLX_1:40;
A9: p2 - s2 = 1 * p2 - (1-r)*p2 - r*q2 by A7,XCMPLX_1:36
.= (1-(1-r))*p2 - r*q2 by XCMPLX_1:40
.= (1-1+r)*p2 - r*q2 by XCMPLX_1:37
.= r*(p2-q2) by XCMPLX_1:40;
A10: q2-p2 > 0 & p2-q2 < 0 by A3,REAL_2:105,SQUARE_1:11;
r < 1 by A2,A4,A5,Th36;
then 1-r > 0 & r > 0 by A2,A4,A5,Th35,SQUARE_1:11;
then q2 - s2 > 0 & p2 - s2 < 0 by A8,A9,A10,REAL_2:129,SQUARE_1:24;
hence thesis by REAL_2:106,SQUARE_1:12;
end;

theorem
for p being Point of TOP-REAL 2
ex q being Point of TOP-REAL 2 st q1 < W-bound D & p <> q
proof
let p be Point of TOP-REAL 2;
take q = |[W-bound D - 1, p2 - 1]|;
W-bound D - 1 < W-bound D - 0 by REAL_1:92;
hence q1 < W-bound D by EUCLID:56;
p2 - 1 < p2 - 0 by REAL_1:92; hence p <> q by EUCLID:56;
end;

theorem
for p being Point of TOP-REAL 2
ex q being Point of TOP-REAL 2 st q1 > E-bound D & p <> q
proof
let p be Point of TOP-REAL 2;
take q = |[E-bound D + 1, p2 - 1]|;
E-bound D + 1 > E-bound D + 0 by REAL_1:53;
hence q1 > E-bound D by EUCLID:56;
p2 - 1 < p2 - 0 by REAL_1:92; hence p <> q by EUCLID:56;
end;

theorem
for p being Point of TOP-REAL 2
ex q being Point of TOP-REAL 2 st q2 > N-bound D & p <> q
proof
let p be Point of TOP-REAL 2;
take q = |[p1 - 1,N-bound D + 1]|;
N-bound D + 1 > N-bound D + 0 by REAL_1:53;
hence q2 > N-bound D by EUCLID:56;
p1 - 1 < p1 - 0 by REAL_1:92; hence p <> q by EUCLID:56;
end;

theorem
for p being Point of TOP-REAL 2
ex q being Point of TOP-REAL 2 st q2 < S-bound D & p <> q
proof
let p be Point of TOP-REAL 2;
take q = |[p1 - 1,S-bound D - 1]|;
S-bound D - 1 < S-bound D - 0 by REAL_1:92;
hence q2 < S-bound D by EUCLID:56;
p1 - 1 < p1 - 0 by REAL_1:92; hence p <> q by EUCLID:56;
end;

definition
cluster convex non empty -> connected Subset of TOP-REAL 2;
coherence by JORDAN1:9;
cluster non horizontal -> non empty Subset of TOP-REAL 2;
coherence
proof
let P be Subset of TOP-REAL 2;
assume P is non horizontal;
then ex p, q being Point of TOP-REAL 2 st p in P & q in P & p2 <> q2
by SPPOL_1:def 2;
hence thesis;
end;
cluster non vertical -> non empty Subset of TOP-REAL 2;
coherence
proof
let P be Subset of TOP-REAL 2;
assume P is non vertical;
then ex p, q being Point of TOP-REAL 2 st p in P & q in P & p1 <> q1
by SPPOL_1:def 3;
hence thesis;
end;
cluster being_Region -> open connected Subset of TOP-REAL 2;
coherence by TOPREAL4:def 3;
cluster open connected -> being_Region Subset of TOP-REAL 2;
coherence by TOPREAL4:def 3;
end;

definition
cluster empty -> horizontal Subset of TOP-REAL 2;
coherence
proof
let A be Subset of TOP-REAL 2;
assume
A1:   A is empty;
assume A is non horizontal;
then reconsider B = A as non horizontal Subset of TOP-REAL 2;
B is non empty;
hence thesis by A1;
end;
cluster empty -> vertical Subset of TOP-REAL 2;
coherence
proof
let A be Subset of TOP-REAL 2;
assume
A2:   A is empty;
assume A is non vertical;
then reconsider B = A as non vertical Subset of TOP-REAL 2;
B is non empty;
hence thesis by A2;
end;
end;

definition
cluster non empty convex Subset of TOP-REAL 2;
existence
proof
consider C being non empty convex Subset of TOP-REAL 2;
take C;
thus thesis;
end;
end;

definition let a, b be Point of TOP-REAL 2;
cluster LSeg(a,b) -> convex connected;
coherence by GOBOARD9:7,8;
end;

definition
cluster R^2-unit_square -> connected;
coherence
proof
A1:  R^2-unit_square = LSeg(|[ 0,0 ]|, |[ 0,1 ]|) \/ LSeg(|[ 0,1 ]|, |[ 1,1 ]|)
\/ LSeg(|[ 1,1 ]|, |[ 1,0 ]|) \/ LSeg(|[ 1,0 ]|, |[ 0,0 ]|)
by TOPREAL1:20,XBOOLE_1:4;
LSeg(|[0,0]|,|[0,1]|) meets LSeg(|[0,1]|,|[1,1]|) &
LSeg(|[0,0]|,|[1,0]|) meets LSeg(|[1,0]|,|[1,1]|) &
LSeg(|[0,1]|,|[1,1]|) meets LSeg(|[1,0]|,|[1,1]|)
by TOPREAL1:21,22,24,XBOOLE_0:def 7;
hence thesis by A1,JORDAN1:8;
end;
end;

definition
cluster being_simple_closed_curve -> connected compact Subset of TOP-REAL 2;
coherence
proof
let P be Subset of TOP-REAL 2;
given f being map of (TOP-REAL 2)|R^2-unit_square, (TOP-REAL 2)|P
such that
A1: f is_homeomorphism;
A2: (TOP-REAL 2)|R^2-unit_square, (TOP-REAL 2)|P are_homeomorphic
proof
take f;
thus f is_homeomorphism by A1;
end;
thus P is connected
proof
(TOP-REAL 2)|R^2-unit_square is connected by CONNSP_1:def 3;
then (TOP-REAL 2)|P is connected by A2,Th25;
hence thesis by CONNSP_1:def 3;
end;
per cases;
suppose
A3:   P is empty;
{}TOP-REAL 2 is compact;
hence thesis by A3;
suppose P is non empty;
then reconsider R = P as non empty Subset of TOP-REAL 2;
f is continuous & rng f = [#]((TOP-REAL 2)|P) by A1,TOPS_2:def 5;
then (TOP-REAL 2)|R is compact by COMPTS_1:23;
hence P is compact by COMPTS_1:12;
end;
end;

theorem  :: SPRECT_3:26
LSeg(NE-corner P,SE-corner P) c= L~SpStSeq P
proof
A1: LSeg(NE-corner P,SE-corner P) c=
(LSeg(NW-corner P,NE-corner P) \/ LSeg(NE-corner P,SE-corner P))
by XBOOLE_1:7;
LSeg(NW-corner P,NE-corner P) \/ LSeg(NE-corner P,SE-corner P) c=
(LSeg(NW-corner P,NE-corner P) \/ LSeg(NE-corner P,SE-corner P)) \/
(LSeg(SE-corner P,SW-corner P) \/ LSeg(SW-corner P,NW-corner P))
by XBOOLE_1:7;
then LSeg(NE-corner P,SE-corner P) c=
(LSeg(NW-corner P,NE-corner P) \/ LSeg(NE-corner P,SE-corner P)) \/
(LSeg(SE-corner P,SW-corner P) \/ LSeg(SW-corner P,NW-corner P))
by A1,XBOOLE_1:1;
hence thesis by SPRECT_1:43;
end;

theorem
LSeg(SW-corner P,SE-corner P) c= L~SpStSeq P
proof
A1: LSeg(SW-corner P,SE-corner P) c=
(LSeg(NW-corner P,NE-corner P) \/ LSeg(NE-corner P,SE-corner P)) \/
LSeg(SW-corner P,SE-corner P) by XBOOLE_1:7;
LSeg(NW-corner P,NE-corner P) \/ LSeg(NE-corner P,SE-corner P) \/
LSeg(SE-corner P,SW-corner P) c=
LSeg(NW-corner P,NE-corner P) \/ LSeg(NE-corner P,SE-corner P) \/
LSeg(SE-corner P,SW-corner P) \/ LSeg(SW-corner P,NW-corner P)
by XBOOLE_1:7;
then LSeg(NW-corner P,NE-corner P) \/ LSeg(NE-corner P,SE-corner P) \/
LSeg(SE-corner P,SW-corner P) c=
LSeg(NW-corner P,NE-corner P) \/ LSeg(NE-corner P,SE-corner P) \/
(LSeg(SE-corner P,SW-corner P) \/ LSeg(SW-corner P,NW-corner P))
by XBOOLE_1:4;
then LSeg(SW-corner P,SE-corner P) c=
(LSeg(NW-corner P,NE-corner P) \/ LSeg(NE-corner P,SE-corner P)) \/
(LSeg(SE-corner P,SW-corner P) \/ LSeg(SW-corner P,NW-corner P))
by A1,XBOOLE_1:1;
hence thesis by SPRECT_1:43;
end;

theorem
LSeg(SW-corner P,NW-corner P) c= L~SpStSeq P
proof
LSeg(SW-corner P,NW-corner P) c=
LSeg(NW-corner P,NE-corner P) \/ LSeg(NE-corner P,SE-corner P) \/
LSeg(SE-corner P,SW-corner P) \/ LSeg(SW-corner P,NW-corner P)
by XBOOLE_1:7;
then LSeg(SW-corner P,NW-corner P) c=
LSeg(NW-corner P,NE-corner P) \/ LSeg(NE-corner P,SE-corner P) \/
(LSeg(SE-corner P,SW-corner P) \/ LSeg(SW-corner P,NW-corner P))
by XBOOLE_1:4;
hence thesis by SPRECT_1:43;
end;

theorem
for C being Subset of TOP-REAL 2 holds
{p where p is Point of TOP-REAL 2: p1 < W-bound C} is
non empty convex connected Subset of TOP-REAL 2
proof
let C be Subset of TOP-REAL 2;
set A = {p where p is Point of TOP-REAL 2: p1 < W-bound C};
A c= the carrier of TOP-REAL 2
proof
let a be set;
assume a in A;
then consider p being Point of TOP-REAL 2 such that
A1:     a = p and p1 < W-bound C;
thus thesis by A1;
end;
then reconsider A as Subset of TOP-REAL 2;
set p = W-bound C;
set b = |[p-1,0]|;
A2: p - 1 < p - 0 by REAL_1:92;
b1 = p-1 by EUCLID:56;
then A3: b in A by A2;
A is convex
proof
let w1, w2 be Point of TOP-REAL 2;
assume w1 in A;
then consider p being Point of TOP-REAL 2 such that
A4:     w1 = p and
A5:     p1 < W-bound C;
assume w2 in A;
then consider q being Point of TOP-REAL 2 such that
A6:     w2 = q and
A7:     q1 < W-bound C;
let k be set; assume
A8:     k in LSeg(w1,w2);
then reconsider z = k as Point of TOP-REAL 2;
per cases by REAL_1:def 5;
suppose p1 < q1;
then z1 <= w21 by A4,A6,A8,TOPREAL1:9;
then z1 < W-bound C by A6,A7,AXIOMS:22;
hence k in A;
suppose q1 < p1;
then z1 <= w11 by A4,A6,A8,TOPREAL1:9;
then z1 < W-bound C by A4,A5,AXIOMS:22;
hence k in A;
suppose p1 = q1;
then z1 = p1 by A4,A6,A8,GOBOARD7:5;
hence k in A by A5;
end;
then reconsider A as non empty convex Subset of TOP-REAL 2 by A3;
A is connected;
hence thesis;
end;

begin  :: Balls as subsets of TOP-REAL n

theorem Th47:
e = q & p in Ball(e,r) implies q1-r < p1 & p1 < q1+r
proof
assume that
A1:   e = q and
A2:   p in Ball(e,r);
reconsider f = p as Point of Euclid 2 by TOPREAL3:13;
A3: dist(e,f) < r by A2,METRIC_1:12;
A4: dist(e,f) = (Pitag_dist 2).(e,f) by Lm2,METRIC_1:def 1
.= sqrt ((q1 - p1)^2 + (q2 - p2)^2) by A1,TOPREAL3:12;
A5: r > 0 by A2,TBSP_1:17;
then A6: r^2 > 0 by SQUARE_1:74;
assume
A7:   not thesis;
per cases by A7;
suppose q1-r >= p1;
then q1-p1 >= r by REAL_2:165;
then A8: (q1-p1)^2 >= r^2 by A5,SQUARE_1:77;
(q2-p2)^2 >= 0 by SQUARE_1:72;
then (q1-p1)^2 + (q2-p2)^2 >= (q1-p1)^2 + 0 by AXIOMS:24;
then (q1-p1)^2 + (q2-p2)^2 >= r^2 by A8,AXIOMS:22;
then sqrt((q1-p1)^2 + (q2-p2)^2) >= sqrt(r^2) by A6,SQUARE_1:94;
suppose p1 >= q1+r;
then p1-q1 >= r by REAL_1:84;
then (p1-q1)^2 >= r^2 by A5,SQUARE_1:77;
then (-(q1-p1))^2 >= r^2 by XCMPLX_1:143;
then A9: (q1-p1)^2 >= r^2 by SQUARE_1:61;
(q2-p2)^2 >= 0 by SQUARE_1:72;
then (q1-p1)^2 + (q2-p2)^2 >= (q1-p1)^2 + 0 by AXIOMS:24;
then (q1-p1)^2 + (q2-p2)^2 >= r^2 by A9,AXIOMS:22;
then sqrt((q1-p1)^2 + (q2-p2)^2) >= sqrt(r^2) by A6,SQUARE_1:94;
end;

theorem Th48:
e = q & p in Ball(e,r) implies q2-r < p2 & p2 < q2+r
proof
assume that
A1:   e = q and
A2:   p in Ball(e,r);
reconsider f = p as Point of Euclid 2 by TOPREAL3:13;
A3: dist(e,f) < r by A2,METRIC_1:12;
A4: dist(e,f) = (Pitag_dist 2).(e,f) by Lm2,METRIC_1:def 1
.= sqrt ((q1 - p1)^2 + (q2 - p2)^2) by A1,TOPREAL3:12;
A5: r > 0 by A2,TBSP_1:17;
then A6: r^2 > 0 by SQUARE_1:74;
assume
A7:   not thesis;
per cases by A7;
suppose q2-r >= p2;
then q2-p2 >= r by REAL_2:165;
then A8: (q2-p2)^2 >= r^2 by A5,SQUARE_1:77;
(q1-p1)^2 >= 0 by SQUARE_1:72;
then (q1-p1)^2 + (q2-p2)^2 >= (q2-p2)^2 + 0 by AXIOMS:24;
then (q1-p1)^2 + (q2-p2)^2 >= r^2 by A8,AXIOMS:22;
then sqrt((q1-p1)^2 + (q2-p2)^2) >= sqrt(r^2) by A6,SQUARE_1:94;
suppose p2 >= q2+r;
then p2-q2 >= r by REAL_1:84;
then (p2-q2)^2 >= r^2 by A5,SQUARE_1:77;
then (-(q2-p2))^2 >= r^2 by XCMPLX_1:143;
then A9: (q2-p2)^2 >= r^2 by SQUARE_1:61;
(q1-p1)^2 >= 0 by SQUARE_1:72;
then (q1-p1)^2 + (q2-p2)^2 >= (q2-p2)^2 + 0 by AXIOMS:24;
then (q1-p1)^2 + (q2-p2)^2 >= r^2 by A9,AXIOMS:22;
then sqrt((q1-p1)^2 + (q2-p2)^2) >= sqrt(r^2) by A6,SQUARE_1:94;
end;

theorem Th49:
p = e implies
product ((1,2) --> (].p1-r/sqrt 2,p1+r/sqrt 2.[,
].p2-r/sqrt 2,p2+r/sqrt 2.[))
c= Ball(e,r)
proof
set A = ].p1-r/sqrt 2,p1+r/sqrt 2.[,
B = ].p2-r/sqrt 2,p2+r/sqrt 2.[,
f = (1,2) --> (A,B);
assume
A1:   p = e;
let a be set;
assume a in product f;
then consider g being Function such that
A2:   a = g and
A3:   dom g = dom f and
A4:   for x being set st x in dom f holds g.x in f.x by CARD_3:def 5;
A5: A = {m where m is Real :
p1-r/sqrt 2 < m & m < p1+r/sqrt 2 } by RCOMP_1:def 2;
A6: B = {n where n is Real : p2-r/sqrt 2 < n & n < p2+r/sqrt 2 }
by RCOMP_1:def 2;
A7: dom f = {1,2} by FUNCT_4:65;
then A8: 1 in dom f & 2 in dom f by TARSKI:def 2;
f.1 = A & f.2 = B by FUNCT_4:66;
then A9: g.1 in A & g.2 in B by A4,A8;
then consider m being Real such that
A10:   m = g.1 and
p1-r/sqrt 2 < m & m < p1+r/sqrt 2 by A5;
consider n being Real such that
A11:   n = g.2 and
p2-r/sqrt 2 < n & n < p2+r/sqrt 2 by A6,A9;
p1+r/sqrt 2 > p1-r/sqrt 2 by A9,RCOMP_1:12;
then p1-(p1+r/sqrt 2) < p1-(p1-r/sqrt 2) by REAL_1:92;
then p1-p1-r/sqrt 2 < p1-(p1-r/sqrt 2) by XCMPLX_1:36;
then p1-p1-r/sqrt 2 < p1-p1+r/sqrt 2 by XCMPLX_1:37;
then 0-r/sqrt 2 < p1-p1+r/sqrt 2 by XCMPLX_1:14;
then 0-r/sqrt 2 < 0+r/sqrt 2 by XCMPLX_1:14;
then -r/sqrt 2 < r/sqrt 2 by XCMPLX_1:150;
then -r/sqrt 2+r/sqrt 2 < r/sqrt 2+r/sqrt 2 by REAL_1:53;
then 0 < r/sqrt 2+r/sqrt 2 by XCMPLX_0:def 6;
then A12: 0 < (r+r)/sqrt 2 by XCMPLX_1:63;
A13: now
assume 0 >= r;
then 0+0 >= r+r by REAL_1:55;
end;
A14: dom <*g.1,g.2*> = {1,2} by FINSEQ_1:4,FINSEQ_3:29;
now
let k be set;
assume k in dom g;
then k = 1 or k = 2 by A3,A7,TARSKI:def 2;
hence g.k = <*g.1,g.2*>.k by FINSEQ_1:61;
end;
then a = <*g.1,g.2*> by A2,A3,A7,A14,FUNCT_1:9;
then A15: a = |[m,n]| by A10,A11,EUCLID:def 16;
then reconsider c = a as Point of TOP-REAL 2;
reconsider b = c as Point of Euclid 2 by TOPREAL3:13;
A16: 0 <= abs(m-p1) & 0 <= abs(n-p2) by ABSVALUE:5;
0 <= (m-p1)^2 & 0 <= (n-p2)^2 by SQUARE_1:72;
then A17: 0+0 <= (m-p1)^2 + (n-p2)^2 by REAL_1:55;
abs(m-p1) < r/sqrt 2 & abs(n-p2) < r/sqrt 2 by A9,A10,A11,RCOMP_1:8;
then (abs(m-p1))^2 < (r/sqrt 2)^2 & (abs(n-p2))^2 < (r/sqrt 2)^2
by A16,SQUARE_1:78;
then (abs(m-p1))^2 < r^2/(sqrt 2)^2 & (abs(n-p2))^2 < r^2/(sqrt 2)^2
by SQUARE_1:69;
then (abs(m-p1))^2 < r^2/2 & (abs(n-p2))^2 < r^2/2 by SQUARE_1:def 4;
then (m-p1)^2 < r^2/2 & (n-p2)^2 < r^2/2 by SQUARE_1:62;
then (m-p1)^2 + (n-p2)^2 < r^2/2 + r^2/2 by REAL_1:67;
then (m-p1)^2 + (n-p2)^2 < r^2 by XCMPLX_1:66;
then sqrt((m-p1)^2 + (n-p2)^2) < sqrt(r^2) by A17,SQUARE_1:95;
then A18: sqrt((m-p1)^2 + (n-p2)^2) < r by A13,SQUARE_1:89;
A19: dist(b,e) = (Pitag_dist 2).(b,e) by Lm2,METRIC_1:def 1
.= sqrt ((c1 - p1)^2 + (c2 - p2)^2) by A1,TOPREAL3:12;
c1 = m & c2 = n by A15,EUCLID:56;
hence a in Ball(e,r) by A18,A19,METRIC_1:12;
end;

theorem Th50:
p = e implies Ball(e,r) c= product((1,2)-->(].p1-r,p1+r.[,].p2-r,p2+r.[))
proof
set A = ].p1-r,p1+r.[,
B = ].p2-r,p2+r.[,
f = (1,2)-->(A,B);
assume that
A1:   p = e;
let a be set;
assume
A2:   a in Ball(e,r);
then reconsider b = a as Point of Euclid 2;
reconsider q = b as Point of TOP-REAL 2 by TOPREAL3:13;
reconsider g = q as FinSequence by EUCLID:27;
A3: dom f = {1,2} by FUNCT_4:65;
q is Function of Seg 2, REAL by EUCLID:26;
then A4: dom g = {1,2} by FINSEQ_1:4,FUNCT_2:def 1;
for x being set st x in dom f holds g.x in f.x
proof
let x be set;
assume
A5:     x in dom f;
per cases by A3,A5,TARSKI:def 2;
suppose
A6:     x = 1;
A7:   f.1 = A by FUNCT_4:66;
A8:   g.1 = q1 by EUCLID:def 14;
p1-r < q1 & q1 < p1+r by A1,A2,Th47;
hence g.x in f.x by A6,A7,A8,JORDAN6:45;
suppose
A9:     x = 2;
A10:   f.2 = B by FUNCT_4:66;
A11:   g.2 = q2 by EUCLID:def 15;
p2-r < q2 & q2 < p2+r by A1,A2,Th48;
hence g.x in f.x by A9,A10,A11,JORDAN6:45;
end;
hence a in product f by A3,A4,CARD_3:18;
end;

theorem Th51:
P = Ball(e,r) & p = e implies proj1.:P = ].p1-r,p1+r.[
proof
assume that
A1:   P = Ball(e,r) and
A2:   p = e;
hereby
let a be set;
assume a in proj1.:P;
then consider x being set such that
A3:     x in the carrier of TOP-REAL 2 and
A4:     x in P and
A5:     a = proj1.x by FUNCT_2:115;
reconsider x as Point of TOP-REAL 2 by A3;
reconsider b = a as Real by A5;
a = x1 by A5,PSCOMP_1:def 28;
then p1-r < b & b < p1+r by A1,A2,A4,Th47;
hence a in ].p1-r,p1+r.[ by JORDAN6:45;
end;
let a be set;
assume
A6:   a in ].p1-r,p1+r.[;
then reconsider b = a as Real;
b < p1+r by A6,JORDAN6:45;
then b - p1 < p1+r - p1 by REAL_1:54
;
then b - p1 < p1 - p1 + r by XCMPLX_1:29;
then A7: b - p1 < 0 + r by XCMPLX_1:14;
A8: a = |[b,p2]|1 by EUCLID:56
.= proj1.(|[b,p2]|) by PSCOMP_1:def 28;
reconsider f = |[b,p2]| as Point of Euclid 2 by TOPREAL3:13;
A9: dist(f,e) = (Pitag_dist 2).(f,e) by Lm2,METRIC_1:def 1
.= sqrt ((|[b,p2]|1 - p1)^2 + (|[b,p2]|2 - p2)^2
) by A2,TOPREAL3:12
.= sqrt ((b - p1)^2 + (|[b,p2]|2 - p2)^2) by EUCLID:56
.= sqrt ((b - p1)^2 + (p2 - p2)^2) by EUCLID:56
.= sqrt ((b - p1)^2 + 0) by SQUARE_1:60,XCMPLX_1:14;
now per cases;
case 0 <= b - p1;
hence dist(f,e) < r by A7,A9,SQUARE_1:89;
case 0 > b - p1;
then A10:   -(b - p1) > 0 by REAL_1:66;
A11:   sqrt ((b - p1)^2) = sqrt ((-(b - p1))^2) by SQUARE_1:61
.= -(b - p1) by A10,SQUARE_1:89;
p1 - r < b by A6,JORDAN6:45;
then p1 - r + r < b + r by REAL_1:53;
then p1 - (r - r) < b + r by XCMPLX_1:37;
then p1 - 0 < b + r by XCMPLX_1:14;
then p1 - b < r + b - b by REAL_1:54
;
then p1 - b < r + (b - b) by XCMPLX_1:29;
then p1 - b < r + 0 by XCMPLX_1:14;
hence dist(f,e) < r by A9,A11,XCMPLX_1:143;
end;
then |[b,p2]| in P by A1,METRIC_1:12;
hence a in proj1.:P by A8,FUNCT_2:43;
end;

theorem Th52:
P = Ball(e,r) & p = e implies proj2.:P = ].p2-r,p2+r.[
proof
assume that
A1:   P = Ball(e,r) and
A2:   p = e;
hereby
let a be set;
assume a in proj2.:P;
then consider x being set such that
A3:     x in the carrier of TOP-REAL 2 and
A4:     x in P and
A5:     a = proj2.x by FUNCT_2:115;
reconsider x as Point of TOP-REAL 2 by A3;
reconsider b = a as Real by A5;
a = x2 by A5,PSCOMP_1:def 29;
then p2-r < b & b < p2+r by A1,A2,A4,Th48;
hence a in ].p2-r,p2+r.[ by JORDAN6:45;
end;
let a be set;
assume
A6:   a in ].p2-r,p2+r.[;
then reconsider b = a as Real;
b < p2+r by A6,JORDAN6:45;
then b - p2 < p2+r - p2 by REAL_1:54
;
then b - p2 < p2 - p2 + r by XCMPLX_1:29;
then A7: b - p2 < 0 + r by XCMPLX_1:14;
A8: a = |[p1,b]|2 by EUCLID:56
.= proj2.(|[p1,b]|) by PSCOMP_1:def 29;
reconsider f = |[p1,b]| as Point of Euclid 2 by TOPREAL3:13;
A9: dist(f,e) = (Pitag_dist 2).(f,e) by Lm2,METRIC_1:def 1
.= sqrt ((|[p1,b]|1 - p1)^2 + (|[p1,b]|2 - p2)^2
) by A2,TOPREAL3:12
.= sqrt ((p1 - p1)^2 + (|[p1,b]|2 - p2)^2) by EUCLID:56
.= sqrt ((p1 - p1)^2 + (b - p2)^2) by EUCLID:56
.= sqrt (0 + (b - p2)^2) by SQUARE_1:60,XCMPLX_1:14;
now per cases;
case 0 <= b - p2;
hence dist(f,e) < r by A7,A9,SQUARE_1:89;
case 0 > b - p2;
then A10:   -(b - p2) > 0 by REAL_1:66;
A11:   sqrt ((b - p2)^2) = sqrt ((-(b - p2))^2) by SQUARE_1:61
.= -(b - p2) by A10,SQUARE_1:89;
p2 - r < b by A6,JORDAN6:45;
then p2 - r + r < b + r by REAL_1:53;
then p2 - (r - r) < b + r by XCMPLX_1:37;
then p2 - 0 < b + r by XCMPLX_1:14;
then p2 - b < r + b - b by REAL_1:54
;
then p2 - b < r + (b - b) by XCMPLX_1:29;
then p2 - b < r + 0 by XCMPLX_1:14;
hence dist(f,e) < r by A9,A11,XCMPLX_1:143;
end;
then |[p1,b]| in P by A1,METRIC_1:12;
hence a in proj2.:P by A8,FUNCT_2:43;
end;

theorem
D = Ball(e,r) & p = e implies W-bound D = p1 - r
proof
assume that
A1:   D = Ball(e,r) and
A2:   p = e;
A3: r > 0 by A1,TBSP_1:17;
then A4: p1-r < p1-0 by REAL_1:92;
p1+0 < p1+r by A3,REAL_1:53;
then p1-r < p1+r by A4,AXIOMS:22;
then A5: inf ].p1-r,p1+r.[ = p1-r by Th22;
proj1.:D = ].p1-r,p1+r.[ by A1,A2,Th51;
hence W-bound D = p1 - r by A5,SPRECT_1:48;
end;

theorem
D = Ball(e,r) & p = e implies E-bound D = p1 + r
proof
assume that
A1:   D = Ball(e,r) and
A2:   p = e;
A3: r > 0 by A1,TBSP_1:17;
then A4: p1-r < p1-0 by REAL_1:92;
p1+0 < p1+r by A3,REAL_1:53;
then p1-r < p1+r by A4,AXIOMS:22;
then A5: sup ].p1-r,p1+r.[ = p1+r by Th22;
proj1.:D = ].p1-r,p1+r.[ by A1,A2,Th51;
hence E-bound D = p1 + r by A5,SPRECT_1:51;
end;

theorem
D = Ball(e,r) & p = e implies S-bound D = p2 - r
proof
assume that
A1:   D = Ball(e,r) and
A2:   p = e;
A3: r > 0 by A1,TBSP_1:17;
then A4: p2-r < p2-0 by REAL_1:92;
p2+0 < p2+r by A3,REAL_1:53;
then p2-r < p2+r by A4,AXIOMS:22;
then A5: inf ].p2-r,p2+r.[ = p2-r by Th22;
proj2.:D = ].p2-r,p2+r.[ by A1,A2,Th52;
hence S-bound D = p2 - r by A5,SPRECT_1:49;
end;

theorem
D = Ball(e,r) & p = e implies N-bound D = p2 + r
proof
assume that
A1:   D = Ball(e,r) and
A2:   p = e;
A3: r > 0 by A1,TBSP_1:17;
then A4: p2-r < p2-0 by REAL_1:92;
p2+0 < p2+r by A3,REAL_1:53;
then p2-r < p2+r by A4,AXIOMS:22;
then A5: sup ].p2-r,p2+r.[ = p2+r by Th22;
proj2.:D = ].p2-r,p2+r.[ by A1,A2,Th52;
hence N-bound D = p2 + r by A5,SPRECT_1:50;
end;

theorem
D = Ball(e,r) implies D is non horizontal
proof
assume
A1:   D = Ball(e,r);
reconsider p = e as Point of TOP-REAL 2 by TOPREAL3:13;
take p, q = |[p1,p2-r/2]|;
reconsider f = q as Point of Euclid 2 by TOPREAL3:13;
A2: r > 0 by A1,TBSP_1:17;
then A3: r/2 > 0 by REAL_2:127;
thus p in D by A1,A2,TBSP_1:16;
dist(e,f) = (Pitag_dist 2).(e,f) by Lm2,METRIC_1:def 1
.= sqrt ((p1 - q1)^2 + (p2 - q2)^2) by TOPREAL3:12
.= sqrt ((p1 - p1)^2 + (p2 - q2)^2) by EUCLID:56
.= sqrt ((p1 - p1)^2 + (p2 - (p2-r/2))^2) by EUCLID:56
.= sqrt (0 + (p2 - (p2-r/2))^2) by SQUARE_1:60,XCMPLX_1:14
.= sqrt ((p2 - p2 + r/2)^2) by XCMPLX_1:37
.= sqrt ((0 + r/2)^2) by XCMPLX_1:14
.= r/2 by A3,SQUARE_1:89;
then dist(e,f) < r by A2,SEQ_2:4;
hence q in D by A1,METRIC_1:12;
p2-r/2 < p2-0 by A3,REAL_1:92; hence p2 <> q2 by EUCLID:56;
end;

theorem
D = Ball(e,r) implies D is non vertical
proof
assume
A1:   D = Ball(e,r);
reconsider p = e as Point of TOP-REAL 2 by TOPREAL3:13;
take p, q = |[p1-r/2,p2]|;
reconsider f = q as Point of Euclid 2 by TOPREAL3:13;
A2: r > 0 by A1,TBSP_1:17;
then A3: r/2 > 0 by REAL_2:127;
thus p in D by A1,A2,TBSP_1:16;
dist(e,f) = (Pitag_dist 2).(e,f) by Lm2,METRIC_1:def 1
.= sqrt ((p1 - q1)^2 + (p2 - q2)^2) by TOPREAL3:12
.= sqrt ((p1 - (p1-r/2))^2 + (p2 - q2)^2) by EUCLID:56
.= sqrt ((p1 - (p1-r/2))^2 + (p2 - p2)^2) by EUCLID:56
.= sqrt ((p1 - (p1-r/2))^2 + 0) by SQUARE_1:60,XCMPLX_1:14
.= sqrt ((p1 - p1 + r/2)^2) by XCMPLX_1:37
.= sqrt ((0 + r/2)^2) by XCMPLX_1:14
.= r/2 by A3,SQUARE_1:89;
then dist(e,f) < r by A2,SEQ_2:4;
hence q in D by A1,METRIC_1:12;
p1-r/2 < p1-0 by A3,REAL_1:92; hence p1 <> q1 by EUCLID:56;
end;

theorem
for f being Point of Euclid 2, x being Point of TOP-REAL 2 st
x in Ball(f,a) holds not |[x1-2*a,x2]| in Ball(f,a)
proof
let f be Point of Euclid 2,
x be Point of TOP-REAL 2 such that
A1:   x in Ball(f,a);
set p = |[x1-2*a,x2]|;
reconsider z = p, X = x as Point of Euclid 2 by TOPREAL3:13;
A2: dist(f,X) < a by A1,METRIC_1:12;
a > 0 by A1,TBSP_1:17;
then A3: 2*a > 2*0 by REAL_1:70;
A4: dist(X,z) = (Pitag_dist 2).(X,z) by Lm2,METRIC_1:def 1
.= sqrt ((x1 - p1)^2 + (x2 - p2)^2) by TOPREAL3:12
.= sqrt ((x1 - (x1-2*a))^2 + (x2 - p2)^2) by EUCLID:56
.= sqrt ((x1 - (x1-2*a))^2 + (x2 - x2)^2) by EUCLID:56
.= sqrt ((x1 - x1 + 2*a)^2 + (x2 - x2)^2) by XCMPLX_1:37
.= sqrt ((x1 - x1)^2 + 2*(x1 - x1)*(2*a) + (2*a)^2 + (x2 - x2)^2)
by SQUARE_1:63
.= sqrt (0^2 + 2*(x1 - x1)*(2*a) + (2*a)^2 + (x2 - x2)^2
) by XCMPLX_1:14
.= sqrt (0^2 + 2*0 * (2*a) + (2*a)^2 + (x2 - x2)^2) by XCMPLX_1:14
.= sqrt ((2*a)^2) by SQUARE_1:60,XCMPLX_1:14
.= 2*a by A3,SQUARE_1:89;
assume |[x1-2*a,x2]| in Ball(f,a);
then dist(f,z) < a by METRIC_1:12;
then dist(f,X) + dist(f,z) < a + a by A2,REAL_1:67;
then dist(f,X) + dist(f,z) < 2*a by XCMPLX_1:11;
end;

theorem
for X being non empty compact Subset of TOP-REAL 2,
p being Point of Euclid 2 st p = 0.REAL 2 & a > 0 holds
X c= Ball(p, abs(E-bound X)+abs(N-bound X)+abs(W-bound X)+abs(S-bound X)+a)
proof
let X be non empty compact Subset of TOP-REAL 2,
p be Point of Euclid 2 such that
A1:   p = 0.REAL 2 and
A2:   a > 0;
let x be set; assume
A3:   x in X;
then reconsider b = x as Point of Euclid 2 by TOPREAL3:13;
set A = X,
n = N-bound A, s = S-bound A, e = E-bound A, w = W-bound A,
r = abs(e)+abs(n)+abs(w)+abs(s)+a;
reconsider P = p, B = b as Point of TOP-REAL 2 by TOPREAL3:13;
A4: w <= B1 & B1 <= e & s <= B2 & B2 <= n by A3,PSCOMP_1:71;
A5: P1 = 0 & P2 = 0 by A1,Th32;
A6: dist(p,b) = (Pitag_dist 2).(p,b) by Lm2,METRIC_1:def 1
.= sqrt ((P1 - B1)^2 + (P2 - B2)^2) by TOPREAL3:12
.= sqrt ((- B1)^2 + (P2 - B2)^2) by A5,XCMPLX_1:150
.= sqrt ((- B1)^2 + (- B2)^2) by A5,XCMPLX_1:150
.= sqrt ((B1)^2 + (- B2)^2) by SQUARE_1:61
.= sqrt ((B1)^2 + (B2)^2) by SQUARE_1:61;
0 <= (B1)^2 & 0 <= (B2)^2 by SQUARE_1:72;
then sqrt ((B1)^2 + (B2)^2) <= sqrt(B1)^2 + sqrt(B2)^2 by Th6;
then sqrt ((B1)^2 + (B2)^2) <= abs(B1) + sqrt(B2)^2 by SQUARE_1:91;
then A7: sqrt ((B1)^2 + (B2)^2) <= abs(B1) + abs(B2) by SQUARE_1:91;
A8: 0 <= abs(s) by ABSVALUE:5;
A9: 0 <= abs(w) by ABSVALUE:5;
A10: 0 <= abs(e) by ABSVALUE:5;
A11: 0 <= abs(n) by ABSVALUE:5;
A12: abs(e) + abs(n) + abs(w) + abs(s) + 0 <
abs(e) + abs(n) + abs(w) + abs(s) + a
by A2,REAL_1:67;
now per cases;
case B1 >= 0 & B2 >= 0;
then abs(B1) <= abs(e) & abs(B2) <= abs(n) by A4,Th7;
then abs(B1) + abs(B2) <= abs(e) + abs(n) by REAL_1:55;
then A13:   dist(p,b) <= abs(e) + abs(n) by A6,A7,AXIOMS:22;
abs(e) + abs(n) + 0 <= abs(e) + abs(n) + abs(w) by A9,REAL_1:55;
then abs(e) + abs(n) <= abs(e) + abs(n) + abs(w) + abs(s)
by A8,REAL_1:55;
then abs(e) + abs(n) < r by A12,AXIOMS:22;
hence dist(p,b) < r by A13,AXIOMS:22;
case B1 < 0 & B2 >= 0;
then abs(B1) <= abs(w) & abs(B2) <= abs(n) by A4,Th7,Th8;
then abs(B1) + abs(B2) <= abs(w) + abs(n) by REAL_1:55;
then A14:   dist(p,b) <= abs(w) + abs(n) by A6,A7,AXIOMS:22;
0 + (abs(n) + abs(w)) <= abs(e) + (abs(n) + abs(w))
by A10,REAL_1:55;
then A15:   abs(n) + abs(w) <= abs(e) + abs(n) + abs(w) by XCMPLX_1:1;
abs(e) + abs(n) + abs(w) + 0 <= abs(e) + abs(n) + abs(w) + abs(s)
by A8,REAL_1:55;
then abs(w) + abs(n) <= abs(e) + abs(n) + abs(w) + abs(s)
by A15,AXIOMS:22;
then abs(w) + abs(n) < r by A12,AXIOMS:22;
hence dist(p,b) < r by A14,AXIOMS:22;
case B1 >= 0 & B2 < 0;
then abs(B1) <= abs(e) & abs(B2) <= abs(s) by A4,Th7,Th8;
then abs(B1) + abs(B2) <= abs(e) + abs(s) by REAL_1:55;
then A16:   dist(p,b) <= abs(e) + abs(s) by A6,A7,AXIOMS:22;
abs(e) + abs(s) + 0 <= abs(e) + abs(s) + abs(n) by A11,REAL_1:55;
then A17:   abs(e) + abs(s) <= abs(e) + abs(n) + abs(s) by XCMPLX_1:1;
abs(e) + abs(n) + abs(s) + 0 <= abs(e) + abs(n) + abs(s) + abs(w)
by A9,REAL_1:55;
then abs(e) + abs(n) + abs(s) <= abs(e) + abs(n) + abs(w) + abs(s)
by XCMPLX_1:1;
then abs(e) + abs(s) <= abs(e) + abs(n) + abs(w) + abs(s)
by A17,AXIOMS:22;
then abs(e) + abs(s) < r by A12,AXIOMS:22;
hence dist(p,b) < r by A16,AXIOMS:22;
case B1 < 0 & B2 < 0;
then abs(B1) <= abs(w) & abs(B2) <= abs(s) by A4,Th8;
then abs(B1) + abs(B2) <= abs(w) + abs(s) by REAL_1:55;
then A18:   dist(p,b) <= abs(w) + abs(s) by A6,A7,AXIOMS:22;
0 + 0 <= abs(e) + abs(n) by A10,A11,REAL_1:55;
then 0 + (abs(w) + abs(s)) <= abs(e) + abs(n) + (abs(w) + abs(s))
by REAL_1:55;
then abs(w) + abs(s) <= abs(e) + abs(n) + abs(w) + abs(s) by XCMPLX_1:1;
then abs(w) + abs(s) < r by A12,AXIOMS:22;
hence dist(p,b) < r by A18,AXIOMS:22;
end;
hence x in Ball(p,r) by METRIC_1:12;
end;

theorem Th61:
for M being Reflexive symmetric triangle (non empty MetrStruct),
z being Point of M holds
r < 0 implies Sphere(z,r) = {}
proof
let M be Reflexive symmetric triangle (non empty MetrStruct),
z be Point of M;
assume
A1:   r < 0;
thus Sphere(z,r) c= {}
proof
let a be set;
assume
A2:     a in Sphere(z,r);
then reconsider b = a as Point of M;
dist(b,z) = r by A2,METRIC_1:14;
hence a in {} by A1,METRIC_1:5;
end;
thus thesis by XBOOLE_1:2;
end;

theorem
for M being Reflexive discerning (non empty MetrStruct),
z being Point of M holds
Sphere(z,0) = {z}
proof
let M be Reflexive discerning (non empty MetrStruct),
z be Point of M;
thus Sphere(z,0) c= {z}
proof
let a be set;
assume
A1:     a in Sphere(z,0);
then reconsider b = a as Point of M;
dist(z,b) = 0 by A1,METRIC_1:14;
then b = z by METRIC_1:2;
hence a in {z} by TARSKI:def 1;
end;
let a be set;
assume a in {z};
then A2: a = z by TARSKI:def 1;
dist(z,z) = 0 by METRIC_1:1;
hence thesis by A2,METRIC_1:14;
end;

theorem Th63:
for M being Reflexive symmetric triangle (non empty MetrStruct),
z being Point of M holds
r < 0 implies cl_Ball(z,r) = {}
proof
let M be Reflexive symmetric triangle (non empty MetrStruct),
z be Point of M;
assume r < 0;
then A1: Ball(z,r) = {} & Sphere(z,r) = {} by Th61,TBSP_1:17;
Sphere(z,r) \/ Ball(z,r) = cl_Ball(z,r) by METRIC_1:17;
hence cl_Ball(z,r) = {} by A1;
end;

theorem Th64:
cl_Ball(z,0) = {z}
proof
thus cl_Ball(z,0) c= {z}
proof
let a be set;
assume
A1:     a in cl_Ball(z,0);
then reconsider b = a as Point of M;
dist(b,z) <= 0 & dist(b,z) >= 0 by A1,METRIC_1:5,13;
then dist(b,z) = 0;
then b = z by METRIC_1:2;
hence a in {z} by TARSKI:def 1;
end;
let a be set;
assume a in {z};
then A2: a = z by TARSKI:def 1;
dist(z,z) = 0 by METRIC_1:1;
hence thesis by A2,METRIC_1:13;
end;

Lm3:
for A being Subset of TopSpaceMetr M st A = cl_Ball(z,r) holds
A is open
proof
let A be Subset of TopSpaceMetr M such that
A1:   A = cl_Ball(z,r);
for x being set holds x in A iff
ex Q being Subset of TopSpaceMetr M st Q is open & Q c= A & x in Q
proof
let x be set;
thus x in A implies ex Q being Subset of TopSpaceMetr M st
Q is open & Q c= A & x in Q
proof
assume
A2:       x in A;
then reconsider e = x as Point of M by TOPMETR:16;
the carrier of M = the carrier of TopSpaceMetr M by TOPMETR:16;
then reconsider Q = Ball(e,dist(e,z)-r) as Subset of TopSpaceMetr M
;
take Q;
thus Q is open by TOPMETR:21;
thus Q c= A
proof
let q be set;
assume
A3:         q in Q;
then reconsider f = q as Point of M;
A4:       dist(e,f) < dist(e,z)-r by A3,METRIC_1:12;
dist(e,z) <= dist(e,f) + dist(f,z) by METRIC_1:4;
then dist(e,z) - r <= dist(e,f) + dist(f,z) - r by REAL_1:49;
then dist(e,f) < dist(e,f) + dist(f,z) - r by A4,AXIOMS:22;
then dist(e,f) - dist(e,f) < dist(e,f) + dist(f,z) - r - dist(e,f)
by REAL_1:54;
then 0 < dist(e,f) + dist(f,z) - r - dist(e,f) by XCMPLX_1:14;
then 0 < dist(e,f) + dist(f,z) - dist(e,f) - r by XCMPLX_1:21;
then 0 < dist(e,f) - dist(e,f) + dist(f,z) - r by XCMPLX_1:29;
then 0 < 0 + dist(f,z) - r by XCMPLX_1:14;
then dist(f,z) > r by REAL_2:106;
then not q in A by A1,METRIC_1:13;
then q in A by A3,SUBSET_1:50;
hence thesis;
end;
x in A by A2;
then not x in A by SUBSET_1:54;
then dist(z,e) > r by A1,METRIC_1:13;
then dist(e,z)-r > r-r by REAL_1:54;
then dist(e,z)-r > 0 by XCMPLX_1:14;
hence x in Q by TBSP_1:16;
end;
thus thesis;
end;
hence A is open by TOPS_1:57;
end;

theorem Th65:
for A being Subset of TopSpaceMetr M st A = cl_Ball(z,r) holds
A is closed
proof
let A be Subset of TopSpaceMetr M;
assume A = cl_Ball(z,r);
then A is open by Lm3;
hence A is closed by TOPS_1:29;
end;

theorem Th66:
A = cl_Ball(w,r) implies A is closed
proof
TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
hence thesis by Th65;
end;

theorem Th67:
cl_Ball(z,r) is bounded
proof
per cases;
suppose
A1:   r > 0;
take r+1,z;
r+1 > 0+1 by A1,REAL_1:53;
hence 0 < r+1 by AXIOMS:22;
let a be set;
assume
A2:   a in cl_Ball(z,r);
then reconsider e = a as Point of M;
A3: dist(e,z) <= r by A2,METRIC_1:13;
r+0 < r+1 by REAL_1:53;
then dist(e,z) < r+1 by A3,AXIOMS:22;
hence a in Ball(z,r+1) by METRIC_1:12;
suppose
A4:   r < 0;
{}M is bounded by TBSP_1:14;
hence thesis by A4,Th63;
suppose r = 0;
then cl_Ball(z,r) = {z} by Th64;
hence thesis by TBSP_1:22;
end;

theorem Th68:
for A being Subset of TopSpaceMetr M st A = Sphere(z,r) holds A is closed
proof
let A be Subset of TopSpaceMetr M such that
A1:   A = Sphere(z,r);
A2: the carrier of M = the carrier of TopSpaceMetr M by TOPMETR:16;
then reconsider B = cl_Ball(z,r), C = Ball(z,r) as Subset of TopSpaceMetr M
;
A3: (cl_Ball(z,r)) = B by A2;
A4: A = B \/ C
proof
hereby
let a be set;
assume
A5:       a in A;
then reconsider e = a as Point of M by TOPMETR:16;
a in A by A5;
then not a in A by SUBSET_1:54;
then dist(e,z) <> r by A1,METRIC_1:14;
then dist(e,z) < r or dist(e,z) > r by REAL_1:def 5;
then e in Ball(z,r) or not e in
cl_Ball(z,r) by METRIC_1:12,13;
then e in Ball(z,r) or e in cl_Ball(z,r) by SUBSET_1:50;
then e in Ball(z,r) or e in (cl_Ball(z,r));
hence a in B \/ C by A3,XBOOLE_0:def 2;
end;
let a be set;
assume
A6:     a in B \/ C;
then reconsider e = a as Point of M by TOPMETR:16;
a in B or a in C by A6,XBOOLE_0:def 2;
then e in cl_Ball(z,r) or e in C by A3;
then not e in cl_Ball(z,r) or e in C by SUBSET_1:54;
then dist(e,z) > r or dist(e,z) < r by METRIC_1:12,13;
then not a in A by A1,METRIC_1:14;
then a in A by A6,SUBSET_1:50;
hence a in A;
end;
B is open & C is open by Lm3,TOPMETR:21;
then A is open by A4,TOPS_1:37;
hence A is closed by TOPS_1:29;
end;

theorem
A = Sphere(w,r) implies A is closed
proof
TOP-REAL n = TopSpaceMetr Euclid n by EUCLID:def 8;
hence thesis by Th68;
end;

theorem
Sphere(z,r) is bounded
proof
A1: Sphere(z,r) c= cl_Ball(z,r) by METRIC_1:16;
cl_Ball(z,r) is bounded by Th67;
hence thesis by A1,TBSP_1:21;
end;

theorem Th71:
A is Bounded implies Cl A is Bounded
proof
given C being Subset of Euclid n such that
A1:   C = A and
A2:   C is bounded;
consider r being Real, x being Point of Euclid n such that
0 < r and
A3:   C c= Ball(x,r) by A2,METRIC_6:def 10;
A4: Ball(x,r) c= cl_Ball(x,r) by METRIC_1:15;
Cl A is Subset of Euclid n by TOPREAL3:13;
then reconsider D = Cl A as Subset of Euclid n;
take D;
thus D = Cl A;
cl_Ball(x,r) is Subset of TOP-REAL n by TOPREAL3:13;
then reconsider B = cl_Ball(x,r) as Subset of TOP-REAL n;
A5: B is closed by Th66;
A6: cl_Ball(x,r) is bounded by Th67;
A c= B by A1,A3,A4,XBOOLE_1:1;
then Cl A c= Cl B by PRE_TOPC:49;
then Cl A c= B by A5,PRE_TOPC:52;
hence D is bounded by A6,TBSP_1:21;
end;

theorem
for M being non empty MetrStruct holds
M is bounded iff
for X being Subset of M holds X is bounded
proof
let M be non empty MetrStruct;
hereby
assume M is bounded;
then A1:   [#]M is bounded by TBSP_1:25;
let X be Subset of M;
X c= [#]M by PRE_TOPC:14;
hence X is bounded by A1,TBSP_1:21;
end;
assume for X being Subset of M holds X is bounded;
then [#]M is bounded;
hence thesis by TBSP_1:25;
end;

theorem Th73:
for M being Reflexive symmetric triangle (non empty MetrStruct),
X, Y being Subset of M st
the carrier of M = X \/ Y & M is non bounded & X is bounded
holds Y is non bounded
proof
let M be Reflexive symmetric triangle (non empty MetrStruct),
X, Y be Subset of M such that
A1:   the carrier of M = X \/ Y and
A2:   M is non bounded;
A3: [#]M = X \/ Y by A1,PRE_TOPC:12;
assume X is bounded & Y is bounded;
then [#]M is bounded by A3,TBSP_1:20;
hence thesis by A2,TBSP_1:25;
end;

theorem
for X, Y being Subset of TOP-REAL n st
n >= 1 & the carrier of TOP-REAL n = X \/ Y & X is Bounded holds
Y is non Bounded
proof
set M = TOP-REAL n;
let X, Y be Subset of M such that
A1:   n >= 1 and
A2:   the carrier of M = X \/ Y;
assume X is Bounded;
then consider C being Subset of Euclid n such that
A3:   C = X & C is bounded by JORDAN2C:def 2;
reconsider D = Y as Subset of Euclid n by TOPREAL3:13;
A4: the carrier of Euclid n = C \/ D by A2,A3,TOPREAL3:13;
[#]M is Subset of Euclid n by TOPREAL3:13;
then reconsider E = [#]M as Subset of Euclid n;
A5: E = the carrier of M by PRE_TOPC:def 3
.= the carrier of Euclid n by TOPREAL3:13
.= [#]Euclid n by PRE_TOPC:def 3;
[#](TOP-REAL n) is non Bounded by A1,JORDAN2C:41;
then E is non bounded by JORDAN2C:def 2;
then Euclid n is non bounded by A5,TBSP_1:25;
then for D being Subset of Euclid n holds
D <> Y or D is non bounded by A3,A4,Th73;
hence thesis by JORDAN2C:def 2;
end;

canceled;

theorem
A is Bounded & B is Bounded implies A \/ B is Bounded
proof
given C being Subset of Euclid n such that
A1:   C = A & C is bounded;
given D being Subset of Euclid n such that
A2:   D = B & D is bounded;
reconsider E = C \/ D as Subset of Euclid n;
take E;
thus thesis by A1,A2,TBSP_1:20;
end;

begin  :: Topological properties of real numbers subsets

definition let X be non empty Subset of REAL;
cluster Cl X -> non empty;
coherence
proof
X c= Cl X by PSCOMP_1:33;
hence thesis by XBOOLE_1:3;
end;
end;

definition let D be bounded_below Subset of REAL;
cluster Cl D -> bounded_below;
coherence
proof
consider p being real number such that
A1:   for r being real number st r in D holds p <= r by SEQ_4:def 2;
take p;
let r be real number;
assume r in Cl D;
then consider s being Real_Sequence such that
A2:   rng s c= D and
A3:   s is convergent & lim s = r by PSCOMP_1:39;
for n holds s.n >= p
proof
let n;
dom s = NAT by FUNCT_2:def 1;
then s.n in rng s by FUNCT_1:def 5;
hence s.n >= p by A1,A2;
end;
hence p <= r by A3,PREPOWER:2;
end;
end;

definition let D be bounded_above Subset of REAL;
cluster Cl D -> bounded_above;
coherence
proof
consider p being real number such that
A1:   for r being real number st r in D holds r <= p by SEQ_4:def 1;
take p;
let r be real number;
assume r in Cl D;
then consider s being Real_Sequence such that
A2:   rng s c= D and
A3:   s is convergent & lim s = r by PSCOMP_1:39;
for n holds s.n <= p
proof
let n;
dom s = NAT by FUNCT_2:def 1;
then s.n in rng s by FUNCT_1:def 5;
hence s.n <= p by A1,A2;
end;
hence p >= r by A3,PREPOWER:3;
end;
end;

theorem Th77:
for D being non empty bounded_below Subset of REAL holds inf D = inf Cl D
proof
let D be non empty bounded_below Subset of REAL;
D c= Cl D by PSCOMP_1:33;
then A1: inf Cl D <= inf D by PSCOMP_1:12;
A2: for p being real number st p in D holds p >= inf Cl D
proof
let p be real number;
assume p in D;
then inf D <= p by SEQ_4:def 5;
hence thesis by A1,AXIOMS:22;
end;
for q being real number st
for p being real number st p in D holds p >= q
holds inf Cl D >= q
proof
let q be real number such that
A3:     for p being real number st p in D holds p >= q;
for p being real number st p in Cl D holds p >= q
proof
let p be real number; assume
p in Cl D;
then consider s being Real_Sequence such that
A4:       rng s c= D and
A5:       s is convergent & lim s = p by PSCOMP_1:39;
for n holds s.n >= q
proof
let n;
dom s = NAT by FUNCT_2:def 1;
then s.n in rng s by FUNCT_1:def 5;
hence s.n >= q by A3,A4;
end;
hence p >= q by A5,PREPOWER:2;
end;
hence inf Cl D >= q by PSCOMP_1:8;
end;
hence thesis by A2,PSCOMP_1:9;
end;

theorem Th78:
for D being non empty bounded_above Subset of REAL holds sup D = sup Cl D
proof
let D be non empty bounded_above Subset of REAL;
D c= Cl D by PSCOMP_1:33;
then A1: sup Cl D >= sup D by PSCOMP_1:13;
A2: for p being real number st p in D holds p <= sup Cl D
proof
let p be real number;
assume p in D;
then sup D >= p by SEQ_4:def 4;
hence thesis by A1,AXIOMS:22;
end;
for q being real number st
for p being real number st p in D holds p <= q
holds sup Cl D <= q
proof
let q be real number such that
A3:     for p being real number st p in D holds p <= q;
for p being real number st p in Cl D holds p <= q
proof
let p be real number; assume
p in Cl D;
then consider s being Real_Sequence such that
A4:       rng s c= D and
A5:       s is convergent & lim s = p by PSCOMP_1:39;
for n holds s.n <= q
proof
let n;
dom s = NAT by FUNCT_2:def 1;
then s.n in rng s by FUNCT_1:def 5;
hence s.n <= q by A3,A4;
end;
hence p <= q by A5,PREPOWER:3;
end;
hence sup Cl D <= q by PSCOMP_1:10;
end;
hence thesis by A2,PSCOMP_1:11;
end;

definition
cluster R^1 -> being_T2;
coherence by PCOMPS_1:38,TOPMETR:def 7;
end;

Lm4:
R^1 = TopStruct (#the carrier of RealSpace,Family_open_set RealSpace#)
by PCOMPS_1:def 6,TOPMETR:def 7;

theorem Th79:
for A being Subset of REAL, B being Subset of R^1 st A = B holds
A is closed iff B is closed
proof
let A be Subset of REAL,
B be Subset of R^1 such that
A1:   A = B;
thus A is closed implies B is closed
proof
assume A is closed;
then A is closed;
then A is open by RCOMP_1:def 5;
then A in Family_open_set RealSpace by JORDAN5A:6;
then B in the topology of R^1 by A1,Lm4,TOPMETR:24;
then [#]R^1 \ B in the topology of R^1 by PRE_TOPC:17;
hence [#]R^1 \ B is open by PRE_TOPC:def 5;
end;
assume B is closed;
then B is open by TOPS_1:29;
then B in the topology of R^1 by PRE_TOPC:def 5;
then B in the topology of R^1;
then A is open by A1,Lm4,JORDAN5A:6,TOPMETR:24;
then A is closed by RCOMP_1:def 5;
hence A is closed;
end;

theorem
for A being Subset of REAL, B being Subset of R^1 st A = B holds Cl A = Cl B
proof
let A be Subset of REAL,
B be Subset of R^1 such that
A1:   A = B;
thus Cl A c= Cl B
proof
let a be set;
assume
A2:     a in Cl A;
for G being Subset of R^1 st G is open & a in G holds B meets G
proof
let G be Subset of R^1 such that
A3:       G is open and
A4:       a in G;
A5:     G in Family_open_set RealSpace by A3,Lm4,PRE_TOPC:def 5;
reconsider H = G as Subset of REAL by TOPMETR:24;
H is open by A5,JORDAN5A:6;
then A /\ H is non empty by A2,A4,PSCOMP_1:38;
hence B meets G by A1,XBOOLE_0:def 7;
end;
hence a in Cl B by A2,PRE_TOPC:def 13,TOPMETR:24;
end;
let a be set;
assume
A6:   a in Cl B;
for O being open Subset of REAL st a in O holds O /\ A is non empty
proof
let O be open Subset of REAL such that
A7:     a in O;
reconsider P = O as Subset of R^1 by TOPMETR:24;
P in Family_open_set RealSpace by JORDAN5A:6;
then P is open by Lm4,PRE_TOPC:def 5;
then P meets B by A6,A7,PRE_TOPC:def 13;
hence O /\ A is non empty by A1,XBOOLE_0:def 7;
end;
hence thesis by A6,PSCOMP_1:38,TOPMETR:24;
end;

theorem Th81:
for A being Subset of REAL, B being Subset of R^1 st A = B holds
A is compact iff B is compact
proof
let A be Subset of REAL,
B be Subset of R^1 such that
A1:   A = B;
thus A is compact implies B is compact
proof
assume
A2:     A is compact;
per cases;
suppose A = {};
then reconsider C = B as empty Subset of R^1 by A1;
C is compact;
hence B is compact;
suppose
A3:     A <> {};
reconsider X = [.inf A,sup A.] as Subset of R^1
by TOPMETR:24;
A is closed by A2,RCOMP_1:26;
then A4:   B is closed by A1,Th79;
A5:   A is bounded by A2,RCOMP_1:28;
then A6:   A c= [.inf A,sup A.] by Th24;
A7:   inf A <= sup A by A3,A5,SEQ_4:24;
then A8:   Closed-Interval-TSpace(inf A,sup A) is compact by HEINE:11;
A9:   X = {} or X <> {};
Closed-Interval-TSpace(inf A,sup A) = R^1|X by A7,TOPMETR:26;
then X is compact by A8,A9,COMPTS_1:12;
hence B is compact by A1,A4,A6,COMPTS_1:18;
end;
assume B is compact;
then [#]B is compact by WEIERSTR:19;
hence A is compact by A1,WEIERSTR:def 3;
end;

definition
cluster finite -> compact Subset of REAL;
coherence
proof
let A be Subset of REAL;
assume A is finite;
then reconsider B = A as finite Subset of R^1 by TOPMETR:24;
B is compact;
hence A is compact by Th81;
end;
end;

definition let a, b be real number;
cluster [.a,b.] -> compact;
coherence by RCOMP_1:24;
end;

theorem
for a, b being real number holds a <> b iff Cl ].a,b.[ = [.a,b.]
proof
let a, b be real number;
thus a <> b implies Cl ].a,b.[ = [.a,b.]
proof
assume
A1:   a <> b;
reconsider a1 = a, b1 = b as Real by XREAL_0:def 1;
per cases by A1,REAL_1:def 5;
suppose
A2:   a > b;
hence Cl ].a,b.[ = {} by PSCOMP_1:35,RCOMP_1:12
.= [.a,b.] by A2,RCOMP_1:13;
suppose
A3:   a < b;
A4: [.a,b.] is closed by RCOMP_1:26;
].a,b.[ c= [.a,b.] by RCOMP_1:15;
hence Cl ].a,b.[ c= [.a,b.] by A4,PSCOMP_1:32;
A5: [.a,b.] = {w where w is Real : a <= w & w <= b } by RCOMP_1:def 1;
A6: ].a,b.[ = {w where w is Real : a < w & w < b } by RCOMP_1:def 2;
let p be set;
assume p in [.a,b.];
then consider r such that
A7:   p = r and
A8:   a <= r & r <= b by A5;
a1 < (a1+b1)/2 & (a1+b1)/2 < b1 by A3,TOPREAL3:3;
then A9: (a1+b1)/2 in ].a1,b1.[ by A6;
now per cases by A8,REAL_1:def 5;
case a < r & r < b;
then A10: r in ].a,b.[ by A6;
].a,b.[ c= Cl ].a,b.[ by PSCOMP_1:33;
hence p in Cl ].a,b.[ by A7,A10;
case
A11:   a = r;
for O being open Subset of REAL st a in O holds O /\ ].a,b.[ is non empty
proof
let O be open Subset of REAL;
assume a in O;
then consider g being real number such that
A12:     0 < g and
A13:     ].a-g,a+g.[ c= O by RCOMP_1:40;
reconsider g as Real by XREAL_0:def 1;
A14:  ].a-g,a+g.[ = {w where w is Real : a-g < w & w < a+g } by RCOMP_1:def 2;
A15:  a-g < a-0 by A12,REAL_1:92;
per cases;
suppose
A16:     a+g < b;
A17:   a+0 < a+g by A12,REAL_1:53;
then A18:   a1 < (a1+(a1+g))/2 by TOPREAL3:3;
then A19:   a-g < (a+(a+g))/2 by A15,AXIOMS:22;
A20:   (a1+(a1+g))/2 < a1+g by A17,TOPREAL3:3;
then A21:   (a1+(a1+g))/2 in ].a1-g,a1+g.[ by A14,A19;
(a+(a+g))/2 < b by A16,A20,AXIOMS:22;
then (a1+(a1+g))/2 in ].a1,b1.[ by A6,A18;
hence O /\ ].a,b.[ is non empty by A13,A21,XBOOLE_0:def 3;
suppose
A22:     a+g >= b;
a1 < (a1+b1)/2 by A3,TOPREAL3:3;
then A23:  a-g < (a+b)/2 by A15,AXIOMS:22;
(a1+b1)/2 < b1 by A3,TOPREAL3:3;
then (a+b)/2 < a+g by A22,AXIOMS:22;
then (a1+b1)/2 in ].a1-g,a1+g.[ by A14,A23;
hence O /\ ].a,b.[ is non empty by A9,A13,XBOOLE_0:def 3;
end;
hence p in Cl ].a,b.[ by A7,A11,PSCOMP_1:38;
case
A24:   b = r;
for O being open Subset of REAL st b in O holds O /\ ].a,b.[ is non empty
proof
let O be open Subset of REAL;
assume b in O;
then consider g being real number such that
A25:     0 < g and
A26:     ].b-g,b+g.[ c= O by RCOMP_1:40;
reconsider g as Real by XREAL_0:def 1;
A27:   ].b-g,b+g.[ = {w where w is Real : b-g < w & w < b+g } by RCOMP_1:def 2;
A28:   b-g < b-0 by A25,REAL_1:92;
A29:   b+0 < b+g by A25,REAL_1:53;
per cases;
suppose
A30:     b-g > a;
A31:   b1-g < (b1+(b1-g))/2 by A28,TOPREAL3:3;
then A32:   a < (b+(b-g))/2 by A30,AXIOMS:22;
(b1+(b1-g))/2 < b1 by A28,TOPREAL3:3;
then (b+(b-g))/2 < b+g by A29,AXIOMS:22;
then A33:  (b1+(b1-g))/2 in ].b1-g,b1+g.[ by A27,A31;
(b1+(b1-g))/2 < b1 by A28,TOPREAL3:3;
then (b1+(b1-g))/2 in ].a1,b1.[ by A6,A32;
hence O /\ ].a,b.[ is non empty by A26,A33,XBOOLE_0:def 3;
suppose
A34:     b-g <= a;
a1 < (a1+b1)/2 by A3,TOPREAL3:3;
then A35:   b-g < (a+b)/2 by A34,AXIOMS:22;
(a1+b1)/2 < b1 by A3,TOPREAL3:3;
then (a+b)/2 < b+g by A29,AXIOMS:22;
then (a1+b1)/2 in ].b1-g,b1+g.[ by A27,A35;
hence O /\ ].a,b.[ is non empty by A9,A26,XBOOLE_0:def 3;
end;
hence p in Cl ].a,b.[ by A7,A24,PSCOMP_1:38;
end;
hence thesis;
end;
assume that
A36:   Cl ].a,b.[ = [.a,b.] and
A37:   a = b;
[.a,b.] = {a} by A37,RCOMP_1:14;
end;

definition
cluster non empty finite bounded Subset of REAL;
existence
proof
reconsider a = {0} as finite Subset of REAL;
take a;
thus thesis by RCOMP_1:28;
end;
end;

theorem Th83:
for T being TopStruct, f being RealMap of T, g being map of T, R^1 st f = g
holds
f is continuous iff g is continuous
proof
let T be TopStruct,
f be RealMap of T,
g be map of T, R^1 such that
A1:   f = g;
thus f is continuous implies g is continuous
proof
assume
A2:     for Y being Subset of REAL st Y is closed holds f"Y is closed;
let P be Subset of R^1 such that
A3:     P is closed;
reconsider R = P as Subset of REAL by TOPMETR:24;
R is closed by A3,Th79;
hence g"P is closed by A1,A2;
end;
assume
A4:   for Y being Subset of R^1 st Y is closed holds g"Y is closed;
let P be Subset of REAL such that
A5:   P is closed;
reconsider R = P as Subset of R^1 by TOPMETR:24;
R is closed by A5,Th79;
hence f"P is closed by A1,A4;
end;

theorem Th84:
for A, B being Subset of REAL,
f being map of [:R^1,R^1:], TOP-REAL 2 st
for x, y being Real holds f. [x,y] = <*x,y*> holds
f.:[:A,B:] = product ((1,2) --> (A,B))
proof
let A, B be Subset of REAL,
f be map of [:R^1,R^1:], TOP-REAL 2 such that
A1:   for x, y being Real holds f. [x,y] = <*x,y*>;
set h = (1,2) --> (A,B);
A2: dom h = {1,2} by FUNCT_4:65;
A3: h.1 = A & h.2 = B by FUNCT_4:66;
thus f.:[:A,B:] c= product h
proof
let x be set;
assume x in f.:[:A,B:];
then consider a being set such that
A4:     a in the carrier of [:R^1,R^1:] and
A5:     a in [:A,B:] and
A6:     f.a = x by FUNCT_2:115;
reconsider a as Point of [:R^1,R^1:] by A4;
consider m, n being set such that
A7:     m in A & n in B and
A8:     a = [m,n] by A5,ZFMISC_1:def 2;
reconsider m, n as Real by A7;
A9:   |[m,n]| = <*m,n*> by EUCLID:def 16;
f.a = x by A6;
then reconsider g = x as Function of Seg 2, REAL by EUCLID:26;
A10:   dom g = dom h by A2,FINSEQ_1:4,FUNCT_2:def 1;
for y being set st y in dom h holds g.y in h.y
proof
let y be set;
assume y in dom h;
then A11:     y = 1 or y = 2 by A2,TARSKI:def 2;
A12:     f. [m,n] = |[m,n]| by A1,A9;
|[m,n]|1 = m & |[m,n]|2 = n by EUCLID:56;
hence g.y in h.y by A3,A6,A7,A8,A9,A11,A12,EUCLID:def 14,def 15;
end;
hence thesis by A10,CARD_3:18;
end;
let a be set;
assume a in product h;
then consider g being Function such that
A13:   a = g and
A14:   dom g = dom h and
A15:   for x being set st x in dom h holds g.x in h.x by CARD_3:def 5;
1 in dom h & 2 in dom h by A2,TARSKI:def 2;
then A16: g.1 in A & g.2 in B by A3,A15;
then A17: [g.1,g.2] in [:A,B:] by ZFMISC_1:106;
A18: dom <*g.1,g.2*> = {1,2} by FINSEQ_1:4,FINSEQ_3:29;
now
let k be set;
assume k in dom g;
then k = 1 or k = 2 by A2,A14,TARSKI:def 2;
hence g.k = <*g.1,g.2*>.k by FINSEQ_1:61;
end;
then A19: a = <*g.1,g.2*> by A2,A13,A14,A18,FUNCT_1:9;
the carrier of [:R^1,R^1:] = [:the carrier of R^1,the carrier of R^1:]
by BORSUK_1:def 5;
then A20: [g.1,g.2] in the carrier of [:R^1,R^1:] by A16,TOPMETR:24,ZFMISC_1:
106;
f. [g.1,g.2] = <*g.1,g.2*> by A1,A16;
hence a in f.:[:A,B:] by A17,A19,A20,FUNCT_2:43;
end;

theorem Th85:
for f being map of [:R^1,R^1:], TOP-REAL 2 st
for x, y being Real holds f. [x,y] = <*x,y*> holds
f is_homeomorphism
proof
let f be map of [:R^1,R^1:], TOP-REAL 2 such that
A1:   for x, y being Real holds f. [x,y] = <*x,y*>;
A2: the carrier of [:R^1,R^1:] = [:the carrier of R^1,the carrier of R^1:]
by BORSUK_1:def 5;
then A3: dom f = [:the carrier of R^1,the carrier of R^1:] by FUNCT_2:def 1;
hence dom f = [:[#]R^1,the carrier of R^1:] by PRE_TOPC:12
.= [:[#]R^1,[#]R^1:] by PRE_TOPC:12
.= [#][:R^1,R^1:] by BORSUK_3:1;
thus
A4:   rng f = [#]TOP-REAL 2
proof
rng f c= the carrier of TOP-REAL 2;
hence rng f c= [#]TOP-REAL 2 by PRE_TOPC:12;
let y be set;
assume y in [#]TOP-REAL 2;
then consider a, b such that
A5:     y = <*a,b*> by EUCLID:55;
A6:   [a,b] in dom f by A3,TOPMETR:24,ZFMISC_1:106;
f. [a,b] = <*a,b*> by A1;
hence y in rng f by A5,A6,FUNCT_1:def 5;
end;
thus
A7:   f is one-to-one
proof
let x, y be set;
assume x in dom f;
then consider x1, x2 being set such that
A8:     x1 in REAL & x2 in REAL and
A9:     x = [x1,x2] by A3,TOPMETR:24,ZFMISC_1:def 2;
assume y in dom f;
then consider y1, y2 being set such that
A10:     y1 in REAL & y2 in REAL and
A11:     y = [y1,y2] by A3,TOPMETR:24,ZFMISC_1:def 2;
reconsider x1, x2, y1, y2 as Real by A8,A10;
A12:   f. [x1,x2] = <*x1,x2*> & f. [y1,y2] = <*y1,y2*> by A1;
assume f.x = f.y;
then x1 = y1 & x2 = y2 by A9,A11,A12,GROUP_7:2;
hence x = y by A9,A11;
end;
thus f is continuous
proof
let w be Point of [:R^1,R^1:],
G be a_neighborhood of f.w;
consider x, y being set such that
A13:     x in the carrier of R^1 & y in the carrier of R^1 and
A14:     w = [x,y] by A2,ZFMISC_1:def 2;
reconsider x, y as Real by A13,TOPMETR:24;
reconsider fw = f.w as Point of Euclid 2 by TOPREAL3:13;
fw in Int G by CONNSP_2:def 1;
then consider r being real number such that
A15:     r > 0 and
A16:     Ball(fw,r) c= G by GOBOARD6:8;
reconsider r as Real by XREAL_0:def 1;
set A = ].(f.w)1-r/sqrt 2,(f.w)1+r/sqrt 2.[,
B = ].(f.w)2-r/sqrt 2,(f.w)2+r/sqrt 2.[;
reconsider A, B as Subset of R^1 by TOPMETR:24;
take [:A,B:];
thus [:A,B:] is a_neighborhood of w
proof
A17:     Base-Appr [:A,B:] = { [:X1,Y1:] where X1, Y1 is Subset of R^1 :
[:X1,Y1:] c= [:A,B:] & X1 is open & Y1 is open} by BORSUK_1:def 6;
A is open & B is open by JORDAN6:46;
then A18:     [:A,B:] in Base-Appr [:A,B:] by A17;
A19:     r/sqrt 2 > 0 by A15,Lm1,REAL_2:127;
f. [x,y] = <*x,y*> by A1;
then f. [x,y] = |[x,y]| by EUCLID:def 16;
then x = (f.w)1 & y = (f.w)2 by A14,EUCLID:56;
then x in A & y in B by A19,Th20;
then w in [:A,B:] by A14,ZFMISC_1:106;
then w in union Base-Appr [:A,B:] by A18,TARSKI:def 4;
hence w in Int [:A,B:] by BORSUK_1:55;
end;
product ((1,2)-->(A,B)) c= Ball(fw,r) by Th49;
then f.:[:A,B:] c= Ball(fw,r) by A1,Th84;
hence f.:[:A,B:] c= G by A16,XBOOLE_1:1;
end;
A20: dom (f") = [#]TOP-REAL 2 by A4,A7,TOPS_2:62
.= the carrier of TOP-REAL 2 by PRE_TOPC:12;
reconsider f1 = proj1, f2 = proj2 as map of TOP-REAL 2, R^1 by TOPMETR:24;
A21: dom <:f1,f2:> = the carrier of TOP-REAL 2 by FUNCT_2:def 1;
now
let x be set;
assume
A22:     x in dom (f");
then consider a, b such that
A23:     x = <*a,b*> by A20,EUCLID:55;
A24:   dom f1 = the carrier of TOP-REAL 2 &
dom f2 = the carrier of TOP-REAL 2 by FUNCT_2:def 1;
A25:   [a,b] in dom f by A3,TOPMETR:24,ZFMISC_1:106;
A26:   f. [a,b] = <*a,b*> by A1;
reconsider p = x as Point of TOP-REAL 2 by A20,A22;
A27:   p = |[a,b]| by A23,EUCLID:def 16;
thus f".x = (f qua Function)".x by A4,A7,TOPS_2:def 4
.= [a,b] by A7,A23,A25,A26,FUNCT_1:54
.= [p1,b] by A27,EUCLID:56
.= [p1,p2] by A27,EUCLID:56
.= [f1.x,p2] by PSCOMP_1:def 28
.= [f1.x,f2.x] by PSCOMP_1:def 29
.= <:f1,f2:>.x by A20,A22,A24,FUNCT_3:69;
end;
then A28: f" = <:f1,f2:> by A20,A21,FUNCT_1:9;
f1 is continuous & f2 is continuous by Th83;
hence f" is continuous by A28,YELLOW12:41;
end;

theorem
[:R^1,R^1:], TOP-REAL 2 are_homeomorphic
proof
defpred P[Element of REAL,Element of REAL,set] means
ex c being Element of REAL 2 st c = $3 &$3 = <*$1,$2*>;
A1: for x, y being Element of REAL
ex u being Element of REAL 2 st P[x,y,u]
proof
let x, y be Element of REAL;
take <*x,y*>;
<*x,y*> in 2-tuples_on REAL by CATALG_1:10;
hence <*x,y*> is Element of REAL 2 by EUCLID:def 1;
hence P[x,y,<*x,y*>];
end;
consider f being Function of [:REAL,REAL:],REAL 2 such that
A2:  for x, y being Element of REAL holds P[x,y,f. [x,y]]
from FuncEx2D(A1);
the carrier of [:R^1,R^1:] = [:the carrier of R^1,the carrier of R^1:] &
the carrier of R^1 = REAL &
the carrier of TOP-REAL 2 = REAL 2
by BORSUK_1:def 5,EUCLID:25,TOPMETR:24;
then reconsider f as map of [:R^1,R^1:], TOP-REAL 2;
take f;
for x, y being Real holds f. [x,y] = <*x,y*>
proof
let x, y be Real;
P[x,y,f. [x,y]] by A2;
hence thesis;
end;
hence thesis by Th85;
end;

begin  :: Bounded subsets

theorem Th87:
for A, B being compact Subset of REAL holds
product ((1,2) --> (A,B)) is compact Subset of TOP-REAL 2
proof
let A, B be compact Subset of REAL;
reconsider A1 = A, B1 = B as Subset of R^1 by TOPMETR:24;
A1 is compact & B1 is compact by Th81;
then A1: [:A1,B1:] is compact by BORSUK_3:27;
reconsider X = product ((1,2) --> (A,B)) as Subset of TOP-REAL 2 by Th30;
defpred P[Element of REAL,Element of REAL,set] means
ex c being Element of REAL 2 st c = $3 &$3 = <*$1,$2*>;
A2: for x, y being Element of REAL
ex u being Element of REAL 2 st P[x,y,u]
proof
let x, y be Element of REAL;
take <*x,y*>;
<*x,y*> in 2-tuples_on REAL by CATALG_1:10;
hence <*x,y*> is Element of REAL 2 by EUCLID:def 1;
hence P[x,y,<*x,y*>];
end;
consider h being Function of [:REAL,REAL:],REAL 2 such that
A3:  for x, y being Element of REAL holds P[x,y,h. [x,y]]
from FuncEx2D(A2);
the carrier of [:R^1,R^1:] = [:the carrier of R^1,the carrier of R^1:] &
the carrier of R^1 = REAL &
the carrier of TOP-REAL 2 = REAL 2
by BORSUK_1:def 5,EUCLID:25,TOPMETR:24;
then reconsider h as map of [:R^1,R^1:], TOP-REAL 2;
A4: for x, y being Real holds h. [x,y] = <*x,y*>
proof
let x, y be Real;
P[x,y,h. [x,y]] by A3;
hence thesis;
end;
then A5: h.:[:A1,B1:] = X by Th84;
h is_homeomorphism by A4,Th85;
then h is continuous by TOPS_2:def 5;
hence thesis by A1,A5,WEIERSTR:14;
end;

theorem Th88:
P is Bounded closed implies P is compact
proof
assume
A1:   P is Bounded closed;
then consider C being Subset of Euclid 2 such that
A2:   C = P and
A3:   C is bounded by JORDAN2C:def 2;
consider r, e such that
0 < r and
A4:   C c= Ball(e,r) by A3,METRIC_6:def 10;
reconsider p = e as Point of TOP-REAL 2 by TOPREAL3:13;
A5: Ball(e,r) c= product ((1,2)-->(].p1-r,p1+r.[,].p2-r,p2+r.[)) by Th50;
].p1-r,p1+r.[ c= [.p1-r,p1+r.] & ].p2-r,p2+r.[ c= [.p2-r,p2+r.]
by RCOMP_1:15;
then product ((1,2)-->(].p1-r,p1+r.[,].p2-r,p2+r.[)) c=
product ((1,2)-->([.p1-r,p1+r.],[.p2-r,p2+r.])) by Th29;
then Ball(e,r) c= product ((1,2)-->([.p1-r,p1+r.],[.p2-r,p2+r.]))
by A5,XBOOLE_1:1;
then A6: P c= product ((1,2)-->([.p1-r,p1+r.],[.p2-r,p2+r.]))
by A2,A4,XBOOLE_1:1;
product ((1,2)-->([.p1-r,p1+r.],[.p2-r,p2+r.])) is compact
Subset of TOP-REAL 2 by Th87;
hence P is compact by A1,A6,COMPTS_1:18;
end;

theorem Th89:
P is Bounded implies
for g being continuous RealMap of TOP-REAL 2 holds Cl(g.:P) c= g.:Cl P
proof
assume
A1:   P is Bounded;
let g be continuous RealMap of TOP-REAL 2;
reconsider f = g as map of TOP-REAL 2, R^1 by TOPMETR:24;
A2: f is continuous by Th83;
Cl P is Bounded by A1,Th71;
then Cl P is compact by Th88;
then f.:Cl P is compact by A2,WEIERSTR:15;
then f.:Cl P is closed by COMPTS_1:16;
then A3: g.:Cl P is closed by Th79;
P c= Cl P by PRE_TOPC:48;
then g.:P c= g.:Cl P by RELAT_1:156;
hence Cl(g.:P) c= g.:Cl P by A3,PSCOMP_1:32;
end;

theorem Th90:
proj1.:Cl P c= Cl(proj1.:P)
proof
let y be set;
assume y in proj1.:Cl P;
then consider x being set such that
A1:   x in the carrier of TOP-REAL 2 and
A2:   x in Cl P and
A3:   y = proj1.x by FUNCT_2:115;
reconsider x as Point of TOP-REAL 2 by A1;
set r = proj1.x;
for O being open Subset of REAL st y in O holds O /\ proj1.:P is non
empty
proof
let O be open Subset of REAL;
assume y in O;
then consider g being real number such that
A4:     0 < g and
A5:     ].r-g,r+g.[ c= O by A3,RCOMP_1:40;
reconsider g as Real by XREAL_0:def 1;
reconsider e = x as Point of Euclid 2 by TOPREAL3:13;
the carrier of TOP-REAL 2 = the carrier of Euclid 2 by TOPREAL3:13;
then reconsider B = Ball(e,g/2) as Subset of TOP-REAL 2;
A6:   B is open by GOBOARD6:6;
g/2 > 0 by A4,REAL_2:127;
then e in B by TBSP_1:16;
then P meets B by A2,A6,TOPS_1:39;
then P /\ B <> {} by XBOOLE_0:def 7;
then consider d being Point of TOP-REAL 2 such that
A7:     d in P /\ B by SUBSET_1:10;
d in P by A7,XBOOLE_0:def 3;
then proj1.d in proj1.:P by FUNCT_2:43;
then A8:   d1 in proj1.:P by PSCOMP_1:def 28;
A9:   ].r-g,r+g.[ = {t where t is Real: r-g < t & t < r+g} by RCOMP_1:def 2;
d in B by A7,XBOOLE_0:def 3;
then x1-g/2 < d1 & d1 < x1+g/2 by Th47;
then A10:   r-g/2 < d1 & d1 < r+g/2 by PSCOMP_1:def 28;
g/2 < g/1 by A4,REAL_2:200;
then r-g < r-g/2 & r+g/2 < r+g by REAL_1:53,92;
then r-g < d1 & d1 < r+g by A10,AXIOMS:22;
then d1 in ].r-g,r+g.[ by A9;
hence thesis by A5,A8,XBOOLE_0:def 3;
end;
hence y in Cl(proj1.:P) by A3,PSCOMP_1:38;
end;

theorem Th91:
proj2.:Cl P c= Cl(proj2.:P)
proof
let y be set;
assume y in proj2.:Cl P;
then consider x being set such that
A1:   x in the carrier of TOP-REAL 2 and
A2:   x in Cl P and
A3:   y = proj2.x by FUNCT_2:115;
reconsider x as Point of TOP-REAL 2 by A1;
set r = proj2.x;
for O being open Subset of REAL st y in O holds O /\ proj2.:P is non
empty
proof
let O be open Subset of REAL;
assume y in O;
then consider g being real number such that
A4:     0 < g and
A5:     ].r-g,r+g.[ c= O by A3,RCOMP_1:40;
reconsider g as Real by XREAL_0:def 1;
reconsider e = x as Point of Euclid 2 by TOPREAL3:13;
the carrier of TOP-REAL 2 = the carrier of Euclid 2 by TOPREAL3:13;
then reconsider B = Ball(e,g/2) as Subset of TOP-REAL 2;
A6:   B is open by GOBOARD6:6;
g/2 > 0 by A4,REAL_2:127;
then e in B by TBSP_1:16;
then P meets B by A2,A6,TOPS_1:39;
then P /\ B <> {} by XBOOLE_0:def 7;
then consider d being Point of TOP-REAL 2 such that
A7:     d in P /\ B by SUBSET_1:10;
d in P by A7,XBOOLE_0:def 3;
then proj2.d in proj2.:P by FUNCT_2:43;
then A8:   d2 in proj2.:P by PSCOMP_1:def 29;
A9:   ].r-g,r+g.[ = {t where t is Real: r-g < t & t < r+g} by RCOMP_1:def 2;
d in B by A7,XBOOLE_0:def 3;
then x2-g/2 < d2 & d2 < x2+g/2 by Th48;
then A10:   r-g/2 < d2 & d2 < r+g/2 by PSCOMP_1:def 29;
g/2 < g/1 by A4,REAL_2:200;
then r-g < r-g/2 & r+g/2 < r+g by REAL_1:53,92;
then r-g < d2 & d2 < r+g by A10,AXIOMS:22;
then d2 in ].r-g,r+g.[ by A9;
hence thesis by A5,A8,XBOOLE_0:def 3;
end;
hence y in Cl(proj2.:P) by A3,PSCOMP_1:38;
end;

theorem Th92:
P is Bounded implies Cl(proj1.:P) = proj1.:Cl P
proof
assume P is Bounded;
hence Cl(proj1.:P) c= proj1.:Cl P by Th89;
thus thesis by Th90;
end;

theorem Th93:
P is Bounded implies Cl(proj2.:P) = proj2.:Cl P
proof
assume P is Bounded;
hence Cl(proj2.:P) c= proj2.:Cl P by Th89;
thus thesis by Th91;
end;

theorem
D is Bounded implies W-bound D = W-bound Cl D
proof
assume
A1:   D is Bounded;
then Cl D is Bounded by Th71;
then A2: Cl D is compact by Th88;
A3: W-bound D = inf (proj1.:D) & W-bound Cl D = inf (proj1.:
Cl D) by SPRECT_1:48;
A4: proj1.:Cl D is bounded_below by A2,SPRECT_1:46;
D c= Cl D by PRE_TOPC:48;
then proj1.:D c= proj1.:Cl D by RELAT_1:156;
then proj1.:D is bounded_below by A4,RCOMP_1:3;
then inf (proj1.:D) = inf Cl(proj1.:D) by Th77
.= inf (proj1.:Cl D) by A1,Th92;
hence thesis by A3;
end;

theorem
D is Bounded implies E-bound D = E-bound Cl D
proof
assume
A1:   D is Bounded;
then Cl D is Bounded by Th71;
then A2: Cl D is compact by Th88;
A3: E-bound D = sup (proj1.:D) & E-bound Cl D = sup (proj1.:
Cl D) by SPRECT_1:51;
A4: proj1.:Cl D is bounded_above by A2,SPRECT_1:47;
D c= Cl D by PRE_TOPC:48;
then proj1.:D c= proj1.:Cl D by RELAT_1:156;
then proj1.:D is bounded_above by A4,RCOMP_1:4;
then sup (proj1.:D) = sup Cl(proj1.:D) by Th78
.= sup (proj1.:Cl D) by A1,Th92;
hence thesis by A3;
end;

theorem
D is Bounded implies N-bound D = N-bound Cl D
proof
assume
A1:   D is Bounded;
then Cl D is Bounded by Th71;
then A2: Cl D is compact by Th88;
A3: N-bound D = sup (proj2.:D) & N-bound Cl D = sup (proj2.:
Cl D) by SPRECT_1:50;
A4: proj2.:Cl D is bounded_above by A2,SPRECT_1:47;
D c= Cl D by PRE_TOPC:48;
then proj2.:D c= proj2.:Cl D by RELAT_1:156;
then proj2.:D is bounded_above by A4,RCOMP_1:4;
then sup (proj2.:D) = sup Cl(proj2.:D) by Th78
.= sup (proj2.:Cl D) by A1,Th93;
hence thesis by A3;
end;

theorem
D is Bounded implies S-bound D = S-bound Cl D
proof
assume
A1:   D is Bounded;
then Cl D is Bounded by Th71;
then A2: Cl D is compact by Th88;
A3: S-bound D = inf (proj2.:D) & S-bound Cl D = inf (proj2.:
Cl D) by SPRECT_1:49;
A4: proj2.:Cl D is bounded_below by A2,SPRECT_1:46;
D c= Cl D by PRE_TOPC:48;
then proj2.:D c= proj2.:Cl D by RELAT_1:156;
then proj2.:D is bounded_below by A4,RCOMP_1:3;
then inf (proj2.:D) = inf Cl(proj2.:D) by Th77
.= inf (proj2.:Cl D) by A1,Th93;
hence thesis by A3;
end;
`