Subset of TOP-REAL 2 equals {p: a <=p`1 & p`1<= b & c <=p`2 & p`2<= d}; coherence proof defpred P[Point of TOP-REAL 2] means a <=$1`1 & $1`1<= b & c <=$1`2 & $1`2<= d; {p: P[p]} c= the carrier of TOP-REAL 2 from FRAENKEL:sch 10; hence thesis; end; end; definition let a,b,c,d be Real; func outside_of_rectangle(a,b,c,d) -> Subset of TOP-REAL 2 equals {p: not(a <=p`1 & p`1<= b & c <=p`2 & p`2<= d)}; coherence proof defpred P[Point of TOP-REAL 2] means not(a <=$1`1 & $1`1<= b & c <=$1`2 & $1`2<= d); {p: P[p] } c= the carrier of TOP-REAL 2 from FRAENKEL:sch 10; hence thesis; end; end; definition let a,b,c,d be Real; func closed_outside_of_rectangle(a,b,c,d) -> Subset of TOP-REAL 2 equals {p: not(a

=0 & Kb={q: |.q.|=1}&
Cb={p2 where p2 is Point of TOP-REAL 2: |.(p2- |[a,b]|).|=r} holds
AffineMap(r,a,r,b).:Kb=Cb
proof
let a,b,r be Real,Kb,Cb be Subset of TOP-REAL 2;
assume
A1: r>=0 & Kb={q: |.q.|=1}&
Cb={p2 where p2 is Point of TOP-REAL 2: |.(p2- |[a,b]|).|=r};
reconsider rr=r as Real;
A2: AffineMap(r,a,r,b).:Kb c= Cb
proof
let y be object;
assume y in AffineMap(r,a,r,b).:Kb;
then consider x being object such that
x in dom (AffineMap(r,a,r,b)) and
A3: x in Kb and
A4: y=(AffineMap(r,a,r,b)).x by FUNCT_1:def 6;
consider p being Point of TOP-REAL 2 such that
A5: x=p and
A6: |.p.|=1 by A1,A3;
A7: (AffineMap(r,a,r,b)).p=|[r*(p`1)+a,r*(p`2)+b]| by JGRAPH_2:def 2;
then reconsider q=y as Point of TOP-REAL 2 by A4,A5;
A8: q- |[a,b]|= |[r*(p`1)+a-a,r*(p`2)+b-b]| by A4,A5,A7,EUCLID:62
.= r*(|[(p`1),(p`2)]|) by EUCLID:58
.= r*p by EUCLID:53;
|.r*p.|=|.rr.|*(|.p.|) by TOPRNS_1:7
.=r by A1,A6,ABSVALUE:def 1;
hence thesis by A1,A8;
end;
Cb c= AffineMap(r,a,r,b).:Kb
proof
let y be object;
assume y in Cb;
then consider p2 being Point of TOP-REAL 2 such that
A9: y=p2 and
A10: |.(p2- |[a,b]|).|=r by A1;
now per cases by A1;
case
A11: r>0;
set p1=(1/r)*(p2- |[a,b]|);
|.p1.|=|.1/rr.|*|.(p2- |[a,b]|).| by TOPRNS_1:7
.=(1/r)*r by A10,ABSVALUE:def 1
.= 1 by A11,XCMPLX_1:87;
then
A12: p1 in Kb by A1;
A13: p1=|[(1/r)*(p2- |[a,b]|)`1,(1/r)*(p2- |[a,b]|)`2]| by EUCLID:57;
then
A14: p1`1=(1/r)*(p2- |[a,b]|)`1 by EUCLID:52;
A15: p1`2=(1/r)*(p2- |[a,b]|)`2 by A13,EUCLID:52;
A16: r*p1`1=r*(1/r)*(p2- |[a,b]|)`1 by A14
.=1*(p2- |[a,b]|)`1 by A11,XCMPLX_1:87
.=p2`1 -(|[a,b]|)`1 by TOPREAL3:3
.=p2`1 - a by EUCLID:52;
A17: r*p1`2=r*(1/r)*(p2- |[a,b]|)`2 by A15
.=1*(p2- |[a,b]|)`2 by A11,XCMPLX_1:87
.=p2`2 -(|[a,b]|)`2 by TOPREAL3:3
.=p2`2 - b by EUCLID:52;
A18: (AffineMap(r,a,r,b)).p1= |[r*(p1`1)+a,r*(p1`2)+b]| by JGRAPH_2:def 2
.=p2 by A16,A17,EUCLID:53;
dom (AffineMap(r,a,r,b))=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
hence thesis by A9,A12,A18,FUNCT_1:def 6;
end;
case
A19: r=0;
set p1= |[1,0]|;
A20: p1`1=1 by EUCLID:52;
p1`2=0 by EUCLID:52;
then |.p1.|=sqrt(1^2+0^2) by A20,JGRAPH_3:1
.=1 by SQUARE_1:22;
then
A21: p1 in Kb by A1;
A22: (AffineMap(r,a,r,b)).p1= |[(0)*(p1`1)+a,(0)*(p1`2)+b]|
by A19,JGRAPH_2:def 2
.=p2 by A10,A19,TOPRNS_1:28;
dom (AffineMap(r,a,r,b))=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
hence thesis by A9,A21,A22,FUNCT_1:def 6;
end;
end;
hence thesis;
end;
hence thesis by A2;
end;
theorem Th21:
for P,Q being Subset of TOP-REAL 2 st
(ex f being Function of (TOP-REAL 2)|P,(TOP-REAL 2)|Q st
f is being_homeomorphism) & P is being_simple_closed_curve holds
Q is being_simple_closed_curve
proof
let P,Q be Subset of TOP-REAL 2;
assume that
A1: ex f being Function of (TOP-REAL 2)|P,(TOP-REAL 2)|Q st f is
being_homeomorphism and
A2: P is being_simple_closed_curve;
consider f being Function of (TOP-REAL 2)|P,(TOP-REAL 2)|Q such that
A3: f is being_homeomorphism by A1;
consider g being Function of (TOP-REAL 2)|R^2-unit_square,
(TOP-REAL 2)|P such that
A4: g is being_homeomorphism by A2,TOPREAL2:def 1;
A5: (|[1,0]|)`1=1 by EUCLID:52;
(|[1,0]|)`2=0 by EUCLID:52;
then
A6: |[1,0]| in R^2-unit_square by A5,TOPREAL1:14;
A7: dom g=[#]((TOP-REAL 2)|R^2-unit_square) by A4,TOPS_2:def 5;
A8: rng g=[#]((TOP-REAL 2)|P) by A4,TOPS_2:def 5;
dom g= R^2-unit_square by A7,PRE_TOPC:def 5;
then
A9: g.(|[1,0]|) in rng g by A6,FUNCT_1:3;
then
A10: g.(|[1,0]|) in P by A8,PRE_TOPC:def 5;
reconsider P1=P as non empty Subset of TOP-REAL 2 by A9;
dom f=[#]((TOP-REAL 2)|P) by A3,TOPS_2:def 5;
then dom f= P by PRE_TOPC:def 5;
then f.(g.(|[1,0]|)) in rng f by A10,FUNCT_1:3;
then reconsider Q1=Q as non empty Subset of TOP-REAL 2;
reconsider f1=f as Function of (TOP-REAL 2)|P1,(TOP-REAL 2)|Q1;
reconsider g1=g as Function of (TOP-REAL 2)|R^2-unit_square,(TOP-REAL 2)|P1;
reconsider h=f1*g1 as Function of (TOP-REAL 2)|R^2-unit_square,
(TOP-REAL 2)|Q1;
h is being_homeomorphism by A3,A4,TOPS_2:57;
hence thesis by TOPREAL2:def 1;
end;
theorem Th22:
for P being Subset of TOP-REAL 2 st
P is being_simple_closed_curve holds P is compact;
theorem Th23:
for a,b,r be Real, Cb being Subset of TOP-REAL 2 st r>0 &
Cb={p where p is Point of TOP-REAL 2: |.(p- |[a,b]|).|=r}
holds Cb is being_simple_closed_curve
proof
let a,b,r be Real, Cb be Subset of TOP-REAL 2;
assume that
A1: r>0 and
A2: Cb={p where p is Point of TOP-REAL 2: |.(p- |[a,b]|).|=r};
A3: (|[r,0]|)`1=r by EUCLID:52;
A4: (|[r,0]|)`2=0 by EUCLID:52;
|.(|[r+a,b]| - |[a,b]|).|=|.(|[r+a,0+b]| - |[a,b]|).|
.=|.(|[r,0]|+|[a,b]|- |[a,b]|).| by EUCLID:56
.= |.(|[r,0]|+(|[a,b]|- |[a,b]|)).| by RLVECT_1:def 3
.=|.|[r,0]|+(0.TOP-REAL 2).| by RLVECT_1:5
.=|.|[r,0]|.| by RLVECT_1:4
.=sqrt(r^2+0^2) by A3,A4,JGRAPH_3:1
.=r by A1,SQUARE_1:22;
then |[r+a,b]| in Cb by A2;
then reconsider Cbb=Cb as non empty Subset of TOP-REAL 2;
set v= |[1,0]|;
A5: v`1=1 by EUCLID:52;
v`2=0 by EUCLID:52;
then |.v.|=sqrt(1^2+0^2) by A5,JGRAPH_3:1
.=1 by SQUARE_1:22;
then
A6: |[1,0]| in {q: |.q.|=1};
defpred P[Point of TOP-REAL 2] means |.$1.|=1;
{q where q is Element of TOP-REAL 2:P[q]}
is Subset of TOP-REAL 2 from DOMAIN_1:sch 7;
then reconsider Kb= {q: |.q.|=1} as non empty Subset of TOP-REAL 2 by A6;
A7: the carrier of (TOP-REAL 2)|Kb=Kb by PRE_TOPC:8;
set SC= AffineMap(r,a,r,b);
A8: SC is one-to-one by A1,JGRAPH_2:44;
A9: dom SC = the carrier of TOP-REAL 2 by FUNCT_2:def 1;
A10: dom (SC|Kb)=(dom SC)/\ Kb by RELAT_1:61
.=the carrier of ((TOP-REAL 2)|Kb) by A7,A9,XBOOLE_1:28;
A11: rng (SC|Kb) c= (SC|Kb).:(the carrier of ((TOP-REAL 2)|Kb))
proof
let u be object;
assume u in rng (SC|Kb);
then ex z being object st ( z in dom ((SC|Kb)))&( u=(SC|Kb).z) by
FUNCT_1:def 3;
hence thesis by A10,FUNCT_1:def 6;
end;
(SC|Kb).: (the carrier of ((TOP-REAL 2)|Kb)) = SC.:Kb by A7,RELAT_1:129
.= Cb by A1,A2,Th20
.=the carrier of (TOP-REAL 2)|Cbb by PRE_TOPC:8;
then reconsider f0=SC|Kb
as Function of (TOP-REAL 2)|Kb, (TOP-REAL 2)|Cbb by A10,A11,FUNCT_2:2;
rng (SC|Kb) c= the carrier of (TOP-REAL 2);
then reconsider f00=f0 as Function
of (TOP-REAL 2)|Kb,TOP-REAL 2 by A10,FUNCT_2:2;
A12: rng f0 = (SC|Kb).: (the carrier of ((TOP-REAL 2)|Kb)) by RELSET_1:22
.= SC.:Kb by A7,RELAT_1:129
.= Cb by A1,A2,Th20;
A13: f0 is one-to-one by A8,FUNCT_1:52;
Kb is compact by Th22,JGRAPH_3:26;
then ex f1 being Function of (TOP-REAL 2)|Kb,(TOP-REAL 2)|Cbb st
f00=f1 & f1 is being_homeomorphism by A12,A13,JGRAPH_1:46,TOPMETR:7;
hence thesis by Th21,JGRAPH_3:26;
end;
definition
let a,b,r be Real;
func circle(a,b,r) -> Subset of TOP-REAL 2 equals
{p where p is Point of TOP-REAL 2: |.p- |[a,b]| .|=r};
coherence
proof
defpred P[Point of TOP-REAL 2] means |.$1- |[a,b]| .|=r;
{p where p is Point of TOP-REAL 2:P[p]}
c= the carrier of TOP-REAL 2 from FRAENKEL:sch 10;
hence thesis;
end;
end;
registration
let a,b,r be Real;
cluster circle(a,b,r) -> compact;
coherence
proof
set Cb = circle(a,b,r);
per cases;
suppose
A1: r < 0;
Cb = {}
proof
hereby
let x be object;
assume x in Cb;
then ex p being Point of TOP-REAL 2 st x = p & |.p- |[a,b]| .| = r;
hence x in {} by A1;
end;
thus thesis;
end;
hence thesis;
end;
suppose r > 0;
hence thesis by Th22,Th23;
end;
suppose
A2: r = 0;
Cb = {|[a,b]|}
proof
hereby
let x be object;
assume x in Cb;
then consider p being Point of TOP-REAL 2 such that
A3: x = p and
A4: |.p- |[a,b]| .| = r;
p = |[a,b]| by A2,A4,TOPRNS_1:28;
hence x in {|[a,b]|} by A3,TARSKI:def 1;
end;
let x be object;
assume x in {|[a,b]|};
then
A5: x = |[a,b]| by TARSKI:def 1;
|. |[a,b]| - |[a,b]| .| = 0 by TOPRNS_1:28;
hence thesis by A2,A5;
end;
hence thesis;
end;
end;
end;
registration
let a,b be Real;
let r be non negative Real;
cluster circle(a,b,r) -> non empty;
coherence
proof
set Cb = circle(a,b,r);
A1: (|[r,0]|)`1=r by EUCLID:52;
A2: (|[r,0]|)`2=0 by EUCLID:52;
|.(|[r+a,b]| - |[a,b]|).|=|.(|[r+a,0+b]| - |[a,b]|).|
.=|.(|[r,0]|+|[a,b]|- |[a,b]|).| by EUCLID:56
.= |.(|[r,0]|+(|[a,b]|- |[a,b]|)).| by RLVECT_1:def 3
.=|.|[r,0]|+(0.TOP-REAL 2).| by RLVECT_1:5
.=|.|[r,0]|.| by RLVECT_1:4
.=sqrt(r^2+0^2) by A1,A2,JGRAPH_3:1
.= r by SQUARE_1:22;
then |[r+a,b]| in Cb;
hence thesis;
end;
end;
definition
let a,b,r be Real;
func inside_of_circle(a,b,r) -> Subset of TOP-REAL 2 equals
{p where p is Point of TOP-REAL 2: |.p- |[a,b]| .| 0.TOP-REAL 2 & (q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
then
A12: Sq_Circ.q=|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2 )]|
by JGRAPH_3:def 1;
A13: (|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|)`1 = q`1/sqrt(1+(q
`2/q`1)^2) by EUCLID:52;
A14: (|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|)`2 = q`2/sqrt(1+(q
`2/q`1)^2) by EUCLID:52;
A15: 1+(q`2/q`1)^2>0 by XREAL_1:34,63;
A16: now
assume
A17: q`1=0;
then q`2=0 by A11;
hence contradiction by A11,A17,EUCLID:53,54;
end;
then
A18: (q`1)^2>0 by SQUARE_1:12;
(q`1)^2<1^2 by A5,A6,SQUARE_1:50;
then
A19: sqrt((q`1)^2)<1 by A18,SQUARE_1:18,27;
|.(|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|).|^2
=((q`1)/sqrt(1+(q`2/(q`1))^2))^2+(q`2/sqrt(1+(q`2/(q`1))^2))^2
by A13,A14,JGRAPH_3:1
.=(q`1)^2/(sqrt(1+(q`2/(q`1))^2))^2+(q`2/sqrt(1+(q`2/(q`1))^2))^2
by XCMPLX_1:76
.=(q`1)^2/(sqrt(1+(q`2/(q`1))^2))^2
+(q`2)^2/(sqrt(1+(q`2/(q`1))^2))^2 by XCMPLX_1:76
.=(q`1)^2/(1+(q`2/q`1)^2)+(q`2)^2/(sqrt(1+(q`2/q`1)^2))^2
by A15,SQUARE_1:def 2
.=(q`1)^2/(1+(q`2/q`1)^2)+(q`2)^2/(1+(q`2/q`1)^2)
by A15,SQUARE_1:def 2
.=((q`1)^2+(q`2)^2)/(1+(q`2/q`1)^2) by XCMPLX_1:62
.=((q`1)^2+(q`2)^2)/(1+(q`2)^2/(q`1)^2) by XCMPLX_1:76
.=((q`1)^2+(q`2)^2)/((q`1)^2/(q`1)^2+(q`2)^2/(q`1)^2)
by A18,XCMPLX_1:60
.=((q`1)^2+(q`2)^2)/(((q`1)^2+(q`2)^2)/(q`1)^2)
by XCMPLX_1:62
.=(q`1)^2*(((q`1)^2+(q`2)^2)/((q`1)^2+(q`2)^2))
by XCMPLX_1:81
.=(q`1)^2*1 by A16,COMPLEX1:1,XCMPLX_1:60
.=(q`1)^2;
then |.(|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|).|<1
by A19,SQUARE_1:22;
hence ex p2 being Point of TOP-REAL 2 st p2=y & |.p2.|<1 by A3,A4,A12;
end;
case
A20: q<>0.TOP-REAL 2 & not(q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
then
A21: Sq_Circ.q=|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2 )]|
by JGRAPH_3:def 1;
A22: (|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|)`1 = q`1/sqrt(1+(q
`1/q`2)^2) by EUCLID:52;
A23: (|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|)`2 = q`2/sqrt(1+(q
`1/q`2)^2) by EUCLID:52;
A24: 1+(q`1/q`2)^2>0 by XREAL_1:34,63;
A25: q`2 <> 0 by A20;
then
A26: (q`2)^2>0 by SQUARE_1:12;
(q`2)^2<1^2 by A7,A8,SQUARE_1:50;
then
A27: sqrt((q`2)^2)<1 by A26,SQUARE_1:18,27;
|.(|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|).|^2
=((q`1)/sqrt(1+(q`1/(q`2))^2))^2+(q`2/sqrt(1+(q`1/(q`2))^2))^2
by A22,A23,JGRAPH_3:1
.=(q`1)^2/(sqrt(1+(q`1/(q`2))^2))^2+(q`2/sqrt(1+(q`1/(q`2))^2))^2
by XCMPLX_1:76
.=(q`1)^2/(sqrt(1+(q`1/(q`2))^2))^2
+(q`2)^2/(sqrt(1+(q`1/(q`2))^2))^2 by XCMPLX_1:76
.=(q`1)^2/(1+(q`1/q`2)^2)+(q`2)^2/(sqrt(1+(q`1/q`2)^2))^2
by A24,SQUARE_1:def 2
.=(q`1)^2/(1+(q`1/q`2)^2)+(q`2)^2/(1+(q`1/q`2)^2)
by A24,SQUARE_1:def 2
.=((q`1)^2+(q`2)^2)/(1+(q`1/q`2)^2) by XCMPLX_1:62
.=((q`1)^2+(q`2)^2)/(1+(q`1)^2/(q`2)^2) by XCMPLX_1:76
.=((q`1)^2+(q`2)^2)/((q`1)^2/(q`2)^2+(q`2)^2/(q`2)^2)
by A26,XCMPLX_1:60
.=((q`1)^2+(q`2)^2)/(((q`1)^2+(q`2)^2)/(q`2)^2)
by XCMPLX_1:62
.=(q`2)^2*(((q`1)^2+(q`2)^2)/((q`1)^2+(q`2)^2))
by XCMPLX_1:81
.=(q`2)^2*1 by A25,COMPLEX1:1,XCMPLX_1:60
.=(q`2)^2;
then |.(|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|).|<1
by A27,SQUARE_1:22;
hence ex p2 being Point of TOP-REAL 2 st p2=y & |.p2.|<1 by A3,A4,A21;
end;
end;
hence thesis by A1;
end;
let y be object;
assume y in Cb;
then consider p2 being Point of TOP-REAL 2 such that
A28: p2=y and
A29: |.p2.|<1 by A1;
set q=p2;
now per cases;
case
A30: q=0.TOP-REAL 2;
then
A31: q`1=0 by EUCLID:52,54;
q`2=0 by A30,EUCLID:52,54;
then
A32: y in Kb by A1,A28,A31;
A33: Sq_Circ".y=y by A28,A30,JGRAPH_3:28;
A34: dom Sq_Circ=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
y=Sq_Circ.y by A28,A33,FUNCT_1:35,JGRAPH_3:43;
hence ex x being set st x in dom Sq_Circ & x in Kb & y=Sq_Circ.x
by A32,A34;
end;
case
A35: q<>0.TOP-REAL 2 & (q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
set px=|[q`1*sqrt(1+(q`2/q`1)^2),q`2*sqrt(1+(q`2/q`1)^2)]|;
A36: px`1 = q`1*sqrt(1+(q`2/q`1)^2) by EUCLID:52;
A37: px`2 = q`2*sqrt(1+(q`2/q`1)^2) by EUCLID:52;
1+(q`2/q`1)^2>0 by XREAL_1:34,63;
then
A38: sqrt(1+(q`2/q`1)^2)>0 by SQUARE_1:25;
A39: 1+(px`2/px`1)^2>0 by XREAL_1:34,63;
A40: px`2/px`1=q`2/q`1 by A36,A37,A38,XCMPLX_1:91;
A41: q`1=q`1*sqrt(1+(q`2/q`1)^2)/(sqrt(1+(q`2/q`1)^2))by A38,XCMPLX_1:89
.=px`1/(sqrt(1+(q`2/q`1)^2)) by EUCLID:52;
A42: q`2=q`2*sqrt(1+(q`2/q`1)^2)/(sqrt(1+(q`2/q`1)^2))by A38,XCMPLX_1:89
.=px`2/(sqrt(1+(q`2/q`1)^2)) by EUCLID:52;
A43: |.q.|^2=q`1^2+q`2^2 by JGRAPH_3:1;
A44: |.q.|^2<1^2 by A29,SQUARE_1:16;
A45: now
assume that
A46: px`1=0 and
A47: px`2=0;
A48: q`1*sqrt(1+(q`2/q`1)^2)=0 by A46,EUCLID:52;
A49: q`2*sqrt(1+(q`2/q`1)^2)=0 by A47,EUCLID:52;
A50: q`1=0 by A38,A48,XCMPLX_1:6;
q`2=0 by A38,A49,XCMPLX_1:6;
hence contradiction by A35,A50,EUCLID:53,54;
end;
q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 &
q`2*sqrt(1+(q`2/q`1)^2) <= (-q`1)*sqrt(1+(q`2/q`1)^2)
by A35,A38,XREAL_1:64;
then
A51: q`2<=q`1 & (-q`1)*sqrt(1+(q`2/q`1)^2) <= q`2*sqrt(1+(q`2/q`1) ^2)
or px`2>=px`1 & px`2<=-px`1 by A36,A37,A38,XREAL_1:64;
then px`2<=px`1 & -px`1<=px`2 or px`2>=px`1 & px`2<=-px`1
by A36,A37,A38,XREAL_1:64;
then
A52: Sq_Circ
.px=|[px`1/sqrt(1+(px`2/px`1)^2),px`2/sqrt(1+(px`2/px`1 )^2) ]|
by A45,JGRAPH_2:3,JGRAPH_3:def 1;
px`2<=px`1 & --px`1>=-px`2 or px`2>=px`1 & px`2<=-px`1
by A36,A37,A38,A51,XREAL_1:24,64;
then
A53: px`2<=px`1 & px`1>=-px`2 or px`2>=px`1 & -px`2>=--px`1 by XREAL_1:24;
A54: px`1/sqrt(1+(px`2/px`1)^2)=q`1 by A36,A38,A40,XCMPLX_1:89;
A55: px`2/sqrt(1+(px`2/px`1)^2)=q`2 by A37,A38,A40,XCMPLX_1:89;
A56: dom Sq_Circ=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
not px`1=0 by A36,A37,A38,A45,A51,XREAL_1:64;
then
A57: (px`1)^2>0 by SQUARE_1:12;
A58: (px`2)^2>=0 by XREAL_1:63;
(px`1)^2/(sqrt(1+(px`2/px`1)^2))^2+(px`2/sqrt(1+(px`2/px`1)^2)) ^2 < 1
by A40,A41,A42,A43,A44,XCMPLX_1:76;
then (px`1)^2/(sqrt(1+(px`2/px`1)^2))^2+(px`2)^2/(sqrt(1+(px`2/px`1)^2))
^2<1 by XCMPLX_1:76;
then (px`1)^2/(1+(px`2/px`1)^2)+(px`2)^2/(sqrt(1+(px`2/px`1)^2))^2<1
by A39,SQUARE_1:def 2;
then (px`1)^2/(1+(px`2/px`1)^2)+(px`2)^2/(1+(px`2/px`1)^2)<1
by A39,SQUARE_1:def 2;
then ((px`1)^2/(1+(px`2/px`1)^2)
+(px`2)^2/(1+(px`2/px`1)^2))*(1+(px`2/px`1)^2)<1 *(1+(px`2/px`1)^2)
by A39,XREAL_1:68;
then (px`1)^2/(1+(px`2/px`1)^2)*(1+(px`2/px`1)^2)
+(px`2)^2/(1+(px`2/px`1)^2)*(1+(px`2/px`1)^2)<1 *(1+(px`2/px`1)^2);
then (px`1)^2+(px`2)^2/(1+(px`2/px`1)^2)*(1+(px`2/px`1)^2)<1 *(1+(px`2/
px `1)^2) by A39,XCMPLX_1:87;
then
A59: (px`1)^2+(px`2)^2<1 *(1+(px`2/px`1)^2) by A39,XCMPLX_1:87;
1 *(1+(px`2/px`1)^2) =1+(px`2)^2/(px`1)^2 by XCMPLX_1:76;
then (px`1)^2+(px`2)^2-1<1+(px`2)^2/(px`1)^2-1 by A59,XREAL_1:9;
then ((px`1)^2+(px`2)^2-1)*(px`1)^2<((px`2)^2/(px`1)^2)*(px`1)^2
by A57,XREAL_1:68;
then
A60: ((px`1)^2+((px`2)^2-1))*(px`1)^2<(px`2)^2 by A57,XCMPLX_1:87;
(px`1)^2*(px`1)^2+((px`1)^2*(px`2)^2-(px`1)^2*1)-(px`2)^2
= ((px`1)^2-1)*((px`1)^2+(px`2)^2);
then (px`1)^2-1<0 or ((px`1)^2+(px`2)^2)<0 by A60,XREAL_1:49;
then
A61: (px`1)^2-1+1<0+1 by A58,XREAL_1:6;
then
A62: px`1<1^2 by SQUARE_1:48;
A63: px`1>-1^2 by A61,SQUARE_1:48;
px`2<1 & 1>-px`2 or px`2>=px`1 & -px`2>=px`1 by A53,A62,XXREAL_0:2;
then px`2<1 & -1< --px`2 or px`2>-1 & -px`2> -1
by A63,XREAL_1:24,XXREAL_0:2;
then px`2<1 & -1 =1} holds Sq_Circ.:Kb=Cb
proof
let Kb,Cb be Subset of TOP-REAL 2;
assume
A1: Kb={p: not(-1 =1};
thus Sq_Circ.:Kb c= Cb
proof
let y be object;
assume y in Sq_Circ.:Kb;
then consider x being object such that
x in dom Sq_Circ and
A2: x in Kb and
A3: y=Sq_Circ.x by FUNCT_1:def 6;
consider q being Point of TOP-REAL 2 such that
A4: q=x and
A5: not(-1 0 by XREAL_1:34,63;
A14: now
assume
A15: q`1=0;
then q`2=0 by A6;
hence contradiction by A6,A15,EUCLID:53,54;
end;
then
A16: (q`1)^2>0 by SQUARE_1:12;
(q`1)^2>1^2 by A5,A8,SQUARE_1:47;
then
A17: sqrt((q`1)^2)>1 by SQUARE_1:18,27;
|.(|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|).|^2
=((q`1)/sqrt(1+(q`2/(q`1))^2))^2+(q`2/sqrt(1+(q`2/(q`1))^2))^2
by A11,A12,JGRAPH_3:1
.=(q`1)^2/(sqrt(1+(q`2/(q`1))^2))^2+(q`2/sqrt(1+(q`2/(q`1))^2))^2
by XCMPLX_1:76
.=(q`1)^2/(sqrt(1+(q`2/(q`1))^2))^2
+(q`2)^2/(sqrt(1+(q`2/(q`1))^2))^2 by XCMPLX_1:76
.=(q`1)^2/(1+(q`2/q`1)^2)+(q`2)^2/(sqrt(1+(q`2/q`1)^2))^2
by A13,SQUARE_1:def 2
.=(q`1)^2/(1+(q`2/q`1)^2)+(q`2)^2/(1+(q`2/q`1)^2)
by A13,SQUARE_1:def 2
.=((q`1)^2+(q`2)^2)/(1+(q`2/q`1)^2) by XCMPLX_1:62
.=((q`1)^2+(q`2)^2)/(1+(q`2)^2/(q`1)^2) by XCMPLX_1:76
.=((q`1)^2+(q`2)^2)/((q`1)^2/(q`1)^2+(q`2)^2/(q`1)^2)
by A16,XCMPLX_1:60
.=((q`1)^2+(q`2)^2)/(((q`1)^2+(q`2)^2)/(q`1)^2) by XCMPLX_1:62
.=(q`1)^2*(((q`1)^2+(q`2)^2)/((q`1)^2+(q`2)^2)) by XCMPLX_1:81
.=(q`1)^2*1 by A14,COMPLEX1:1,XCMPLX_1:60
.=(q`1)^2;
then |.(|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|).|>1
by A17,SQUARE_1:22;
hence ex p2 being Point of TOP-REAL 2 st p2=y & |.p2.|>1 by A3,A4,A7;
end;
case
A18: q<>0.TOP-REAL 2 & not(q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
then
A19: Sq_Circ.q=|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2 )]|
by JGRAPH_3:def 1;
A20: (|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|)`1 = q`1/sqrt(1+(q
`1/q`2)^2) by EUCLID:52;
A21: (|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|)`2 = q`2/sqrt(1+(q
`1/q`2)^2) by EUCLID:52;
A22: 1+(q`1/q`2)^2>0 by XREAL_1:34,63;
A23: q`2 <> 0 by A18;
then
A24: (q`2)^2>0 by SQUARE_1:12;
not(-1 <=q`1 & q`1<= 1) implies -1>q`2 or q`2>1
proof
assume
A25: not(-1 <=q`1 & q`1<= 1);
now per cases by A25;
case
A26: -1>q`1;
then q`2< -1 or q`1

q`2 by A26,XXREAL_0:2;
hence thesis by XREAL_1:24;
end;
case
A27: q`1>1;
--q`1< -q`2 & q`2

q`1 & q`2> -q`1 by A18,XREAL_1:24;
then 1< -q`2 or q`2>q`1 & q`2> -q`1 by A27,XXREAL_0:2;
then -1> --q`2 or 1

1^2 by A5,SQUARE_1:47;
then
A28: sqrt((q`2)^2)>1 by SQUARE_1:18,27;
|.(|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|).|^2
=((q`1)/sqrt(1+(q`1/(q`2))^2))^2+(q`2/sqrt(1+(q`1/(q`2))^2))^2
by A20,A21,JGRAPH_3:1
.=(q`1)^2/(sqrt(1+(q`1/(q`2))^2))^2+(q`2/sqrt(1+(q`1/(q`2))^2))^2
by XCMPLX_1:76
.=(q`1)^2/(sqrt(1+(q`1/(q`2))^2))^2
+(q`2)^2/(sqrt(1+(q`1/(q`2))^2))^2 by XCMPLX_1:76
.=(q`1)^2/(1+(q`1/q`2)^2)+(q`2)^2/(sqrt(1+(q`1/q`2)^2))^2
by A22,SQUARE_1:def 2
.=(q`1)^2/(1+(q`1/q`2)^2)+(q`2)^2/(1+(q`1/q`2)^2)
by A22,SQUARE_1:def 2
.=((q`1)^2+(q`2)^2)/(1+(q`1/q`2)^2) by XCMPLX_1:62
.=((q`1)^2+(q`2)^2)/(1+(q`1)^2/(q`2)^2) by XCMPLX_1:76
.=((q`1)^2+(q`2)^2)/((q`1)^2/(q`2)^2+(q`2)^2/(q`2)^2)
by A24,XCMPLX_1:60
.=((q`1)^2+(q`2)^2)/(((q`1)^2+(q`2)^2)/(q`2)^2)
by XCMPLX_1:62
.=(q`2)^2*(((q`1)^2+(q`2)^2)/((q`1)^2+(q`2)^2))
by XCMPLX_1:81
.=(q`2)^2*1 by A23,COMPLEX1:1,XCMPLX_1:60
.=(q`2)^2;
then |.(|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|).|>1
by A28,SQUARE_1:22;
hence ex p2 being Point of TOP-REAL 2 st p2=y & |.p2.|>1 by A3,A4,A19;
end;
end;
hence thesis by A1;
end;
let y be object;
assume y in Cb;
then consider p2 being Point of TOP-REAL 2 such that
A29: p2=y and
A30: |.p2.|>1 by A1;
set q=p2;
now per cases;
case q=0.TOP-REAL 2;
hence contradiction by A30,TOPRNS_1:23;
end;
case
A31: q<>0.TOP-REAL 2 & (q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
set px=|[q`1*sqrt(1+(q`2/q`1)^2),q`2*sqrt(1+(q`2/q`1)^2)]|;
A32: px`1 = q`1*sqrt(1+(q`2/q`1)^2) by EUCLID:52;
A33: px`2 = q`2*sqrt(1+(q`2/q`1)^2) by EUCLID:52;
1+(q`2/q`1)^2>0 by XREAL_1:34,63;
then
A34: sqrt(1+(q`2/q`1)^2)>0 by SQUARE_1:25;
A35: 1+(px`2/px`1)^2>0 by XREAL_1:34,63;
A36: px`2/px`1=q`2/q`1 by A32,A33,A34,XCMPLX_1:91;
A37: q`1=q`1*sqrt(1+(q`2/q`1)^2)/(sqrt(1+(q`2/q`1)^2))by A34,XCMPLX_1:89
.=px`1/(sqrt(1+(q`2/q`1)^2)) by EUCLID:52;
A38: q`2=q`2*sqrt(1+(q`2/q`1)^2)/(sqrt(1+(q`2/q`1)^2))by A34,XCMPLX_1:89
.=px`2/(sqrt(1+(q`2/q`1)^2)) by EUCLID:52;
A39: |.q.|^2=q`1^2+q`2^2 by JGRAPH_3:1;
A40: |.q.|^2>1^2 by A30,SQUARE_1:16;
A41: now
assume that
A42: px`1=0 and
A43: px`2=0;
A44: q`1*sqrt(1+(q`2/q`1)^2)=0 by A42,EUCLID:52;
A45: q`2*sqrt(1+(q`2/q`1)^2)=0 by A43,EUCLID:52;
A46: q`1=0 by A34,A44,XCMPLX_1:6;
q`2=0 by A34,A45,XCMPLX_1:6;
hence contradiction by A31,A46,EUCLID:53,54;
end;
q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 &
q`2*sqrt(1+(q`2/q`1)^2) <= (-q`1)*sqrt(1+(q`2/q`1)^2)
by A31,A34,XREAL_1:64;
then
A47: q`2<=q`1 & (-q`1)*sqrt(1+(q`2/q`1)^2) <= q`2*sqrt(1+(q`2/q`1) ^2)
or px`2>=px`1 & px`2<=-px`1 by A32,A33,A34,XREAL_1:64;
then px`2<=px`1 & -px`1<=px`2 or px`2>=px`1 & px`2<=-px`1
by A32,A33,A34,XREAL_1:64;
then
A48: Sq_Circ
.px=|[px`1/sqrt(1+(px`2/px`1)^2),px`2/sqrt(1+(px`2/px`1 )^2) ]|
by A41,JGRAPH_2:3,JGRAPH_3:def 1;
A49: px`1/sqrt(1+(px`2/px`1)^2)=q`1 by A32,A34,A36,XCMPLX_1:89;
A50: px`2/sqrt(1+(px`2/px`1)^2)=q`2 by A33,A34,A36,XCMPLX_1:89;
A51: dom Sq_Circ=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
not px`1=0 by A32,A33,A34,A41,A47,XREAL_1:64;
then
A52: (px`1)^2>0 by SQUARE_1:12;
A53: (px`2)^2>=0 by XREAL_1:63;
(px`1)^2/(sqrt(1+(px`2/px`1)^2))^2+(px`2/sqrt(1+(px`2/px`1)^2)) ^2 > 1
by A36,A37,A38,A39,A40,XCMPLX_1:76;
then (px`1)^2/(sqrt(1+(px`2/px`1)^2))^2+(px`2)^2/(sqrt(1+(px`2/px`1)^2))
^2>1 by XCMPLX_1:76;
then (px`1)^2/(1+(px`2/px`1)^2)+(px`2)^2/(sqrt(1+(px`2/px`1)^2))^2>1
by A35,SQUARE_1:def 2;
then (px`1)^2/(1+(px`2/px`1)^2)+(px`2)^2/(1+(px`2/px`1)^2)>1
by A35,SQUARE_1:def 2;
then ((px`1)^2/(1+(px`2/px`1)^2)
+(px`2)^2/(1+(px`2/px`1)^2))*(1+(px`2/px`1)^2)>1 *(1+(px`2/px`1)^2)
by A35,XREAL_1:68;
then (px`1)^2/(1+(px`2/px`1)^2)*(1+(px`2/px`1)^2)
+(px`2)^2/(1+(px`2/px`1)^2)*(1+(px`2/px`1)^2)>1 *(1+(px`2/px`1)^2);
then (px`1)^2+(px`2)^2/(1+(px`2/px`1)^2)*(1+(px`2/px`1)^2)>1 *(1+(px`2/
px `1)^2) by A35,XCMPLX_1:87;
then
A54: (px`1)^2+(px`2)^2>1 *(1+(px`2/px`1)^2) by A35,XCMPLX_1:87;
1 *(1+(px`2/px`1)^2) =1+(px`2)^2/(px`1)^2 by XCMPLX_1:76;
then (px`1)^2+(px`2)^2-1>1+(px`2)^2/(px`1)^2-1 by A54,XREAL_1:9;
then ((px`1)^2+(px`2)^2-1)*(px`1)^2>((px`2)^2/(px`1)^2)*(px`1)^2
by A52,XREAL_1:68;
then
A55: ((px`1)^2+((px`2)^2-1))*(px`1)^2>(px`2)^2 by A52,XCMPLX_1:87;
(px`1)^2*(px`1)^2+((px`1)^2*(px`2)^2-(px`1)^2*1)-(px`2)^2
= ((px`1)^2-1)*((px`1)^2+(px`2)^2);
then (px`1)^2-1>0 or (px`1)^2+(px`2)^2<0 by A55,XREAL_1:50;
then (px`1)^2-1+1>0+1 by A52,A53,XREAL_1:6;
then px`1>1^2 or px`1< -1 by SQUARE_1:49;
then px in Kb by A1;
hence ex x being set st x in dom Sq_Circ & x in Kb & y=Sq_Circ.x
by A29,A48,A49,A50,A51,EUCLID:53;
end;
case
A56: q<>0.TOP-REAL 2 & not(q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
set px=|[q`1*sqrt(1+(q`1/q`2)^2),q`2*sqrt(1+(q`1/q`2)^2)]|;
A57: q`1<=q`2 & -q`2<=q`1 or q`1>=q`2 & q`1<=-q`2 by A56,JGRAPH_2:13;
A58: px`2 = q`2*sqrt(1+(q`1/q`2)^2) by EUCLID:52;
A59: px`1 = q`1*sqrt(1+(q`1/q`2)^2) by EUCLID:52;
1+(q`1/q`2)^2>0 by XREAL_1:34,63;
then
A60: sqrt(1+(q`1/q`2)^2)>0 by SQUARE_1:25;
A61: 1+(px`1/px`2)^2>0 by XREAL_1:34,63;
A62: px`1/px`2=q`1/q`2 by A58,A59,A60,XCMPLX_1:91;
A63: q`2=q`2*sqrt(1+(q`1/q`2)^2)/(sqrt(1+(q`1/q`2)^2))by A60,XCMPLX_1:89
.=px`2/(sqrt(1+(q`1/q`2)^2)) by EUCLID:52;
A64: q`1=q`1*sqrt(1+(q`1/q`2)^2)/(sqrt(1+(q`1/q`2)^2))by A60,XCMPLX_1:89
.=px`1/(sqrt(1+(q`1/q`2)^2)) by EUCLID:52;
A65: |.q.|^2=q`2^2+q`1^2 by JGRAPH_3:1;
A66: |.q.|^2>1^2 by A30,SQUARE_1:16;
A67: now
assume that
A68: px`2=0 and
A69: px`1=0;
A70: q`2*sqrt(1+(q`1/q`2)^2)=0 by A68,EUCLID:52;
q`1*sqrt(1+(q`1/q`2)^2)=0 by A69,EUCLID:52;
then q`1=0 by A60,XCMPLX_1:6;
hence contradiction by A56,A60,A70,XCMPLX_1:6;
end;
q`1<=q`2 & -q`2<=q`1 or q`1>=q`2 &
q`1*sqrt(1+(q`1/q`2)^2) <= (-q`2)*sqrt(1+(q`1/q`2)^2)
by A57,A60,XREAL_1:64;
then
A71: q`1<=q`2 & (-q`2)*sqrt(1+(q`1/q`2)^2) <= q`1*sqrt(1+(q`1/q`2) ^2)
or px`1>=px`2 & px`1<=-px`2 by A58,A59,A60,XREAL_1:64;
then px`1<=px`2 & -px`2<=px`1 or px`1>=px`2 & px`1<=-px`2
by A58,A59,A60,XREAL_1:64;
then
A72: Sq_Circ
.px=|[px`1/sqrt(1+(px`1/px`2)^2),px`2/sqrt(1+(px`1/px`2 )^2) ]|
by A67,JGRAPH_2:3,JGRAPH_3:4;
A73: px`2/sqrt(1+(px`1/px`2)^2)=q`2 by A58,A60,A62,XCMPLX_1:89;
A74: px`1/sqrt(1+(px`1/px`2)^2)=q`1 by A59,A60,A62,XCMPLX_1:89;
A75: dom Sq_Circ=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
not px`2=0 by A58,A59,A60,A67,A71,XREAL_1:64;
then
A76: (px`2)^2>0 by SQUARE_1:12;
A77: (px`1)^2>=0 by XREAL_1:63;
(px`2)^2/(sqrt(1+(px`1/px`2)^2))^2+(px`1/sqrt(1+(px`1/px`2)^2)) ^2 > 1
by A62,A63,A64,A65,A66,XCMPLX_1:76;
then (px`2)^2/(sqrt(1+(px`1/px`2)^2))^2+(px`1)^2/(sqrt(1+(px`1/px`2)^2))
^2>1 by XCMPLX_1:76;
then (px`2)^2/(1+(px`1/px`2)^2)+(px`1)^2/(sqrt(1+(px`1/px`2)^2))^2>1
by A61,SQUARE_1:def 2;
then (px`2)^2/(1+(px`1/px`2)^2)+(px`1)^2/(1+(px`1/px`2)^2)>1
by A61,SQUARE_1:def 2;
then ((px`2)^2/(1+(px`1/px`2)^2)
+(px`1)^2/(1+(px`1/px`2)^2))*(1+(px`1/px`2)^2)>1 *(1+(px`1/px`2)^2)
by A61,XREAL_1:68;
then (px`2)^2/(1+(px`1/px`2)^2)*(1+(px`1/px`2)^2)
+(px`1)^2/(1+(px`1/px`2)^2)*(1+(px`1/px`2)^2)>1 *(1+(px`1/px`2)^2);
then (px`2)^2+(px`1)^2/(1+(px`1/px`2)^2)*(1+(px`1/px`2)^2)>1 *(1+(px`1/
px `2)^2) by A61,XCMPLX_1:87;
then
A78: (px`2)^2+(px`1)^2>1 *(1+(px`1/px`2)^2) by A61,XCMPLX_1:87;
1 *(1+(px`1/px`2)^2) =1+(px`1)^2/(px`2)^2 by XCMPLX_1:76;
then (px`2)^2+(px`1)^2-1>1+(px`1)^2/(px`2)^2-1 by A78,XREAL_1:9;
then ((px`2)^2+(px`1)^2-1)*(px`2)^2>((px`1)^2/(px`2)^2)*(px`2)^2
by A76,XREAL_1:68;
then
A79: ((px`2)^2+((px`1)^2-1))*(px`2)^2>(px`1)^2 by A76,XCMPLX_1:87;
(px`2)^2*(px`2)^2+((px`2)^2*(px`1)^2-(px`2)^2*1)-(px`1)^2
= ((px`2)^2-1)*((px`2)^2+(px`1)^2);
then (px`2)^2-1>0 or (px`1)^2+(px`2)^2<0 by A79,XREAL_1:50;
then (px`2)^2-1+1>0+1 by A76,A77,XREAL_1:6;
then px`2>1^2 or px`2< -1 by SQUARE_1:49;
then px in Kb by A1;
hence ex x being set st x in dom Sq_Circ & x in Kb & y=Sq_Circ.x
by A29,A72,A73,A74,A75,EUCLID:53;
end;
end;
hence thesis by FUNCT_1:def 6;
end;
theorem Th27:
for Kb,Cb being Subset of TOP-REAL 2 st
Kb={p: -1 <=p`1 & p`1<= 1 & -1 <=p`2 & p`2<= 1}&
Cb={p2 where p2 is Point of TOP-REAL 2: |.p2.|<=1} holds Sq_Circ.:Kb=Cb
proof
let Kb,Cb be Subset of TOP-REAL 2;
assume
A1: Kb={p: -1 <=p`1 & p`1<= 1 & -1 <=p`2 & p`2<= 1}&
Cb={p2 where p2 is Point of TOP-REAL 2: |.p2.|<=1};
thus Sq_Circ.:Kb c= Cb
proof
let y be object;
assume y in Sq_Circ.:Kb;
then consider x being object such that
x in dom Sq_Circ and
A2: x in Kb and
A3: y=Sq_Circ.x by FUNCT_1:def 6;
consider q being Point of TOP-REAL 2 such that
A4: q=x and
A5: -1 <=q`1 and
A6: q`1<= 1 and
A7: -1 <=q`2 and
A8: q`2<= 1 by A1,A2;
now per cases;
case
A9: q=0.TOP-REAL 2;
then
A10: Sq_Circ.q=q by JGRAPH_3:def 1;
|.q.|=0 by A9,TOPRNS_1:23;
hence ex p2 being Point of TOP-REAL 2 st p2=y & |.p2.|<=1 by A3,A4,A10;
end;
case
A11: q<>0.TOP-REAL 2 & (q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
then
A12: Sq_Circ.q=|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2 )]|
by JGRAPH_3:def 1;
A13: (|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|)`1 = q`1/sqrt(1+(q
`2/q`1)^2) by EUCLID:52;
A14: (|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|)`2 = q`2/sqrt(1+(q
`2/q`1)^2) by EUCLID:52;
A15: 1+(q`2/q`1)^2>0 by XREAL_1:34,63;
A16: now
assume
A17: q`1=0;
then q`2=0 by A11;
hence contradiction by A11,A17,EUCLID:53,54;
end;
then
A18: (q`1)^2>0 by SQUARE_1:12;
(q`1)^2<=1^2 by A5,A6,SQUARE_1:49;
then
A19: sqrt((q`1)^2)<=1 by A18,SQUARE_1:18,26;
|.(|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|).|^2
=((q`1)/sqrt(1+(q`2/(q`1))^2))^2+(q`2/sqrt(1+(q`2/(q`1))^2))^2
by A13,A14,JGRAPH_3:1
.=(q`1)^2/(sqrt(1+(q`2/(q`1))^2))^2+(q`2/sqrt(1+(q`2/(q`1))^2))^2
by XCMPLX_1:76
.=(q`1)^2/(sqrt(1+(q`2/(q`1))^2))^2
+(q`2)^2/(sqrt(1+(q`2/(q`1))^2))^2 by XCMPLX_1:76
.=(q`1)^2/(1+(q`2/q`1)^2)+(q`2)^2/(sqrt(1+(q`2/q`1)^2))^2
by A15,SQUARE_1:def 2
.=(q`1)^2/(1+(q`2/q`1)^2)+(q`2)^2/(1+(q`2/q`1)^2)
by A15,SQUARE_1:def 2
.=((q`1)^2+(q`2)^2)/(1+(q`2/q`1)^2) by XCMPLX_1:62
.=((q`1)^2+(q`2)^2)/(1+(q`2)^2/(q`1)^2) by XCMPLX_1:76
.=((q`1)^2+(q`2)^2)/((q`1)^2/(q`1)^2+(q`2)^2/(q`1)^2)
by A18,XCMPLX_1:60
.=((q`1)^2+(q`2)^2)/(((q`1)^2+(q`2)^2)/(q`1)^2)
by XCMPLX_1:62
.=(q`1)^2*(((q`1)^2+(q`2)^2)/((q`1)^2+(q`2)^2))
by XCMPLX_1:81
.=(q`1)^2*1 by A16,COMPLEX1:1,XCMPLX_1:60
.=(q`1)^2;
then |.(|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|).|<=1
by A19,SQUARE_1:22;
hence ex p2 being Point of TOP-REAL 2 st p2=y & |.p2.|<=1 by A3,A4,A12;
end;
case
A20: q<>0.TOP-REAL 2 & not(q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
then
A21: Sq_Circ.q=|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2 )]|
by JGRAPH_3:def 1;
A22: (|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|)`1 = q`1/sqrt(1+(q
`1/q`2)^2) by EUCLID:52;
A23: (|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|)`2 = q`2/sqrt(1+(q
`1/q`2)^2) by EUCLID:52;
A24: 1+(q`1/q`2)^2>0 by XREAL_1:34,63;
A25: q`2 <>0 by A20;
then
A26: (q`2)^2>0 by SQUARE_1:12;
(q`2)^2<=1^2 by A7,A8,SQUARE_1:49;
then
A27: sqrt((q`2)^2)<=1 by A26,SQUARE_1:18,26;
|.(|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|).|^2
=((q`1)/sqrt(1+(q`1/(q`2))^2))^2+(q`2/sqrt(1+(q`1/(q`2))^2))^2
by A22,A23,JGRAPH_3:1
.=(q`1)^2/(sqrt(1+(q`1/(q`2))^2))^2+(q`2/sqrt(1+(q`1/(q`2))^2))^2
by XCMPLX_1:76
.=(q`1)^2/(sqrt(1+(q`1/(q`2))^2))^2
+(q`2)^2/(sqrt(1+(q`1/(q`2))^2))^2 by XCMPLX_1:76
.=(q`1)^2/(1+(q`1/q`2)^2)+(q`2)^2/(sqrt(1+(q`1/q`2)^2))^2
by A24,SQUARE_1:def 2
.=(q`1)^2/(1+(q`1/q`2)^2)+(q`2)^2/(1+(q`1/q`2)^2)
by A24,SQUARE_1:def 2
.=((q`1)^2+(q`2)^2)/(1+(q`1/q`2)^2) by XCMPLX_1:62
.=((q`1)^2+(q`2)^2)/(1+(q`1)^2/(q`2)^2) by XCMPLX_1:76
.=((q`1)^2+(q`2)^2)/((q`1)^2/(q`2)^2+(q`2)^2/(q`2)^2)
by A26,XCMPLX_1:60
.=((q`1)^2+(q`2)^2)/(((q`1)^2+(q`2)^2)/(q`2)^2)
by XCMPLX_1:62
.=(q`2)^2*(((q`1)^2+(q`2)^2)/((q`1)^2+(q`2)^2)) by XCMPLX_1:81
.=(q`2)^2*1 by A25,COMPLEX1:1,XCMPLX_1:60
.=(q`2)^2;
then |.(|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|).|<=1
by A27,SQUARE_1:22;
hence ex p2 being Point of TOP-REAL 2 st p2=y & |.p2.|<=1 by A3,A4,A21;
end;
end;
hence thesis by A1;
end;
let y be object;
assume y in Cb;
then consider p2 being Point of TOP-REAL 2 such that
A28: p2=y and
A29: |.p2.|<=1 by A1;
set q=p2;
now per cases;
case
A30: q=0.TOP-REAL 2;
then
A31: q`1=0 by EUCLID:52,54;
q`2=0 by A30,EUCLID:52,54;
then
A32: y in Kb by A1,A28,A31;
A33: Sq_Circ".y=y by A28,A30,JGRAPH_3:28;
A34: dom Sq_Circ=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
y=Sq_Circ.y by A28,A33,FUNCT_1:35,JGRAPH_3:43;
hence ex x being set st x in dom Sq_Circ & x in Kb & y=Sq_Circ.x
by A32,A34;
end;
case
A35: q<>0.TOP-REAL 2 & (q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
set px=|[q`1*sqrt(1+(q`2/q`1)^2),q`2*sqrt(1+(q`2/q`1)^2)]|;
A36: px`1 = q`1*sqrt(1+(q`2/q`1)^2) by EUCLID:52;
A37: px`2 = q`2*sqrt(1+(q`2/q`1)^2) by EUCLID:52;
1+(q`2/q`1)^2>0 by XREAL_1:34,63;
then
A38: sqrt(1+(q`2/q`1)^2)>0 by SQUARE_1:25;
A39: 1+(px`2/px`1)^2>0 by XREAL_1:34,63;
A40: px`2/px`1=q`2/q`1 by A36,A37,A38,XCMPLX_1:91;
A41: q`1=q`1*sqrt(1+(q`2/q`1)^2)/(sqrt(1+(q`2/q`1)^2))by A38,XCMPLX_1:89
.=px`1/(sqrt(1+(q`2/q`1)^2)) by EUCLID:52;
A42: q`2=q`2*sqrt(1+(q`2/q`1)^2)/(sqrt(1+(q`2/q`1)^2))by A38,XCMPLX_1:89
.=px`2/(sqrt(1+(q`2/q`1)^2)) by EUCLID:52;
A43: |.q.|^2=q`1^2+q`2^2 by JGRAPH_3:1;
A44: |.q.|^2<=1^2 by A29,SQUARE_1:15;
A45: now
assume that
A46: px`1=0 and
A47: px`2=0;
A48: q`1*sqrt(1+(q`2/q`1)^2)=0 by A46,EUCLID:52;
A49: q`2*sqrt(1+(q`2/q`1)^2)=0 by A47,EUCLID:52;
A50: q`1=0 by A38,A48,XCMPLX_1:6;
q`2=0 by A38,A49,XCMPLX_1:6;
hence contradiction by A35,A50,EUCLID:53,54;
end;
q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 &
q`2*sqrt(1+(q`2/q`1)^2) <= (-q`1)*sqrt(1+(q`2/q`1)^2)
by A35,A38,XREAL_1:64;
then
A51: q`2<=q`1 & (-q`1)*sqrt(1+(q`2/q`1)^2) <= q`2*sqrt(1+(q`2/q`1) ^2)
or px`2>=px`1 & px`2<=-px`1 by A36,A37,A38,XREAL_1:64;
then px`2<=px`1 & -px`1<=px`2 or px`2>=px`1 & px`2<=-px`1
by A36,A37,A38,XREAL_1:64;
then
A52: Sq_Circ
.px=|[px`1/sqrt(1+(px`2/px`1)^2),px`2/sqrt(1+(px`2/px`1 )^2) ]|
by A45,JGRAPH_2:3,JGRAPH_3:def 1;
px`2<=px`1 & --px`1>=-px`2 or px`2>=px`1 & px`2<=-px`1
by A36,A37,A38,A51,XREAL_1:24,64;
then
A53: px`2<=px`1 & px`1>=-px`2 or px`2>=px`1 & -px`2>=--px`1 by XREAL_1:24;
A54: px`1/sqrt(1+(px`2/px`1)^2)=q`1 by A36,A38,A40,XCMPLX_1:89;
A55: px`2/sqrt(1+(px`2/px`1)^2)=q`2 by A37,A38,A40,XCMPLX_1:89;
A56: dom Sq_Circ=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
not px`1=0 by A36,A37,A38,A45,A51,XREAL_1:64;
then
A57: (px`1)^2>0 by SQUARE_1:12;
A58: (px`2)^2>=0 by XREAL_1:63;
(px`1)^2/(sqrt(1+(px`2/px`1)^2))^2+(px`2/sqrt(1+(px`2/px`1)^2)) ^2 <=1
by A40,A41,A42,A43,A44,XCMPLX_1:76;
then (px`1)^2/(sqrt(1+(px`2/px`1)^2))^2+(px`2)^2/(sqrt(1+(px`2/px`1)^2))
^2<=1 by XCMPLX_1:76;
then (px`1)^2/(1+(px`2/px`1)^2)+(px`2)^2/(sqrt(1+(px`2/px`1)^2))^2<=1
by A39,SQUARE_1:def 2;
then (px`1)^2/(1+(px`2/px`1)^2)+(px`2)^2/(1+(px`2/px`1)^2)<=1
by A39,SQUARE_1:def 2;
then ((px`1)^2/(1+(px`2/px`1)^2)
+(px`2)^2/(1+(px`2/px`1)^2))*(1+(px`2/px`1)^2)<=1 *(1+(px`2/px`1)^2)
by A39,XREAL_1:64;
then (px`1)^2/(1+(px`2/px`1)^2)*(1+(px`2/px`1)^2)
+(px`2)^2/(1+(px`2/px`1)^2)*(1+(px`2/px`1)^2)<=1 *(1+(px`2/px`1)^2);
then (px`1)^2+(px`2)^2/(1+(px`2/px`1)^2)*(1+(px`2/px`1)^2)
<=1 *(1+(px`2/px`1)^2) by A39,XCMPLX_1:87;
then
A59: (px`1)^2+(px`2)^2<=1 *(1+(px`2/px`1)^2) by A39,XCMPLX_1:87;
1 *(1+(px`2/px`1)^2) =1+(px`2)^2/(px`1)^2 by XCMPLX_1:76;
then (px`1)^2+(px`2)^2-1<=1+(px`2)^2/(px`1)^2-1 by A59,XREAL_1:9;
then ((px`1)^2+(px`2)^2-1)*(px`1)^2<=((px`2)^2/(px`1)^2)*(px`1)^2
by A57,XREAL_1:64;
then ((px`1)^2+((px`2)^2-1))*(px`1)^2<=(px`2)^2 by A57,XCMPLX_1:87;
then
A60: (px`1)^2*(px`1)^2+(px`1)^2*((px`2)^2-1)-(px`2)^2<=0 by XREAL_1:47;
(px`1)^2*(px`1)^2+((px`1)^2*(px`2)^2-(px`1)^2*1)-(px`2)^2
= ((px`1)^2-1)*((px`1)^2+(px`2)^2);
then (px`1)^2-1<=0 & (px`1)^2-1>=0 or
(px`1)^2-1<=0 & (px`1)^2+(px`2)^2>=0 or
(px`1)^2+(px`2)^2<=0 & (px`1)^2-1>=0 or
(px`1)^2+(px`2)^2<=0 & (px`1)^2+(px`2)^2>=0 by A60,XREAL_1:129,130;
then
A61: (px`1)^2-1+1<=0+1 by A58,XREAL_1:7;
then
A62: px`1<=1^2 by SQUARE_1:47;
A63: px`1>= -1^2 by A61,SQUARE_1:47;
then px`2<=1 & 1>= -px`2 or px`2>= -1 & -px`2>=px`1 by A53,A62,XXREAL_0:2
;
then px`2<=1 & -1<= --px`2 or px`2>= -1 & -px`2>= -1
by A63,XREAL_1:24,XXREAL_0:2;
then px`2<=1 & -1<=px`2 or px`2>= -1 & --px`2<= --1 by XREAL_1:24;
then px in Kb by A1,A62,A63;
hence ex x being set st x in dom Sq_Circ & x in Kb & y=Sq_Circ.x
by A28,A52,A54,A55,A56,EUCLID:53;
end;
case
A64: q<>0.TOP-REAL 2 & not(q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
set px=|[q`1*sqrt(1+(q`1/q`2)^2),q`2*sqrt(1+(q`1/q`2)^2)]|;
A65: q`1<=q`2 & -q`2<=q`1 or q`1>=q`2 & q`1<=-q`2 by A64,JGRAPH_2:13;
A66: px`2 = q`2*sqrt(1+(q`1/q`2)^2) by EUCLID:52;
A67: px`1 = q`1*sqrt(1+(q`1/q`2)^2) by EUCLID:52;
1+(q`1/q`2)^2>0 by XREAL_1:34,63;
then
A68: sqrt(1+(q`1/q`2)^2)>0 by SQUARE_1:25;
A69: 1+(px`1/px`2)^2>0 by XREAL_1:34,63;
A70: px`1/px`2=q`1/q`2 by A66,A67,A68,XCMPLX_1:91;
A71: q`2=q`2*sqrt(1+(q`1/q`2)^2)/(sqrt(1+(q`1/q`2)^2))by A68,XCMPLX_1:89
.=px`2/(sqrt(1+(q`1/q`2)^2)) by EUCLID:52;
A72: q`1=q`1*sqrt(1+(q`1/q`2)^2)/(sqrt(1+(q`1/q`2)^2))by A68,XCMPLX_1:89
.=px`1/(sqrt(1+(q`1/q`2)^2)) by EUCLID:52;
A73: |.q.|^2=q`2^2+q`1^2 by JGRAPH_3:1;
A74: |.q.|^2<=1^2 by A29,SQUARE_1:15;
A75: now
assume that
A76: px`2=0 and
A77: px`1=0;
A78: q`2*sqrt(1+(q`1/q`2)^2)=0 by A76,EUCLID:52;
q`1*sqrt(1+(q`1/q`2)^2)=0 by A77,EUCLID:52;
then q`1=0 by A68,XCMPLX_1:6;
hence contradiction by A64,A68,A78,XCMPLX_1:6;
end;
q`1<=q`2 & -q`2<=q`1 or q`1>=q`2 &
q`1*sqrt(1+(q`1/q`2)^2) <= (-q`2)*sqrt(1+(q`1/q`2)^2)
by A65,A68,XREAL_1:64;
then
A79: q`1<=q`2 & (-q`2)*sqrt(1+(q`1/q`2)^2) <= q`1*sqrt(1+(q`1/q`2) ^2)
or px`1>=px`2 & px`1<=-px`2 by A66,A67,A68,XREAL_1:64;
then px`1<=px`2 & -px`2<=px`1 or px`1>=px`2 & px`1<=-px`2
by A66,A67,A68,XREAL_1:64;
then
A80: Sq_Circ
.px=|[px`1/sqrt(1+(px`1/px`2)^2),px`2/sqrt(1+(px`1/px`2 )^2) ]|
by A75,JGRAPH_2:3,JGRAPH_3:4;
px`1<=px`2 & --px`2>=-px`1 or px`1>=px`2 & px`1<=-px`2
by A66,A67,A68,A79,XREAL_1:24,64;
then
A81: px`1<=px`2 & px`2>=-px`1 or px`1>=px`2 & -px`1>=--px`2 by XREAL_1:24;
A82: px`2/sqrt(1+(px`1/px`2)^2)=q`2 by A66,A68,A70,XCMPLX_1:89;
A83: px`1/sqrt(1+(px`1/px`2)^2)=q`1 by A67,A68,A70,XCMPLX_1:89;
A84: dom Sq_Circ=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
not px`2=0 by A66,A67,A68,A75,A79,XREAL_1:64;
then
A85: (px`2)^2>0 by SQUARE_1:12;
A86: (px`1)^2>=0 by XREAL_1:63;
(px`2)^2/(sqrt(1+(px`1/px`2)^2))^2+(px`1/sqrt(1+(px`1/px`2)^2)) ^2 <= 1
by A70,A71,A72,A73,A74,XCMPLX_1:76;
then
(px`2)^2/(sqrt(1+(px`1/px`2)^2))^2+(px`1)^2/(sqrt(1+(px`1/px`2)^2))
^2<=1 by XCMPLX_1:76;
then (px`2)^2/(1+(px`1/px`2)^2)+(px`1)^2/(sqrt(1+(px`1/px`2)^2))^2<=1
by A69,SQUARE_1:def 2;
then (px`2)^2/(1+(px`1/px`2)^2)+(px`1)^2/(1+(px`1/px`2)^2)<=1
by A69,SQUARE_1:def 2;
then ((px`2)^2/(1+(px`1/px`2)^2)
+(px`1)^2/(1+(px`1/px`2)^2))*(1+(px`1/px`2)^2)<=1 *(1+(px`1/px`2)^2)
by A69,XREAL_1:64;
then (px`2)^2/(1+(px`1/px`2)^2)*(1+(px`1/px`2)^2)
+(px`1)^2/(1+(px`1/px`2)^2)*(1+(px`1/px`2)^2)<=1 *(1+(px`1/px`2)^2);
then (px`2)^2+(px`1)^2/(1+(px`1/px`2)^2)*(1+(px`1/px`2)^2)
<=1 *(1+(px`1/px`2)^2) by A69,XCMPLX_1:87;
then
A87: (px`2)^2+(px`1)^2<=1 *(1+(px`1/px`2)^2) by A69,XCMPLX_1:87;
1 *(1+(px`1/px`2)^2) =1+(px`1)^2/(px`2)^2 by XCMPLX_1:76;
then (px`2)^2+(px`1)^2-1<=1+(px`1)^2/(px`2)^2-1 by A87,XREAL_1:9;
then ((px`2)^2+(px`1)^2-1)*(px`2)^2<=((px`1)^2/(px`2)^2)*(px`2)^2
by A85,XREAL_1:64;
then ((px`2)^2+((px`1)^2-1))*(px`2)^2<=(px`1)^2 by A85,XCMPLX_1:87;
then
A88: (px`2)^2*(px`2)^2+(px`2)^2*((px`1)^2-1)-(px`1)^2<=0 by XREAL_1:47;
(px`2)^2*(px`2)^2+((px`2)^2*(px`1)^2-(px`2)^2*1)-(px`1)^2
= ((px`2)^2-1)*((px`2)^2+(px`1)^2);
then (px`2)^2-1<=0 or ((px`2)^2+(px`1)^2)<=0 by A88,XREAL_1:129;
then
A89: (px`2)^2-1+1<=0+1 by A86,XREAL_1:7;
then
A90: px`2<=1^2 by SQUARE_1:47;
A91: px`2>= -1^2 by A89,SQUARE_1:47;
then px`1<=1 & 1>= -px`1 or px`1>= -1 & -px`1>=px`2 by A81,A90,XXREAL_0:2
;
then px`1<=1 & -1<= --px`1 or px`1>= -1 & -px`1>= -1
by A91,XREAL_1:24,XXREAL_0:2;
then px`1<=1 & -1<=px`1 or px`1>= -1 & --px`1<= --1 by XREAL_1:24;
then px in Kb by A1,A90,A91;
hence ex x being set st x in dom Sq_Circ & x in Kb & y=Sq_Circ.x
by A28,A80,A82,A83,A84,EUCLID:53;
end;
end;
hence thesis by FUNCT_1:def 6;
end;
theorem Th28:
for Kb,Cb being Subset of TOP-REAL 2 st
Kb={p: not(-1

0.TOP-REAL 2 & (q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
then
A9: Sq_Circ.q=|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2 )]|
by JGRAPH_3:def 1;
A10: not(-1

=q`1 or q`1>=1
proof
assume
A11: not(-1

=q`2;
then -q`1<= -1 or q`2>=q`1 & q`2<= -q`1 by A8,XXREAL_0:2;
hence thesis by A12,XREAL_1:24,XXREAL_0:2;
end;
case q`2>=1;
then 1<=q`1 or 1<= -q`1 by A8,XXREAL_0:2;
then 1<=q`1 or --q`1<= -1 by XREAL_1:24;
hence thesis;
end;
end;
hence thesis;
end;
A13: (|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|)`1 = q`1/sqrt(1+(q
`2/q`1)^2) by EUCLID:52;
A14: (|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|)`2 = q`2/sqrt(1+(q
`2/q`1)^2) by EUCLID:52;
A15: 1+(q`2/q`1)^2>0 by XREAL_1:34,63;
A16: now
assume
A17: q`1=0;
then q`2=0 by A8;
hence contradiction by A8,A17,EUCLID:53,54;
end;
then
A18: (q`1)^2>0 by SQUARE_1:12;
(q`1)^2>=1^2 by A5,A10,SQUARE_1:48;
then
A19: sqrt((q`1)^2)>=1 by SQUARE_1:18,26;
|.(|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|).|^2
=((q`1)/sqrt(1+(q`2/(q`1))^2))^2+(q`2/sqrt(1+(q`2/(q`1))^2))^2
by A13,A14,JGRAPH_3:1
.=(q`1)^2/(sqrt(1+(q`2/(q`1))^2))^2+(q`2/sqrt(1+(q`2/(q`1))^2))^2
by XCMPLX_1:76
.=(q`1)^2/(sqrt(1+(q`2/(q`1))^2))^2
+(q`2)^2/(sqrt(1+(q`2/(q`1))^2))^2 by XCMPLX_1:76
.=(q`1)^2/(1+(q`2/q`1)^2)+(q`2)^2/(sqrt(1+(q`2/q`1)^2))^2
by A15,SQUARE_1:def 2
.=(q`1)^2/(1+(q`2/q`1)^2)+(q`2)^2/(1+(q`2/q`1)^2)
by A15,SQUARE_1:def 2
.=((q`1)^2+(q`2)^2)/(1+(q`2/q`1)^2) by XCMPLX_1:62
.=((q`1)^2+(q`2)^2)/(1+(q`2)^2/(q`1)^2) by XCMPLX_1:76
.=((q`1)^2+(q`2)^2)/((q`1)^2/(q`1)^2+(q`2)^2/(q`1)^2)
by A18,XCMPLX_1:60
.=((q`1)^2+(q`2)^2)/(((q`1)^2+(q`2)^2)/(q`1)^2)
by XCMPLX_1:62
.=(q`1)^2*(((q`1)^2+(q`2)^2)/((q`1)^2+(q`2)^2))
by XCMPLX_1:81
.=(q`1)^2*1 by A16,COMPLEX1:1,XCMPLX_1:60
.=(q`1)^2;
then |.(|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|).|>=1
by A19,SQUARE_1:22;
hence ex p2 being Point of TOP-REAL 2 st p2=y & |.p2.|>=1 by A3,A4,A9;
end;
case
A20: q<>0.TOP-REAL 2 & not(q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
then
A21: Sq_Circ.q=|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2 )]|
by JGRAPH_3:def 1;
A22: (|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|)`1 = q`1/sqrt(1+(q
`1/q`2)^2) by EUCLID:52;
A23: (|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|)`2 = q`2/sqrt(1+(q
`1/q`2)^2) by EUCLID:52;
A24: 1+(q`1/q`2)^2>0 by XREAL_1:34,63;
A25: q`2 <> 0 by A20;
then
A26: (q`2)^2>0 by SQUARE_1:12;
not(-1

=q`2 or q`2>=1
proof
assume
A27: not(-1

=q`1;
then q`2<= -1 or q`1

=q`2 by A28,XXREAL_0:2;
hence thesis by XREAL_1:24;
end;
case
A29: q`1>=1;
--q`1<= -q`2 & q`2<=q`1 or q`2>=q`1 & q`2>= -q`1
by A20,XREAL_1:24;
then 1<= -q`2 or q`2>=q`1 & q`2>= -q`1 by A29,XXREAL_0:2;
then -1>= --q`2 or 1<=q`2 by A29,XREAL_1:24,XXREAL_0:2;
hence thesis;
end;
end;
hence thesis;
end;
then (q`2)^2>=1^2 by A5,SQUARE_1:48;
then
A30: sqrt((q`2)^2)>=1 by SQUARE_1:18,26;
|.(|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|).|^2
=((q`1)/sqrt(1+(q`1/(q`2))^2))^2+(q`2/sqrt(1+(q`1/(q`2))^2))^2
by A22,A23,JGRAPH_3:1
.=(q`1)^2/(sqrt(1+(q`1/(q`2))^2))^2+(q`2/sqrt(1+(q`1/(q`2))^2))^2
by XCMPLX_1:76
.=(q`1)^2/(sqrt(1+(q`1/(q`2))^2))^2
+(q`2)^2/(sqrt(1+(q`1/(q`2))^2))^2 by XCMPLX_1:76
.=(q`1)^2/(1+(q`1/q`2)^2)+(q`2)^2/(sqrt(1+(q`1/q`2)^2))^2
by A24,SQUARE_1:def 2
.=(q`1)^2/(1+(q`1/q`2)^2)+(q`2)^2/(1+(q`1/q`2)^2)
by A24,SQUARE_1:def 2
.=((q`1)^2+(q`2)^2)/(1+(q`1/q`2)^2) by XCMPLX_1:62
.=((q`1)^2+(q`2)^2)/(1+(q`1)^2/(q`2)^2) by XCMPLX_1:76
.=((q`1)^2+(q`2)^2)/((q`1)^2/(q`2)^2+(q`2)^2/(q`2)^2)
by A26,XCMPLX_1:60
.=((q`1)^2+(q`2)^2)/(((q`1)^2+(q`2)^2)/(q`2)^2) by XCMPLX_1:62
.=(q`2)^2*(((q`1)^2+(q`2)^2)/((q`1)^2+(q`2)^2)) by XCMPLX_1:81
.=(q`2)^2*1 by A25,COMPLEX1:1,XCMPLX_1:60
.=(q`2)^2;
then |.(|[q`1/sqrt(1+(q`1/q`2)^2),q`2/sqrt(1+(q`1/q`2)^2)]|).|>=1
by A30,SQUARE_1:22;
hence ex p2 being Point of TOP-REAL 2 st p2=y & |.p2.|>=1 by A3,A4,A21;
end;
end;
hence thesis by A1;
end;
let y be object;
assume y in Cb;
then consider p2 being Point of TOP-REAL 2 such that
A31: p2=y and
A32: |.p2.|>=1 by A1;
set q=p2;
now per cases;
case q=0.TOP-REAL 2;
hence contradiction by A32,TOPRNS_1:23;
end;
case
A33: q<>0.TOP-REAL 2 & (q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
set px=|[q`1*sqrt(1+(q`2/q`1)^2),q`2*sqrt(1+(q`2/q`1)^2)]|;
A34: px`1 = q`1*sqrt(1+(q`2/q`1)^2) by EUCLID:52;
A35: px`2 = q`2*sqrt(1+(q`2/q`1)^2) by EUCLID:52;
1+(q`2/q`1)^2>0 by XREAL_1:34,63;
then
A36: sqrt(1+(q`2/q`1)^2)>0 by SQUARE_1:25;
A37: 1+(px`2/px`1)^2>0 by XREAL_1:34,63;
A38: px`2/px`1=q`2/q`1 by A34,A35,A36,XCMPLX_1:91;
A39: q`1=q`1*sqrt(1+(q`2/q`1)^2)/(sqrt(1+(q`2/q`1)^2))by A36,XCMPLX_1:89
.=px`1/(sqrt(1+(q`2/q`1)^2)) by EUCLID:52;
A40: q`2=q`2*sqrt(1+(q`2/q`1)^2)/(sqrt(1+(q`2/q`1)^2))by A36,XCMPLX_1:89
.=px`2/(sqrt(1+(q`2/q`1)^2)) by EUCLID:52;
A41: |.q.|^2=q`1^2+q`2^2 by JGRAPH_3:1;
A42: |.q.|^2>=1^2 by A32,SQUARE_1:15;
A43: now
assume that
A44: px`1=0 and
A45: px`2=0;
A46: q`1*sqrt(1+(q`2/q`1)^2)=0 by A44,EUCLID:52;
A47: q`2*sqrt(1+(q`2/q`1)^2)=0 by A45,EUCLID:52;
A48: q`1=0 by A36,A46,XCMPLX_1:6;
q`2=0 by A36,A47,XCMPLX_1:6;
hence contradiction by A33,A48,EUCLID:53,54;
end;
q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 &
q`2*sqrt(1+(q`2/q`1)^2) <= (-q`1)*sqrt(1+(q`2/q`1)^2)
by A33,A36,XREAL_1:64;
then
A49: q`2<=q`1 & (-q`1)*sqrt(1+(q`2/q`1)^2) <= q`2*sqrt(1+(q`2/q`1) ^2)
or px`2>=px`1 & px`2<=-px`1 by A34,A35,A36,XREAL_1:64;
then px`2<=px`1 & -px`1<=px`2 or px`2>=px`1 & px`2<=-px`1
by A34,A35,A36,XREAL_1:64;
then
A50: Sq_Circ
.px=|[px`1/sqrt(1+(px`2/px`1)^2),px`2/sqrt(1+(px`2/px`1 )^2) ]|
by A43,JGRAPH_2:3,JGRAPH_3:def 1;
A51: px`1/sqrt(1+(px`2/px`1)^2)=q`1 by A34,A36,A38,XCMPLX_1:89;
A52: px`2/sqrt(1+(px`2/px`1)^2)=q`2 by A35,A36,A38,XCMPLX_1:89;
A53: dom Sq_Circ=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
not px`1=0 by A34,A35,A36,A43,A49,XREAL_1:64;
then
A54: (px`1)^2>0 by SQUARE_1:12;
then
A55: (px`1)^2+(px`2)^2>0 by XREAL_1:34,63;
(px`1)^2/(sqrt(1+(px`2/px`1)^2))^2+(px`2/sqrt(1+(px`2/px`1)^2)) ^2 >= 1
by A38,A39,A40,A41,A42,XCMPLX_1:76;
then
(px`1)^2/(sqrt(1+(px`2/px`1)^2))^2+(px`2)^2/(sqrt(1+(px`2/px`1)^2))
^2>=1 by XCMPLX_1:76;
then (px`1)^2/(1+(px`2/px`1)^2)+(px`2)^2/(sqrt(1+(px`2/px`1)^2))^2>=1
by A37,SQUARE_1:def 2;
then (px`1)^2/(1+(px`2/px`1)^2)+(px`2)^2/(1+(px`2/px`1)^2)>=1
by A37,SQUARE_1:def 2;
then ((px`1)^2/(1+(px`2/px`1)^2)
+(px`2)^2/(1+(px`2/px`1)^2))*(1+(px`2/px`1)^2)>=1 *(1+(px`2/px`1)^2)
by A37,XREAL_1:64;
then (px`1)^2/(1+(px`2/px`1)^2)*(1+(px`2/px`1)^2)
+(px`2)^2/(1+(px`2/px`1)^2)*(1+(px`2/px`1)^2)>=1 *(1+(px`2/px`1)^2);
then (px`1)^2+(px`2)^2/(1+(px`2/px`1)^2)*(1+(px`2/px`1)^2)
>=1 *(1+(px`2/px`1)^2) by A37,XCMPLX_1:87;
then
A56: (px`1)^2+(px`2)^2>=1 *(1+(px`2/px`1)^2) by A37,XCMPLX_1:87;
1 *(1+(px`2/px`1)^2) =1+(px`2)^2/(px`1)^2 by XCMPLX_1:76;
then (px`1)^2+(px`2)^2-1>=1+(px`2)^2/(px`1)^2-1 by A56,XREAL_1:9;
then ((px`1)^2+(px`2)^2-1)*(px`1)^2>=((px`2)^2/(px`1)^2)*(px`1)^2
by A54,XREAL_1:64;
then ((px`1)^2+((px`2)^2-1))*(px`1)^2>=(px`2)^2 by A54,XCMPLX_1:87;
then
A57: (px`1)^2*(px`1)^2+(px`1)^2*((px`2)^2-1)-(px`2)^2>=0 by XREAL_1:48;
(px`1)^2*(px`1)^2+((px`1)^2*(px`2)^2-(px`1)^2*1)-(px`2)^2
= ((px`1)^2-1)*((px`1)^2+(px`2)^2);
then (px`1)^2-1>=0 by A55,A57,XREAL_1:132;
then (px`1)^2-1+1>=0+1 by XREAL_1:7;
then px`1>=1^2 or px`1<= -1 by SQUARE_1:50;
then px in Kb by A1;
hence ex x being set st x in dom Sq_Circ & x in Kb & y=Sq_Circ.x
by A31,A50,A51,A52,A53,EUCLID:53;
end;
case
A58: q<>0.TOP-REAL 2 & not(q`2<=q`1 & -q`1<=q`2 or q`2>=q`1 & q`2<=-q`1);
set px=|[q`1*sqrt(1+(q`1/q`2)^2),q`2*sqrt(1+(q`1/q`2)^2)]|;
A59: q`1<=q`2 & -q`2<=q`1 or q`1>=q`2 & q`1<=-q`2 by A58,JGRAPH_2:13;
A60: px`2 = q`2*sqrt(1+(q`1/q`2)^2) by EUCLID:52;
A61: px`1 = q`1*sqrt(1+(q`1/q`2)^2) by EUCLID:52;
1+(q`1/q`2)^2>0 by XREAL_1:34,63;
then
A62: sqrt(1+(q`1/q`2)^2)>0 by SQUARE_1:25;
A63: 1+(px`1/px`2)^2>0 by XREAL_1:34,63;
A64: px`1/px`2=q`1/q`2 by A60,A61,A62,XCMPLX_1:91;
A65: q`2=q`2*sqrt(1+(q`1/q`2)^2)/(sqrt(1+(q`1/q`2)^2))by A62,XCMPLX_1:89
.=px`2/(sqrt(1+(q`1/q`2)^2)) by EUCLID:52;
A66: q`1=q`1*sqrt(1+(q`1/q`2)^2)/(sqrt(1+(q`1/q`2)^2))by A62,XCMPLX_1:89
.=px`1/(sqrt(1+(q`1/q`2)^2)) by EUCLID:52;
A67: |.q.|^2=q`2^2+q`1^2 by JGRAPH_3:1;
A68: |.q.|^2>=1^2 by A32,SQUARE_1:15;
A69: now
assume that
A70: px`2=0 and
A71: px`1=0;
A72: q`2*sqrt(1+(q`1/q`2)^2)=0 by A70,EUCLID:52;
q`1*sqrt(1+(q`1/q`2)^2)=0 by A71,EUCLID:52;
then q`1=0 by A62,XCMPLX_1:6;
hence contradiction by A58,A62,A72,XCMPLX_1:6;
end;
q`1<=q`2 & -q`2<=q`1 or q`1>=q`2 &
q`1*sqrt(1+(q`1/q`2)^2) <= (-q`2)*sqrt(1+(q`1/q`2)^2)
by A59,A62,XREAL_1:64;
then
A73: q`1<=q`2 & (-q`2)*sqrt(1+(q`1/q`2)^2) <= q`1*sqrt(1+(q`1/q`2) ^2)
or px`1>=px`2 & px`1<=-px`2 by A60,A61,A62,XREAL_1:64;
then px`1<=px`2 & -px`2<=px`1 or px`1>=px`2 & px`1<=-px`2
by A60,A61,A62,XREAL_1:64;
then
A74: Sq_Circ
.px=|[px`1/sqrt(1+(px`1/px`2)^2),px`2/sqrt(1+(px`1/px`2 )^2) ]|
by A69,JGRAPH_2:3,JGRAPH_3:4;
A75: px`2/sqrt(1+(px`1/px`2)^2)=q`2 by A60,A62,A64,XCMPLX_1:89;
A76: px`1/sqrt(1+(px`1/px`2)^2)=q`1 by A61,A62,A64,XCMPLX_1:89;
A77: dom Sq_Circ=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
not px`2=0 by A60,A61,A62,A69,A73,XREAL_1:64;
then
A78: (px`2)^2>0 by SQUARE_1:12;
A79: (px`1)^2>=0 by XREAL_1:63;
(px`2)^2/(sqrt(1+(px`1/px`2)^2))^2+(px`1/sqrt(1+(px`1/px`2)^2)) ^2 >= 1
by A64,A65,A66,A67,A68,XCMPLX_1:76;
then
(px`2)^2/(sqrt(1+(px`1/px`2)^2))^2+(px`1)^2/(sqrt(1+(px`1/px`2)^2))
^2>=1 by XCMPLX_1:76;
then (px`2)^2/(1+(px`1/px`2)^2)+(px`1)^2/(sqrt(1+(px`1/px`2)^2))^2>=1
by A63,SQUARE_1:def 2;
then (px`2)^2/(1+(px`1/px`2)^2)+(px`1)^2/(1+(px`1/px`2)^2)>=1
by A63,SQUARE_1:def 2;
then ((px`2)^2/(1+(px`1/px`2)^2)
+(px`1)^2/(1+(px`1/px`2)^2))*(1+(px`1/px`2)^2)>=1 *(1+(px`1/px`2)^2)
by A63,XREAL_1:64;
then (px`2)^2/(1+(px`1/px`2)^2)*(1+(px`1/px`2)^2)
+(px`1)^2/(1+(px`1/px`2)^2)*(1+(px`1/px`2)^2)>=1 *(1+(px`1/px`2)^2);
then (px`2)^2+(px`1)^2/(1+(px`1/px`2)^2)*(1+(px`1/px`2)^2)
>=1 *(1+(px`1/px`2)^2) by A63,XCMPLX_1:87;
then
A80: (px`2)^2+(px`1)^2>=1 *(1+(px`1/px`2)^2) by A63,XCMPLX_1:87;
1 *(1+(px`1/px`2)^2) =1+(px`1)^2/(px`2)^2 by XCMPLX_1:76;
then (px`2)^2+(px`1)^2-1>=1+(px`1)^2/(px`2)^2-1 by A80,XREAL_1:9;
then ((px`2)^2+(px`1)^2-1)*(px`2)^2>=((px`1)^2/(px`2)^2)*(px`2)^2
by A78,XREAL_1:64;
then ((px`2)^2+((px`1)^2-1))*(px`2)^2>=(px`1)^2 by A78,XCMPLX_1:87;
then
A81: (px`2)^2*(px`2)^2+(px`2)^2*((px`1)^2-1)-(px`1)^2>=0 by XREAL_1:48;
(px`2)^2*(px`2)^2+((px`2)^2*(px`1)^2-(px`2)^2*1)-(px`1)^2
= ((px`2)^2-1)*((px`2)^2+(px`1)^2);
then (px`2)^2-1>=0 & (px`1)^2+(px`2)^2>=0 or
(px`2)^2-1<=0 & (px`1)^2+(px`2)^2<=0 by A81,XREAL_1:132;
then (px`2)^2-1+1>=0+1 by A78,A79,XREAL_1:7;
then px`2>=1^2 or px`2<= -1 by SQUARE_1:50;
then px in Kb by A1;
hence ex x being set st x in dom Sq_Circ & x in Kb & y=Sq_Circ.x
by A31,A74,A75,A76,A77,EUCLID:53;
end;
end;
hence thesis by FUNCT_1:def 6;
end;
theorem
for P0,P1,P01,P11,K0,K1,K01,K11 being Subset of TOP-REAL 2,
P being non empty compact Subset of TOP-REAL 2,
f being Function of TOP-REAL 2,TOP-REAL 2 st P= circle(0,0,1) &
P0= inside_of_circle(0,0,1) & P1= outside_of_circle(0,0,1) &
P01= closed_inside_of_circle(0,0,1) & P11= closed_outside_of_circle(0,0,1) &
K0=inside_of_rectangle(-1,1,-1,1) & K1=outside_of_rectangle(-1,1,-1,1) &
K01=closed_inside_of_rectangle(-1,1,-1,1) &
K11=closed_outside_of_rectangle(-1,1,-1,1) & f=Sq_Circ
holds f.:rectangle(-1,1,-1,1)=P & f".:P=rectangle(-1,1,-1,1) &
f.:K0=P0 & f".:P0=K0 & f.:K1=P1 & f".:P1=K1 &
f.:K01=P01 & f.:K11=P11 & f".:P01=K01 & f".:P11=K11
proof
let P0,P1,P01,P11,K0,K1,K01,K11 be Subset of TOP-REAL 2,
P being non empty compact Subset of TOP-REAL 2,
f be Function of TOP-REAL 2,TOP-REAL 2;
assume that
A1: P= circle(0,0,1) and
A2: P0= inside_of_circle(0,0,1) and
A3: P1= outside_of_circle(0,0,1) and
A4: P01= closed_inside_of_circle(0,0,1) and
A5: P11= closed_outside_of_circle(0,0,1) and
A6: K0=inside_of_rectangle(-1,1,-1,1) and
A7: K1=outside_of_rectangle(-1,1,-1,1) and
A8: K01=closed_inside_of_rectangle(-1,1,-1,1) and
A9: K11=closed_outside_of_rectangle(-1,1,-1,1) and
A10: f=Sq_Circ;
set K=rectangle(-1,1,-1,1);
A11: P0={p: |.p.| <1} by A2,Th24;
A12: P01={p: |.p.| <=1} by A4,Th24;
A13: P1={p: |.p.| >1} by A3,Th24;
A14: P11={p: |.p.| >=1} by A5,Th24;
defpred P[Point of TOP-REAL 2] means
$1`1 = -1 & $1`2 <= 1 & $1`2 >= -1 or $1`1 <= 1 & $1`1 >= -1 & $1`2 = 1 or
$1`1 <= 1 & $1`1 >= -1 & $1`2 = -1 or $1`1 = 1 & $1`2 <= 1 & $1`2 >= -1;
defpred Q[Point of TOP-REAL 2] means
-1=$1`1 & -1<=$1`2 & $1`2<=1 or $1`1=1 & -1<=$1`2 & $1`2<=1
or -1=$1`2 & -1<=$1`1 & $1`1<=1 or 1=$1`2 & -1<=$1`1 & $1`1<=1;
deffunc F(set)=$1;
A15: for p being Element of TOP-REAL 2 holds P[p] iff Q[p];
A16: K= {F(p): P[p]} by SPPOL_2:54
.= {F(q):Q[q]} from FRAENKEL:sch 3(A15);
defpred Q[Point of TOP-REAL 2] means |.$1.|=1;
defpred P[Point of TOP-REAL 2] means |.$1- |[0,0]| .|=1;
A17: for p holds P[p] iff Q[p] by EUCLID:54,RLVECT_1:13;
P= {F(p): P[p]} by A1
.= {F(p2) where p2 is Point of TOP-REAL 2: Q[p2]} from FRAENKEL:sch 3(A17
);
then
A18: f.:K=P by A10,A16,JGRAPH_3:23;
A19: dom f=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
A20: f.:K0 = P0 by A6,A10,A11,Th25;
f.:K1 = P1 by A7,A10,A13,Th26;
hence f.:K=P & f".:P=K & f.:K0=P0 & f".:P0=K0 & f.:K1=P1 & f".:P1=K1
by A10,A18,A19,A20,FUNCT_1:107;
A21: f.:K01 = P01 by A8,A10,A12,Th27;
f.:K11 = P11 by A9,A10,A14,Th28;
hence thesis by A10,A19,A21,FUNCT_1:107;
end;
begin :: Order of Points on Rectangle
theorem Th30:
for a,b,c,d being Real st a <= b & c <= d holds
LSeg(|[ a,c ]|, |[ a,d ]|) = { p1 : p1`1 = a & p1`2 <= d & p1`2 >= c}
& LSeg(|[ a,d ]|, |[ b,d ]|) = { p2 : p2`1 <= b & p2`1 >= a & p2`2 = d}
& LSeg(|[ a,c ]|, |[ b,c ]|) = { q1 : q1`1 <= b & q1`1 >= a & q1`2 = c}
& LSeg(|[ b,c ]|, |[ b,d ]|) = { q2 : q2`1 = b & q2`2 <= d & q2`2 >= c}
proof
let a,b,c,d be Real;
assume that
A1: a <= b and
A2: c <= d;
set L1 = { p : p`1 = a & p`2 <= d & p`2 >= c},
L2 = { p : p`1 <= b & p`1 >= a & p`2 = d},
L3 = { p : p`1 <= b & p`1 >= a & p`2 = c},
L4 = { p : p`1 = b & p`2 <= d & p`2 >= c};
set p0 = |[ a,c ]|, p01 = |[ a,d ]|, p10 = |[ b,c ]|, p1 = |[ b,d ]|;
A3: p01`1 = a by EUCLID:52;
A4: p01`2 = d by EUCLID:52;
A5: p10`1 = b by EUCLID:52;
A6: p10`2 = c by EUCLID:52;
A7: L1 c= LSeg(p0,p01)
proof
let a2 be object;
assume a2 in L1;
then consider p such that
A8: a2 = p and
A9: p`1 = a and
A10: p`2 <= d and
A11: p`2 >= c;
now per cases;
case
A12: d <>c;
reconsider lambda = (p`2-c)/(d-c) as Real;
d>=c by A10,A11,XXREAL_0:2;
then d>c by A12,XXREAL_0:1;
then
A13: d-c>0 by XREAL_1:50;
A14: p`2-c>=0 by A11,XREAL_1:48;
d-c>=p`2-c by A10,XREAL_1:9;
then (d-c)/(d-c)>=(p`2-c)/(d-c) by A13,XREAL_1:72;
then
A15: 1>=lambda by A13,XCMPLX_1:60;
A16: (1-lambda)*c+lambda*d
=((d-c)/(d-c)- (p`2-c)/(d-c))*c+(p`2-c)/(d-c)*d by A13,XCMPLX_1:60
.=(((d-c)- (p`2-c))/(d-c))*c+(p`2-c)/(d-c)*d by XCMPLX_1:120
.=c*((d- p`2)/(d-c))+d*(p`2-c)/(d-c) by XCMPLX_1:74
.=c*(d- p`2)/(d-c)+d*(p`2-c)/(d-c) by XCMPLX_1:74
.=((c*d- c*p`2)+(d*p`2-d*c))/(d-c) by XCMPLX_1:62
.=(d- c)*p`2/(d-c)
.=p`2*((d- c)/(d-c)) by XCMPLX_1:74
.=p`2*1 by A13,XCMPLX_1:60
.=p`2;
(1-lambda)*p0 + lambda*p01
=|[(1-lambda)*a,(1-lambda)*c]| + lambda*(|[a,d]|) by EUCLID:58
.=|[(1-lambda)*a,(1-lambda)*c]| +(|[ lambda*a, lambda*d]|)
by EUCLID:58
.=|[(1-lambda)*a+lambda*a,(1-lambda)*c+lambda*d]| by EUCLID:56
.= p by A9,A16,EUCLID:53;
hence thesis by A8,A13,A14,A15;
end;
case d =c;
then
A17: p`2=c by A10,A11,XXREAL_0:1;
reconsider lambda = 0 as Real;
(1-lambda)*p0 + lambda*p01 =
|[(1-lambda)*a,(1-lambda)*c]| + lambda*(|[a,d]|) by EUCLID:58
.=|[(1-lambda)*a,(1-lambda)*c]| +(|[ lambda*a, lambda*d]|)
by EUCLID:58
.=|[(1-lambda)*a+lambda*a,(1-lambda)*c+lambda*d]|
by EUCLID:56
.= p by A9,A17,EUCLID:53;
hence thesis by A8;
end;
end;
hence thesis;
end;
LSeg(p0,p01) c= L1
proof
let a2 be object;
assume a2 in LSeg(p0,p01);
then consider lambda such that
A18: a2 = (1-lambda)*p0 + lambda*p01 and
A19: 0 <= lambda and
A20: lambda <= 1;
set q = (1-lambda)*p0 + lambda*p01;
A21: q`1= ((1-lambda)*p0)`1 + (lambda*p01)`1 by TOPREAL3:2
.= (1-lambda)*(p0)`1 + (lambda*p01)`1 by TOPREAL3:4
.= (1-lambda)*(p0)`1 + lambda*(p01)`1 by TOPREAL3:4
.=(1-lambda)*a +lambda*a by A3,EUCLID:52
.=a;
A22: q`2= ((1-lambda)*p0)`2 + (lambda*p01)`2 by TOPREAL3:2
.= (1-lambda)*(p0)`2 + (lambda*p01)`2 by TOPREAL3:4
.= (1-lambda)*(p0)`2 + lambda*(p01)`2 by TOPREAL3:4
.= (1-lambda)*c + lambda*d by A4,EUCLID:52;
then
A23: q`2 <= d by A2,A20,XREAL_1:172;
q`2 >= c by A2,A19,A20,A22,XREAL_1:173;
hence thesis by A18,A21,A23;
end;
hence L1 = LSeg(p0,p01) by A7;
A24: L2 c= LSeg(p01,p1)
proof
let a2 be object;
assume a2 in L2;
then consider p such that
A25: a2 = p and
A26: p`1 <= b and
A27: p`1 >= a and
A28: p`2=d;
now per cases;
case
A29: b <>a;
reconsider lambda = (p`1-a)/(b-a) as Real;
b>=a by A26,A27,XXREAL_0:2;
then b>a by A29,XXREAL_0:1;
then
A30: b-a>0 by XREAL_1:50;
A31: p`1-a>=0 by A27,XREAL_1:48;
b-a>=p`1-a by A26,XREAL_1:9;
then (b-a)/(b-a)>=(p`1-a)/(b-a) by A30,XREAL_1:72;
then
A32: 1>=lambda by A30,XCMPLX_1:60;
A33: (1-lambda)*a+lambda*b
=((b-a)/(b-a)- (p`1-a)/(b-a))*a+(p`1-a)/(b-a)*b by A30,XCMPLX_1:60
.=(((b-a)- (p`1-a))/(b-a))*a+(p`1-a)/(b-a)*b by XCMPLX_1:120
.=a*((b- p`1)/(b-a))+b*(p`1-a)/(b-a) by XCMPLX_1:74
.=a*(b- p`1)/(b-a)+b*(p`1-a)/(b-a) by XCMPLX_1:74
.=((a*b- a*p`1)+(b*p`1-b*a))/(b-a) by XCMPLX_1:62
.=(b- a)*p`1/(b-a)
.=p`1*((b- a)/(b-a)) by XCMPLX_1:74
.=p`1*1 by A30,XCMPLX_1:60
.=p`1;
(1-lambda)*p01 + lambda*p1
=|[(1-lambda)*a,(1-lambda)*d]| + lambda*(|[b,d]|) by EUCLID:58
.=|[(1-lambda)*a,(1-lambda)*d]| +(|[ lambda*b, lambda*d]|)
by EUCLID:58
.=|[(1-lambda)*a+lambda*b,(1-lambda)*d+lambda*d]|
by EUCLID:56
.= p by A28,A33,EUCLID:53;
hence thesis by A25,A30,A31,A32;
end;
case b =a;
then
A34: p`1=a by A26,A27,XXREAL_0:1;
reconsider lambda = 0 as Real;
(1-lambda)*p01 + lambda*p1
=|[(1-lambda)*a,(1-lambda)*d]| + lambda*(|[b,d]|) by EUCLID:58
.=|[(1-lambda)*a,(1-lambda)*d]| +(|[ lambda*b, lambda*d]|)
by EUCLID:58
.=|[(1-lambda)*a+lambda*b,(1-lambda)*d+lambda*d]|
by EUCLID:56
.= p by A28,A34,EUCLID:53;
hence thesis by A25;
end;
end;
hence thesis;
end;
LSeg(p01,p1) c= L2
proof
let a2 be object;
assume a2 in LSeg(p01,p1);
then consider lambda such that
A35: a2 = (1-lambda)*p01 + lambda*p1 and
A36: 0 <= lambda and
A37: lambda <= 1;
set q = (1-lambda)*p01 + lambda*p1;
A38: q`2= ((1-lambda)*p01)`2 + (lambda*p1)`2 by TOPREAL3:2
.= (1-lambda)*(p01)`2 + (lambda*p1)`2 by TOPREAL3:4
.= (1-lambda)*(p01)`2 + lambda*(p1)`2 by TOPREAL3:4
.=(1-lambda)*d +lambda*d by A4,EUCLID:52
.=d;
A39: q`1= ((1-lambda)*p01)`1 + (lambda*p1)`1 by TOPREAL3:2
.= (1-lambda)*(p01)`1 + (lambda*p1)`1 by TOPREAL3:4
.= (1-lambda)*(p01)`1 + lambda*(p1)`1 by TOPREAL3:4
.= (1-lambda)*a + lambda*b by A3,EUCLID:52;
then
A40: q`1 <= b by A1,A37,XREAL_1:172;
q`1 >= a by A1,A36,A37,A39,XREAL_1:173;
hence thesis by A35,A38,A40;
end;
hence L2 = LSeg(p01,p1) by A24;
A41: L3 c= LSeg(p0,p10)
proof
let a2 be object;
assume a2 in L3;
then consider p such that
A42: a2 = p and
A43: p`1 <= b and
A44: p`1 >= a and
A45: p`2=c;
now per cases;
case
A46: b <>a;
reconsider lambda = (p`1-a)/(b-a) as Real;
b>=a by A43,A44,XXREAL_0:2;
then b>a by A46,XXREAL_0:1;
then
A47: b-a>0 by XREAL_1:50;
A48: p`1-a>=0 by A44,XREAL_1:48;
b-a>=p`1-a by A43,XREAL_1:9;
then (b-a)/(b-a)>=(p`1-a)/(b-a) by A47,XREAL_1:72;
then
A49: 1>=lambda by A47,XCMPLX_1:60;
A50: (1-lambda)*a+lambda*b
=((b-a)/(b-a)- (p`1-a)/(b-a))*a+(p`1-a)/(b-a)*b by A47,XCMPLX_1:60
.=(((b-a)- (p`1-a))/(b-a))*a+(p`1-a)/(b-a)*b by XCMPLX_1:120
.=a*((b- p`1)/(b-a))+b*(p`1-a)/(b-a) by XCMPLX_1:74
.=a*(b- p`1)/(b-a)+b*(p`1-a)/(b-a) by XCMPLX_1:74
.=((a*b- a*p`1)+(b*p`1-b*a))/(b-a) by XCMPLX_1:62
.=(b- a)*p`1/(b-a)
.=p`1*((b- a)/(b-a)) by XCMPLX_1:74
.=p`1*1 by A47,XCMPLX_1:60
.=p`1;
(1-lambda)*p0 + lambda*p10
=|[(1-lambda)*a,(1-lambda)*c]| + lambda*(|[b,c]|) by EUCLID:58
.=|[(1-lambda)*a,(1-lambda)*c]| +(|[ lambda*b, lambda*c]|)
by EUCLID:58
.=|[(1-lambda)*a+lambda*b,(1-lambda)*c+lambda*c]| by EUCLID:56
.= p by A45,A50,EUCLID:53;
hence thesis by A42,A47,A48,A49;
end;
case b =a;
then
A51: p`1=a by A43,A44,XXREAL_0:1;
reconsider lambda = 0 as Real;
(1-lambda)*p0 + lambda*p10 =
|[(1-lambda)*a,(1-lambda)*c]| + lambda*(|[b,c]|) by EUCLID:58
.=|[(1-lambda)*a,(1-lambda)*c]| +(|[ lambda*b, lambda*c]|)
by EUCLID:58
.=|[(1-lambda)*a+lambda*b,(1-lambda)*c+lambda*c]|
by EUCLID:56
.= p by A45,A51,EUCLID:53;
hence thesis by A42;
end;
end;
hence thesis;
end;
LSeg(p0,p10) c= L3
proof
let a2 be object;
assume a2 in LSeg(p0,p10);
then consider lambda such that
A52: a2 = (1-lambda)*p0 + lambda*p10 and
A53: 0 <= lambda and
A54: lambda <= 1;
set q = (1-lambda)*p0 + lambda*p10;
A55: q`2= ((1-lambda)*p0)`2 + (lambda*p10)`2 by TOPREAL3:2
.= (1-lambda)*(p0)`2 + (lambda*p10)`2 by TOPREAL3:4
.= (1-lambda)*(p0)`2 + lambda*(p10)`2 by TOPREAL3:4
.=(1-lambda)*c +lambda*c by A6,EUCLID:52
.=c;
A56: q`1= ((1-lambda)*p0)`1 + (lambda*p10)`1 by TOPREAL3:2
.= (1-lambda)*(p0)`1 + (lambda*p10)`1 by TOPREAL3:4
.= (1-lambda)*(p0)`1 + lambda*(p10)`1 by TOPREAL3:4
.= (1-lambda)*a + lambda*b by A5,EUCLID:52;
then
A57: q`1 <= b by A1,A54,XREAL_1:172;
q`1 >= a by A1,A53,A54,A56,XREAL_1:173;
hence thesis by A52,A55,A57;
end;
hence L3 = LSeg(p0,p10) by A41;
A58: L4 c= LSeg(p10,p1)
proof
let a2 be object;
assume a2 in L4;
then consider p such that
A59: a2 = p and
A60: p`1 = b and
A61: p`2 <= d and
A62: p`2 >= c;
now per cases;
case
A63: d <>c;
reconsider lambda = (p`2-c)/(d-c) as Real;
d>=c by A61,A62,XXREAL_0:2;
then d>c by A63,XXREAL_0:1;
then
A64: d-c>0 by XREAL_1:50;
A65: p`2-c>=0 by A62,XREAL_1:48;
d-c>=p`2-c by A61,XREAL_1:9;
then (d-c)/(d-c)>=(p`2-c)/(d-c) by A64,XREAL_1:72;
then
A66: 1>=lambda by A64,XCMPLX_1:60;
A67: (1-lambda)*c+lambda*d
=((d-c)/(d-c)- (p`2-c)/(d-c))*c+(p`2-c)/(d-c)*d by A64,XCMPLX_1:60
.=(((d-c)- (p`2-c))/(d-c))*c+(p`2-c)/(d-c)*d by XCMPLX_1:120
.=c*((d- p`2)/(d-c))+d*(p`2-c)/(d-c) by XCMPLX_1:74
.=c*(d- p`2)/(d-c)+d*(p`2-c)/(d-c) by XCMPLX_1:74
.=((c*d- c*p`2)+(d*p`2-d*c))/(d-c) by XCMPLX_1:62
.=(d- c)*p`2/(d-c)
.=p`2*((d- c)/(d-c)) by XCMPLX_1:74
.=p`2*1 by A64,XCMPLX_1:60
.=p`2;
(1-lambda)*p10 + lambda*p1
=|[(1-lambda)*b,(1-lambda)*c]| + lambda*(|[b,d]|) by EUCLID:58
.=|[(1-lambda)*b,(1-lambda)*c]| +(|[ lambda*b, lambda*d]|)
by EUCLID:58
.=|[(1-lambda)*b+lambda*b,(1-lambda)*c+lambda*d]|
by EUCLID:56
.= p by A60,A67,EUCLID:53;
hence thesis by A59,A64,A65,A66;
end;
case d =c;
then
A68: p`2=c by A61,A62,XXREAL_0:1;
reconsider lambda = 0 as Real;
(1-lambda)*p10 + lambda*p1
=|[(1-lambda)*b,(1-lambda)*c]| + lambda*(|[b,d]|) by EUCLID:58
.=|[(1-lambda)*b,(1-lambda)*c]| +(|[ lambda*b, lambda*d]|)
by EUCLID:58
.=|[(1-lambda)*b+lambda*b,(1-lambda)*c+lambda*d]|
by EUCLID:56
.= p by A60,A68,EUCLID:53;
hence thesis by A59;
end;
end;
hence thesis;
end;
LSeg(p10,p1) c= L4
proof
let a2 be object;
assume a2 in LSeg(p10,p1);
then consider lambda such that
A69: a2 = (1-lambda)*p10 + lambda*p1 and
A70: 0 <= lambda and
A71: lambda <= 1;
set q = (1-lambda)*p10 + lambda*p1;
A72: q`1= ((1-lambda)*p10)`1 + (lambda*p1)`1 by TOPREAL3:2
.= (1-lambda)*(p10)`1 + (lambda*p1)`1 by TOPREAL3:4
.= (1-lambda)*(p10)`1 + lambda*(p1)`1 by TOPREAL3:4
.=(1-lambda)*b +lambda*b by A5,EUCLID:52
.=b;
A73: q`2= ((1-lambda)*p10)`2 + (lambda*p1)`2 by TOPREAL3:2
.= (1-lambda)*(p10)`2 + (lambda*p1)`2 by TOPREAL3:4
.= (1-lambda)*(p10)`2 + lambda*(p1)`2 by TOPREAL3:4
.= (1-lambda)*c + lambda*d by A6,EUCLID:52;
then
A74: q`2 <= d by A2,A71,XREAL_1:172;
q`2 >= c by A2,A70,A71,A73,XREAL_1:173;
hence thesis by A69,A72,A74;
end;
hence L4 = LSeg(p10,p1) by A58;
end;
theorem Th31:
for a,b,c,d being Real st a <= b & c <= d holds
LSeg(|[a,c]|,|[a,d]|) /\ LSeg(|[a,c]|,|[b,c]|) = {|[a,c]|}
proof
let a,b,c,d be Real;
assume that
A1: a <= b and
A2: c <= d;
for ax being object
holds ax in LSeg(|[a,c]|,|[a,d]|) /\ LSeg(|[a,c]|,|[b,c]|) iff ax = |[a,c]|
proof
let ax be object;
thus ax in LSeg(|[a,c]|,|[a,d]|) /\ LSeg(|[a,c]|,|[b,c]|)
implies ax = |[a,c]|
proof
assume
A3: ax in LSeg(|[a,c]|,|[a,d]|) /\ LSeg(|[a,c]|,|[b,c]|);
then
A4: ax in LSeg(|[a,c]|,|[a,d]|) by XBOOLE_0:def 4;
ax in LSeg(|[a,c]|,|[b,c]|) by A3,XBOOLE_0:def 4;
then ax in { p2 : p2`1 <= b & p2`1 >= a & p2`2 = c } by A1,Th30;
then
A5: ex p2 st p2 = ax & p2`1 <= b & p2`1 >= a & p2`2 = c;
ax in { p2 : p2`1 = a & p2`2 <= d & p2`2 >= c } by A2,A4,Th30;
then ex p st p = ax & p`1 = a & p`2 <= d & p`2 >= c;
hence thesis by A5,EUCLID:53;
end;
assume
A6: ax = |[a,c]|;
then
A7: ax in LSeg(|[a,c]|,|[a,d]|) by RLTOPSP1:68;
ax in LSeg(|[a,c]|,|[b,c]|) by A6,RLTOPSP1:68;
hence thesis by A7,XBOOLE_0:def 4;
end;
hence thesis by TARSKI:def 1;
end;
theorem Th32:
for a,b,c,d being Real st a <= b & c <= d holds
LSeg(|[a,c]|,|[b,c]|) /\ LSeg(|[b,c]|,|[b,d]|) = {|[b,c]|}
proof
let a,b,c,d be Real;
assume that
A1: a <= b and
A2: c <= d;
for ax being object
holds ax in LSeg(|[a,c]|,|[b,c]|) /\ LSeg(|[b,c]|,|[b,d]|) iff ax = |[b,c]|
proof
let ax be object;
thus ax in LSeg(|[a,c]|,|[b,c]|) /\ LSeg(|[b,c]|,|[b,d]|)
implies ax = |[b,c]|
proof
assume
A3: ax in LSeg(|[a,c]|,|[b,c]|) /\ LSeg(|[b,c]|,|[b,d]|);
then
A4: ax in LSeg(|[a,c]|,|[b,c]|) by XBOOLE_0:def 4;
A5: ax in LSeg(|[b,c]|,|[b,d]|) by A3,XBOOLE_0:def 4;
ax in { q1 : q1`1 <= b & q1`1 >= a & q1`2 = c} by A1,A4,Th30;
then
A6: ex p2 st p2 = ax & p2`1 <= b & p2`1 >= a & p2`2 = c;
ax in { q2 : q2`1 = b & q2`2 <= d & q2`2 >= c} by A2,A5,Th30;
then ex p st p = ax & p`1 = b & p`2 <= d & p`2 >= c;
hence thesis by A6,EUCLID:53;
end;
assume
A7: ax = |[b,c]|;
then
A8: ax in LSeg(|[a,c]|,|[b,c]|) by RLTOPSP1:68;
ax in LSeg(|[b,c]|,|[b,d]|) by A7,RLTOPSP1:68;
hence thesis by A8,XBOOLE_0:def 4;
end;
hence thesis by TARSKI:def 1;
end;
theorem Th33:
for a,b,c,d being Real st a <= b & c <= d holds
LSeg(|[a,d]|,|[b,d]|) /\ LSeg(|[b,c]|,|[b,d]|) = {|[b,d]|}
proof
let a,b,c,d be Real;
assume that
A1: a <= b and
A2: c <= d;
for ax being object
holds ax in LSeg(|[a,d]|,|[b,d]|) /\ LSeg(|[b,c]|,|[b,d]|) iff ax = |[b,d]|
proof
let ax be object;
thus ax in LSeg(|[a,d]|,|[b,d]|) /\ LSeg(|[b,c]|,|[b,d]|)
implies ax = |[b,d]|
proof
assume
A3: ax in LSeg(|[a,d]|,|[b,d]|) /\ LSeg(|[b,c]|,|[b,d]|);
then
A4: ax in LSeg(|[b,c]|,|[b,d]|) by XBOOLE_0:def 4;
ax in LSeg(|[a,d]|,|[b,d]|) by A3,XBOOLE_0:def 4;
then ax in { p : p`1 <= b & p`1 >= a & p`2 = d} by A1,Th30;
then
A5: ex p st p = ax & p`1 <= b & p`1 >= a & p`2 = d;
ax in { p : p`1 = b & p`2 <= d & p`2 >= c} by A2,A4,Th30;
then ex p2 st p2 = ax & p2`1 = b & p2`2 <= d & p2`2 >= c;
hence thesis by A5,EUCLID:53;
end;
assume
A6: ax = |[b,d]|;
then
A7: ax in LSeg(|[a,d]|,|[b,d]|) by RLTOPSP1:68;
ax in LSeg(|[b,c]|,|[b,d]|) by A6,RLTOPSP1:68;
hence thesis by A7,XBOOLE_0:def 4;
end;
hence thesis by TARSKI:def 1;
end;
theorem Th34:
for a,b,c,d being Real st a <= b & c <= d holds
LSeg(|[a,c]|,|[a,d]|) /\ LSeg(|[a,d]|,|[b,d]|) = {|[a,d]|}
proof
let a,b,c,d be Real;
assume that
A1: a <= b and
A2: c <= d;
for ax being object
holds ax in LSeg(|[a,c]|,|[a,d]|) /\ LSeg(|[a,d]|,|[b,d]|) iff ax = |[a,d]|
proof
let ax be object;
thus ax in LSeg(|[a,c]|,|[a,d]|) /\ LSeg(|[a,d]|,|[b,d]|)
implies ax = |[a,d]|
proof
assume
A3: ax in LSeg(|[a,c]|,|[a,d]|) /\ LSeg(|[a,d]|,|[b,d]|);
then
A4: ax in LSeg(|[a,c]|,|[a,d]|) by XBOOLE_0:def 4;
ax in LSeg(|[a,d]|,|[b,d]|) by A3,XBOOLE_0:def 4;
then ax in { p2 : p2`1 <= b & p2`1 >= a & p2`2 = d } by A1,Th30;
then
A5: ex p2 st p2 = ax & p2`1 <= b & p2`1 >= a & p2`2 = d;
ax in { p2 : p2`1 = a & p2`2 <= d & p2`2 >= c } by A2,A4,Th30;
then ex p st p = ax & p`1 = a & p`2 <= d & p`2 >= c;
hence thesis by A5,EUCLID:53;
end;
assume
A6: ax = |[a,d]|;
then
A7: ax in LSeg(|[a,c]|,|[a,d]|) by RLTOPSP1:68;
ax in LSeg(|[a,d]|,|[b,d]|) by A6,RLTOPSP1:68;
hence thesis by A7,XBOOLE_0:def 4;
end;
hence thesis by TARSKI:def 1;
end;
theorem Th35:
{q: -1=q`1 & -1<=q`2 & q`2<=1 or q`1=1 & -1<=q`2 & q`2<=1
or -1=q`2 & -1<=q`1 & q`1<=1 or 1=q`2 & -1<=q`1 & q`1<=1}
= {p: p`1=-1 & -1 <=p`2 & p`2<=1 or p`2=1 & -1<=p`1 & p`1<=1 or
p`1=1 & -1 <=p`2 & p`2<=1 or p`2=-1 & -1<=p`1 & p`1<=1}
proof
thus {q: -1=q`1 & -1<=q`2 & q`2<=1 or q`1=1 & -1<=q`2 & q`2<=1
or -1=q`2 & -1<=q`1 & q`1<=1 or 1=q`2 & -1<=q`1 & q`1<=1}
c= {p: p`1=-1 & -1 <=p`2 & p`2<=1 or p`2=1 & -1<=p`1 & p`1<=1 or
p`1=1 & -1 <=p`2 & p`2<=1 or p`2=-1 & -1<=p`1 & p`1<=1}
proof
let x be object;
assume x in {q: -1=q`1 & -1<=q`2 & q`2<=1 or q`1=1 & -1<=q`2 & q`2<=1
or -1=q`2 & -1<=q`1 & q`1<=1 or 1=q`2 & -1<=q`1 & q`1<=1};
then ex q st ( x=q)&( -1=q`1 & -1<=q`2 & q`2<=1 or q`1=1 & -1<=q
`2 & q`2<=1 or -1=q`2 & -1<=q`1 & q`1<=1 or 1=q`2 & -1<=q`1 & q`1<=1);
hence thesis;
end;
thus {p: p`1=-1 & -1 <=p`2 & p`2<=1 or p`2=1 & -1<=p`1 & p`1<=1 or
p`1=1 & -1 <=p`2 & p`2<=1 or p`2=-1 & -1<=p`1 & p`1<=1}
c= {q: -1=q`1 & -1<=q`2 & q`2<=1 or q`1=1 & -1<=q`2 & q`2<=1
or -1=q`2 & -1<=q`1 & q`1<=1 or 1=q`2 & -1<=q`1 & q`1<=1}
proof
let x be object;
assume x in {p: p`1=-1 & -1 <=p`2 & p`2<=1 or p`2=1 & -1<=p`1 & p`1<=1 or
p`1=1 & -1 <=p`2 & p`2<=1 or p`2=-1 & -1<=p`1 & p`1<=1};
then ex p st ( p=x)&( p`1=-1 & -1 <=p`2 & p`2<=1 or p`2=1 & -1<=
p`1 & p`1<=1 or p`1=1 & -1 <=p`2 & p`2<=1 or p`2=-1 & -1<=p`1 & p`1<=1);
hence thesis;
end;
end;
theorem Th36:
for a,b,c,d being Real st a<=b & c <=d
holds W-bound rectangle(a,b,c,d) = a
proof
let a,b,c,d be Real;
assume that
A1: a<=b and
A2: c <=d;
set X = rectangle(a,b,c,d);
reconsider Z = (proj1|X).:the carrier of ((TOP-REAL 2)|X)
as Subset of REAL;
A3: X = the carrier of ((TOP-REAL 2)|X) by PRE_TOPC:8;
A4: for p be Real st p in Z holds p >= a
proof
let p be Real;
assume p in Z;
then consider p0 being object such that
A5: p0 in the carrier of (TOP-REAL 2)|X and
p0 in the carrier of (TOP-REAL 2)|X and
A6: p = (proj1|X).p0 by FUNCT_2:64;
reconsider p0 as Point of TOP-REAL 2 by A3,A5;
X= {q : q`1 = a & q`2 <= d & q`2 >= c or q`1 <= b & q`1 >= a & q`2 = d or
q`1 <= b & q`1 >= a & q`2 = c or q`1 = b & q`2 <= d & q`2 >= c}
by A1,A2,SPPOL_2:54;
then ex q being Point of TOP-REAL 2 st p0 = q &
(q`1 = a & q`2 <= d & q`2 >= c or q`1 <= b & q`1 >= a & q`2 = d or
q`1 <= b & q`1 >= a & q`2 = c or q`1 = b & q`2 <= d & q`2 >= c) by A3,A5;
hence thesis by A1,A3,A5,A6,PSCOMP_1:22;
end;
A7: for q being Real st
for p being Real st p in Z holds p >= q holds a >= q
proof
let q be Real such that
A8: for p being Real st p in Z holds p >= q;
|[a,c]| in LSeg(|[ a,c ]|, |[ b,c ]|) by RLTOPSP1:68;
then
A9: |[a,c]| in LSeg(|[ a,c ]|, |[ b,c ]|) \/ LSeg(|[ b,c ]|, |[ b,d ]| )
by XBOOLE_0:def 3;
X= (LSeg(|[ a,c ]|, |[ a,d ]|) \/ LSeg(|[ a,d ]|, |[ b,d ]|))
\/ (LSeg(|[ a,c ]|, |[ b,c ]|) \/ LSeg(|[ b,c ]|, |[ b,d ]|))
by SPPOL_2:def 3;
then
A10: |[a,c]| in X by A9,XBOOLE_0:def 3;
then (proj1|X). |[a,c]| = |[a,c]|`1 by PSCOMP_1:22
.= a by EUCLID:52;
hence thesis by A3,A8,A10,FUNCT_2:35;
end;
thus W-bound X = lower_bound (proj1|X) by PSCOMP_1:def 7
.= lower_bound Z by PSCOMP_1:def 1
.= a by A4,A7,SEQ_4:44;
end;
theorem Th37:
for a,b,c,d being Real st a<=b & c <=d
holds N-bound rectangle(a,b,c,d) = d
proof
let a,b,c,d be Real;
assume that
A1: a<=b and
A2: c <=d;
set X = rectangle(a,b,c,d);
reconsider Z = (proj2|X).:the carrier of ((TOP-REAL 2)|X)
as Subset of REAL;
A3: X = the carrier of ((TOP-REAL 2)|X) by PRE_TOPC:8;
A4: for p be Real st p in Z holds p <= d
proof
let p be Real;
assume p in Z;
then consider p0 being object such that
A5: p0 in the carrier of (TOP-REAL 2)|X and
p0 in the carrier of (TOP-REAL 2)|X and
A6: p = (proj2|X).p0 by FUNCT_2:64;
reconsider p0 as Point of TOP-REAL 2 by A3,A5;
X= {q : q`1 = a & q`2 <= d & q`2 >= c or q`1 <= b & q`1 >= a & q`2 = d or
q`1 <= b & q`1 >= a & q`2 = c or q`1 = b & q`2 <= d & q`2 >= c}
by A1,A2,SPPOL_2:54;
then ex q being Point of TOP-REAL 2 st p0 = q &
(q`1 = a & q`2 <= d & q`2 >= c or q`1 <= b & q`1 >= a & q`2 = d or
q`1 <= b & q`1 >= a & q`2 = c or q`1 = b & q`2 <= d & q`2 >= c) by A3,A5;
hence thesis by A2,A3,A5,A6,PSCOMP_1:23;
end;
A7: for q being Real st for p being Real
st p in Z holds p <= q holds d <= q
proof
let q be Real such that
A8: for p be Real st p in Z holds p <= q;
|[b,d]| in LSeg(|[ b,c ]|, |[ b,d ]|) by RLTOPSP1:68;
then
A9: |[b,d]| in LSeg(|[ a,c ]|, |[ b,c ]|) \/ LSeg(|[ b,c ]|, |[ b,d ]| )
by XBOOLE_0:def 3;
X= (LSeg(|[ a,c ]|, |[ a,d ]|) \/ LSeg(|[ a,d ]|, |[ b,d ]|))
\/ (LSeg(|[ a,c ]|, |[ b,c ]|) \/ LSeg(|[ b,c ]|, |[ b,d ]|))
by SPPOL_2:def 3;
then
A10: |[b,d]| in X by A9,XBOOLE_0:def 3;
then (proj2|X). |[b,d]| = |[b,d]|`2 by PSCOMP_1:23
.= d by EUCLID:52;
hence thesis by A3,A8,A10,FUNCT_2:35;
end;
thus N-bound X = upper_bound (proj2|X) by PSCOMP_1:def 8
.= upper_bound Z by PSCOMP_1:def 2
.= d by A4,A7,SEQ_4:46;
end;
theorem Th38:
for a,b,c,d being Real st a<=b & c <=d
holds E-bound rectangle(a,b,c,d) = b
proof
let a,b,c,d be Real;
assume that
A1: a<=b and
A2: c <=d;
set X = rectangle(a,b,c,d);
reconsider Z = (proj1|X).:the carrier of ((TOP-REAL 2)|X)
as Subset of REAL;
A3: X = the carrier of ((TOP-REAL 2)|X) by PRE_TOPC:8;
A4: for p be Real st p in Z holds p <= b
proof
let p be Real;
assume p in Z;
then consider p0 being object such that
A5: p0 in the carrier of (TOP-REAL 2)|X and
p0 in the carrier of (TOP-REAL 2)|X and
A6: p = (proj1|X).p0 by FUNCT_2:64;
reconsider p0 as Point of TOP-REAL 2 by A3,A5;
X= {q : q`1 = a & q`2 <= d & q`2 >= c or q`1 <= b & q`1 >= a & q`2 = d or
q`1 <= b & q`1 >= a & q`2 = c or q`1 = b & q`2 <= d & q`2 >= c}
by A1,A2,SPPOL_2:54;
then ex q being Point of TOP-REAL 2 st p0 = q &
(q`1 = a & q`2 <= d & q`2 >= c or q`1 <= b & q`1 >= a & q`2 = d or
q`1 <= b & q`1 >= a & q`2 = c or q`1 = b & q`2 <= d & q`2 >= c) by A3,A5;
hence thesis by A1,A3,A5,A6,PSCOMP_1:22;
end;
A7: for q being Real st for p being Real
st p in Z holds p <= q holds b <= q
proof
let q be Real such that
A8: for p be Real st p in Z holds p <= q;
|[b,d]| in LSeg(|[ b,c ]|, |[ b,d ]|) by RLTOPSP1:68;
then
A9: |[b,d]| in LSeg(|[ a,c ]|, |[ b,c ]|) \/ LSeg(|[ b,c ]|, |[ b,d ]| )
by XBOOLE_0:def 3;
X= (LSeg(|[ a,c ]|, |[ a,d ]|) \/ LSeg(|[ a,d ]|, |[ b,d ]|))
\/ (LSeg(|[ a,c ]|, |[ b,c ]|) \/ LSeg(|[ b,c ]|, |[ b,d ]|))
by SPPOL_2:def 3;
then
A10: |[b,d]| in X by A9,XBOOLE_0:def 3;
then (proj1|X). |[b,d]| = |[b,d]|`1 by PSCOMP_1:22
.= b by EUCLID:52;
hence thesis by A3,A8,A10,FUNCT_2:35;
end;
thus E-bound X = upper_bound (proj1|X) by PSCOMP_1:def 9
.= upper_bound Z by PSCOMP_1:def 2
.= b by A4,A7,SEQ_4:46;
end;
theorem Th39:
for a,b,c,d being Real st a<=b & c <=d
holds S-bound rectangle(a,b,c,d) = c
proof
let a,b,c,d be Real;
assume that
A1: a<=b and
A2: c <=d;
set X = rectangle(a,b,c,d);
reconsider Z = (proj2|X).:the carrier of ((TOP-REAL 2)|X)
as Subset of REAL;
A3: X = the carrier of ((TOP-REAL 2)|X) by PRE_TOPC:8;
A4: for p be Real st p in Z holds p >= c
proof
let p be Real;
assume p in Z;
then consider p0 being object such that
A5: p0 in the carrier of (TOP-REAL 2)|X and
p0 in the carrier of (TOP-REAL 2)|X and
A6: p = (proj2|X).p0 by FUNCT_2:64;
reconsider p0 as Point of TOP-REAL 2 by A3,A5;
X= {q : q`1 = a & q`2 <= d & q`2 >= c or q`1 <= b & q`1 >= a & q`2 = d or
q`1 <= b & q`1 >= a & q`2 = c or q`1 = b & q`2 <= d & q`2 >= c}
by A1,A2,SPPOL_2:54;
then ex q being Point of TOP-REAL 2 st p0 = q &
(q`1 = a & q`2 <= d & q`2 >= c or q`1 <= b & q`1 >= a & q`2 = d or
q`1 <= b & q`1 >= a & q`2 = c or q`1 = b & q`2 <= d & q`2 >= c) by A3,A5;
hence thesis by A2,A3,A5,A6,PSCOMP_1:23;
end;
A7: for q being Real st
for p being Real st p in Z holds p >= q holds c >= q
proof
let q be Real such that
A8: for p being Real st p in Z holds p >= q;
|[b,c]| in LSeg(|[ b,c ]|, |[ b,d ]|) by RLTOPSP1:68;
then
A9: |[b,c]| in LSeg(|[ a,c ]|, |[ b,c ]|) \/ LSeg(|[ b,c ]|, |[ b,d ]| )
by XBOOLE_0:def 3;
X= (LSeg(|[ a,c ]|, |[ a,d ]|) \/ LSeg(|[ a,d ]|, |[ b,d ]|))
\/ (LSeg(|[ a,c ]|, |[ b,c ]|) \/ LSeg(|[ b,c ]|, |[ b,d ]|))
by SPPOL_2:def 3;
then
A10: |[b,c]| in X by A9,XBOOLE_0:def 3;
then (proj2|X). |[b,c]| = |[b,c]|`2 by PSCOMP_1:23
.= c by EUCLID:52;
hence thesis by A3,A8,A10,FUNCT_2:35;
end;
thus S-bound X = lower_bound (proj2|X) by PSCOMP_1:def 10
.= lower_bound Z by PSCOMP_1:def 1
.= c by A4,A7,SEQ_4:44;
end;
theorem Th40:
for a,b,c,d being Real st a<=b & c <=d holds
NW-corner rectangle(a,b,c,d) = |[a,d]|
proof
let a,b,c,d be Real;
assume that
A1: a<=b and
A2: c <=d;
set K=rectangle(a,b,c,d);
A3: NW-corner K= |[W-bound K, N-bound K]| by PSCOMP_1:def 12;
W-bound K=a by A1,A2,Th36;
hence thesis by A1,A2,A3,Th37;
end;
theorem Th41:
for a,b,c,d being Real st a<=b & c <=d holds
NE-corner rectangle(a,b,c,d) = |[b,d]|
proof
let a,b,c,d be Real;
set K=rectangle(a,b,c,d);
assume that
A1: a<=b and
A2: c <=d;
A3: NE-corner K= |[E-bound K, N-bound K]| by PSCOMP_1:def 13;
E-bound K=b by A1,A2,Th38;
hence thesis by A1,A2,A3,Th37;
end;
theorem
for a,b,c,d being Real st a<=b & c <=d
holds SW-corner rectangle(a,b,c,d) = |[a,c]|
proof
let a,b,c,d be Real;
set K=rectangle(a,b,c,d);
assume that
A1: a<=b and
A2: c <=d;
A3: SW-corner K= |[W-bound K, S-bound K]| by PSCOMP_1:def 11;
W-bound K=a by A1,A2,Th36;
hence thesis by A1,A2,A3,Th39;
end;
theorem
for a,b,c,d being Real st a<=b & c <=d
holds SE-corner rectangle(a,b,c,d) = |[b,c]|
proof
let a,b,c,d be Real;
set K=rectangle(a,b,c,d);
assume that
A1: a<=b and
A2: c <=d;
A3: SE-corner K= |[E-bound K, S-bound K]| by PSCOMP_1:def 14;
E-bound K=b by A1,A2,Th38;
hence thesis by A1,A2,A3,Th39;
end;
theorem Th44:
for a,b,c,d being Real st a<=b & c <=d
holds W-most rectangle(a,b,c,d) = LSeg(|[a,c]|,|[a,d]|)
proof
let a,b,c,d be Real;
set K = rectangle(a,b,c,d);
assume that
A1: a<=b and
A2: c <=d;
K= LSeg(|[ a,c ]|, |[ a,d ]|) \/ LSeg(|[ a,d ]|, |[ b,d ]|)
\/ (LSeg(|[ a,c ]|, |[ b,c ]|) \/ LSeg(|[ b,c ]|, |[ b,d ]|))
by SPPOL_2:def 3;
then
A3: LSeg(|[ a,c ]|, |[ a,d ]|) \/ LSeg(|[ a,d ]|, |[ b,d ]|) c= K
by XBOOLE_1:7;
A4: LSeg(|[a,c]|,|[a,d]|) c=
LSeg(|[ a,c ]|, |[ a,d ]|) \/ LSeg(|[ a,d ]|, |[ b,d ]|) by XBOOLE_1:7;
A5: SW-corner K= |[W-bound K, S-bound K]| by PSCOMP_1:def 11;
A6: NW-corner K = |[a,d]| by A1,A2,Th40;
A7: W-bound K=a by A1,A2,Th36;
A8: S-bound K= c by A1,A2,Th39;
thus W-most K = LSeg(SW-corner K, NW-corner K)/\K by PSCOMP_1:def 15
.= LSeg(|[a,c]|,|[a,d]|) by A3,A4,A5,A6,A7,A8,XBOOLE_1:1,28;
end;
theorem Th45:
for a,b,c,d being Real st a<=b & c <=d
holds E-most rectangle(a,b,c,d) = LSeg(|[b,c]|,|[b,d]|)
proof
let a,b,c,d be Real;
set K = rectangle(a,b,c,d);
assume that
A1: a<=b and
A2: c <=d;
K= LSeg(|[ a,c ]|, |[ a,d ]|) \/ LSeg(|[ a,d ]|, |[ b,d ]|)
\/ (LSeg(|[ a,c ]|, |[ b,c ]|) \/ LSeg(|[ b,c ]|, |[ b,d ]|))
by SPPOL_2:def 3;
then
A3: LSeg(|[ a,c ]|, |[ b,c ]|) \/ LSeg(|[ b,c ]|, |[ b,d ]|) c= K
by XBOOLE_1:7;
A4: LSeg(|[b,c]|,|[b,d]|) c=
LSeg(|[ a,c ]|, |[ b,c ]|) \/ LSeg(|[ b,c ]|, |[ b,d ]|) by XBOOLE_1:7;
A5: SE-corner K= |[E-bound K, S-bound K]| by PSCOMP_1:def 14;
A6: NE-corner K = |[b,d]| by A1,A2,Th41;
A7: E-bound K=b by A1,A2,Th38;
A8: S-bound K= c by A1,A2,Th39;
thus E-most K = LSeg(SE-corner K, NE-corner K)/\K by PSCOMP_1:def 17
.= LSeg(|[b,c]|,|[b,d]|) by A3,A4,A5,A6,A7,A8,XBOOLE_1:1,28;
end;
theorem Th46:
for a,b,c,d being Real st a<=b & c <=d
holds W-min rectangle(a,b,c,d)=|[a,c]| & E-max rectangle(a,b,c,d)=|[b,d]|
proof
let a,b,c,d be Real;
set K = rectangle(a,b,c,d);
assume that
A1: a<=b and
A2: c <=d;
A3: lower_bound (proj2|LSeg(|[a,c]|,|[a,d]|)) = c
proof
set X = LSeg(|[a,c]|,|[a,d]|);
reconsider Z = (proj2|X).:the carrier of ((TOP-REAL 2)|X)
as Subset of REAL;
A4: X = the carrier of ((TOP-REAL 2)|X) by PRE_TOPC:8;
A5: for p be Real st p in Z holds p >= c
proof
let p be Real;
assume p in Z;
then consider p0 being object such that
A6: p0 in the carrier of (TOP-REAL 2)|X and
p0 in the carrier of (TOP-REAL 2)|X and
A7: p = (proj2|X).p0 by FUNCT_2:64;
reconsider p0 as Point of TOP-REAL 2 by A4,A6;
A8: |[a,c]|`2 = c by EUCLID:52;
|[a,d]|`2 = d by EUCLID:52;
then p0`2 >= c by A2,A4,A6,A8,TOPREAL1:4;
hence thesis by A4,A6,A7,PSCOMP_1:23;
end;
A9: for q being Real st
for p being Real st p in Z holds p >= q holds c >= q
proof
let q be Real such that
A10: for p being Real st p in Z holds p >= q;
A11: |[a,c]| in X by RLTOPSP1:68;
(proj2|X). |[a,c]| = |[a,c]|`2 by PSCOMP_1:23,RLTOPSP1:68
.= c by EUCLID:52;
hence thesis by A4,A10,A11,FUNCT_2:35;
end;
thus lower_bound (proj2|X) = lower_bound Z by PSCOMP_1:def 1
.= c by A5,A9,SEQ_4:44;
end;
A12: W-most K = LSeg(|[a,c]|,|[a,d]|) by A1,A2,Th44;
A13: W-bound K = a by A1,A2,Th36;
A14: upper_bound (proj2|LSeg(|[b,c]|,|[b,d]|)) = d
proof
set X = LSeg(|[b,c]|,|[b,d]|);
reconsider Z = (proj2|X).:the carrier of ((TOP-REAL 2)|X)
as Subset of REAL;
A15: X = the carrier of ((TOP-REAL 2)|X) by PRE_TOPC:8;
A16: for p be Real st p in Z holds p <= d
proof
let p be Real;
assume p in Z;
then consider p0 being object such that
A17: p0 in the carrier of (TOP-REAL 2)|X and
p0 in the carrier of (TOP-REAL 2)|X and
A18: p = (proj2|X).p0 by FUNCT_2:64;
reconsider p0 as Point of TOP-REAL 2 by A15,A17;
A19: |[b,c]|`2 = c by EUCLID:52;
|[b,d]|`2 = d by EUCLID:52;
then p0`2 <= d by A2,A15,A17,A19,TOPREAL1:4;
hence thesis by A15,A17,A18,PSCOMP_1:23;
end;
A20: for q being Real st
for p being Real st p in Z holds p <= q holds d <= q
proof
let q be Real such that
A21: for p being Real st p in Z holds p <= q;
A22: |[b,d]| in X by RLTOPSP1:68;
(proj2|X). |[b,d]| = |[b,d]|`2 by PSCOMP_1:23,RLTOPSP1:68
.= d by EUCLID:52;
hence thesis by A15,A21,A22,FUNCT_2:35;
end;
thus upper_bound (proj2|X) = upper_bound Z by PSCOMP_1:def 2
.= d by A16,A20,SEQ_4:46;
end;
A23: E-most K = LSeg(|[b,c]|,|[b,d]|) by A1,A2,Th45;
E-bound K = b by A1,A2,Th38;
hence thesis by A3,A12,A13,A14,A23,PSCOMP_1:def 19,def 23;
end;
theorem Th47:
for a,b,c,d being Real st a

** |[a,d]| by A2,EUCLID:52;
set p1= |[a,c]|,p2= |[a,d]|,q1=|[b,d]|;
A6: LSeg(p1,p2) /\ LSeg(p2,q1) ={p2} by A1,A2,Th34;
(|[a,c]|)`1=a by EUCLID:52;
then
A7: |[a,c]| <> |[b,c]| by A1,EUCLID:52;
set q2=|[b,c]|;
LSeg(q1,q2) /\ LSeg(q2,p1) ={q2} by A1,A2,Th32;
hence thesis by A3,A4,A5,A6,A7,TOPREAL1:12;
end;
theorem Th48:
for a,b,c,d being Real, f1,f2 being FinSequence of TOP-REAL 2,
p0,p1,p01,p10 being Point of TOP-REAL 2 st a < b & c < d &
p0=|[a,c]| & p1=|[b,d]| & p01=|[a,d]| & p10=|[b,c]| & f1=<*p0,p01,p1*>
& f2=<*p0,p10,p1*> holds f1 is being_S-Seq &
L~f1 = LSeg(p0,p01) \/ LSeg(p01,p1) &
f2 is being_S-Seq & L~f2 = LSeg(p0,p10) \/ LSeg(p10,p1) &
rectangle(a,b,c,d) = L~f1 \/ L~f2 & L~f1 /\ L~f2 = {p0,p1} & f1/.1 = p0 &
f1/.len f1=p1 & f2/.1 = p0 & f2/.len f2 = p1
proof
let a,b,c,d be Real, f1,f2 be FinSequence of TOP-REAL 2,
p0,p1,p01,p10 be Point of TOP-REAL 2;
assume that
A1: a < b and
A2: c < d and
A3: p0=|[a,c]| and
A4: p1=|[b,d]| and
A5: p01=|[a,d]| and
A6: p10=|[b,c]| and
A7: f1=<*p0,p01,p1*> and
A8: f2=<*p0,p10,p1*>;
set P = rectangle(a,b,c,d);
set L1 = { p : p`1 = a & p`2 <= d & p`2 >= c};
set L2 = { p : p`1 <= b & p`1 >= a & p`2 = d};
set L3 = { p : p`1 <= b & p`1 >= a & p`2 = c};
set L4 = { p : p`1 = b & p`2 <= d & p`2 >= c};
A9: p1`1 = b by A4,EUCLID:52;
A10: p1`2 = d by A4,EUCLID:52;
A11: p10`1 = b by A6,EUCLID:52;
A12: p10`2 = c by A6,EUCLID:52;
A13: p0`1 = a by A3,EUCLID:52;
A14: p0`2 = c by A3,EUCLID:52;
A15: len f1 = 1 + 2 by A7,FINSEQ_1:45;
A16: f1/.1 = p0 by A7,FINSEQ_4:18;
A17: f1/.2 = p01 by A7,FINSEQ_4:18;
A18: f1/.3 = p1 by A7,FINSEQ_4:18;
thus f1 is being_S-Seq
proof
A19: p0 <> p01 by A2,A5,A14,EUCLID:52;
p01 <> p1 by A1,A5,A9,EUCLID:52;
hence f1 is one-to-one by A1,A7,A9,A13,A19,FINSEQ_3:95;
thus len f1 >= 2 by A15;
thus f1 is unfolded
proof
let i be Nat;
assume that
A20: 1 <= i and
A21: i + 2 <= len f1;
i <= 1 by A15,A21,XREAL_1:6;
then
A22: i = 1 by A20,XXREAL_0:1;
reconsider n2=1+1 as Nat;
n2 in Seg len f1 by A15,FINSEQ_1:1;
then
A23: LSeg(f1,1) = LSeg(p0,p01) by A15,A16,A17,TOPREAL1:def 3;
A24: LSeg(f1,n2) = LSeg(p01,p1) by A15,A17,A18,TOPREAL1:def 3;
for x being object holds x in LSeg(p0,p01) /\ LSeg(p01,p1) iff x = p01
proof
let x be object;
thus x in LSeg(p0,p01) /\ LSeg(p01,p1) implies x = p01
proof
assume
A25: x in LSeg(p0,p01) /\ LSeg(p01,p1);
then
A26: x in LSeg(p0,p01) by XBOOLE_0:def 4;
A27: x in LSeg(p01,p1) by A25,XBOOLE_0:def 4;
A28: x in {p : p`1 = a & p`2 <= d & p`2 >= c} by A2,A3,A5,A26,Th30;
A29: x in {p2 : p2`1 <= b & p2`1 >= a & p2`2 = d} by A1,A4,A5,A27,Th30;
A30: ex p st p = x & p`1 = a & p`2 <= d & p`2 >= c by A28;
ex p2 st p2=x & p2`1<=b & p2`1>=a & p2`2=d by A29;
hence thesis by A5,A30,EUCLID:53;
end;
assume
A31: x = p01;
then
A32: x in LSeg(p0,p01) by RLTOPSP1:68;
x in LSeg(p01,p1) by A31,RLTOPSP1:68;
hence thesis by A32,XBOOLE_0:def 4;
end;
hence thesis by A17,A22,A23,A24,TARSKI:def 1;
end;
thus f1 is s.n.c.
proof
let i,j be Nat such that
A33: i+1 < j;
now per cases;
suppose 1 <= i;
then
A34: 1+1 <= i+1 by XREAL_1:6;
now per cases;
case 1 <= j & j+1 <= len f1;
then j <= 2 by A15,XREAL_1:6;
hence contradiction by A33,A34,XXREAL_0:2;
end;
case not (1 <= j & j+1 <= len f1);
then LSeg(f1,j) = {} by TOPREAL1:def 3;
hence LSeg(f1,i) /\ LSeg(f1,j) = {};
end;
end;
hence LSeg(f1,i) /\ LSeg(f1,j) = {};
end;
suppose not (1 <= i & i+1 <= len f1);
then LSeg(f1,i) = {} by TOPREAL1:def 3;
hence LSeg(f1,i) /\ LSeg(f1,j) = {};
end;
end;
hence LSeg(f1,i) /\ LSeg(f1,j) = {};
end;
let i be Nat;
assume that
A35: 1 <= i and
A36: i + 1 <= len f1;
A37: i <= 1 + 1 by A15,A36,XREAL_1:6;
now per cases by A35,A37,NAT_1:9;
suppose
A38: i = 1;
then (f1/.i)`1 = p0`1 by A7,FINSEQ_4:18
.= a by A3,EUCLID:52
.= (f1/.(i+1))`1 by A5,A17,A38,EUCLID:52;
hence thesis;
end;
suppose
A39: i = 2;
then (f1/.i)`2 = p01`2 by A7,FINSEQ_4:18
.= d by A5,EUCLID:52
.= (f1/.(i+1))`2 by A4,A18,A39,EUCLID:52;
hence thesis;
end;
end;
hence thesis;
end;
A40: 1+1 in Seg len f1 by A15,FINSEQ_1:1;
A41: 1+1 <= len f1 by A15;
LSeg(p0,p01) = LSeg(f1,1) by A15,A16,A17,A40,TOPREAL1:def 3;
then
A42: LSeg(p0,p01) in {LSeg(f1,i): 1 <= i & i+1 <= len f1} by A41;
LSeg(p01,p1) = LSeg(f1,2) by A15,A17,A18,TOPREAL1:def 3;
then LSeg(p01,p1) in {LSeg(f1,i): 1 <= i & i+1 <= len f1} by A15;
then
A43: {LSeg(p0,p01),LSeg(p01,p1)} c= {LSeg(f1,i):1<=i & i+1<=len f1}
by A42,ZFMISC_1:32;
{LSeg(f1,i): 1 <= i & i+1 <= len f1} c= {LSeg(p0,p01),LSeg(p01,p1)}
proof
let a be object;
assume a in {LSeg(f1,i): 1 <= i & i+1 <= len f1};
then consider i such that
A44: a = LSeg(f1,i) and
A45: 1<=i and
A46: i+1<=len f1;
i+1 <= 2 + 1 by A7,A46,FINSEQ_1:45;
then i <= 1 + 1 by XREAL_1:6;
then i = 1 or i = 2 by A45,NAT_1:9;
then a = LSeg(p0,p01) or a = LSeg(p01,p1) by A16,A17,A18,A44,A46,
TOPREAL1:def 3;
hence thesis by TARSKI:def 2;
end;
then L~f1 = union {LSeg(p0,p01),LSeg(p01,p1)} by A43,XBOOLE_0:def 10;
hence
A47: L~f1 = (LSeg(p0,p01) \/ LSeg(p01,p1)) by ZFMISC_1:75;
then
A48: L~f1=L1 \/ LSeg(p01,p1) by A2,A3,A5,Th30
.=L1 \/ L2 by A1,A4,A5,Th30;
A49: len f2 = 1 + 2 by A8,FINSEQ_1:45;
A50: f2/.1 = p0 by A8,FINSEQ_4:18;
A51: f2/.2 = p10 by A8,FINSEQ_4:18;
A52: f2/.3 = p1 by A8,FINSEQ_4:18;
thus f2 is being_S-Seq
proof
thus f2 is one-to-one by A1,A2,A8,A9,A10,A11,A12,A13,FINSEQ_3:95;
thus len f2 >= 2 by A49;
thus f2 is unfolded
proof
let i be Nat;
assume that
A53: 1 <= i and
A54: i + 2 <= len f2;
i <= 1 by A49,A54,XREAL_1:6;
then
A55: i = 1 by A53,XXREAL_0:1;
1+1 in Seg len f2 by A49,FINSEQ_1:1;
then
A56: LSeg(f2,1) = LSeg(p0,p10) by A49,A50,A51,TOPREAL1:def 3;
A57: LSeg(f2,1+1) = LSeg(p10,p1) by A49,A51,A52,TOPREAL1:def 3;
for x being object holds x in LSeg(p0,p10) /\ LSeg(p10,p1) iff x = p10
proof
let x be object;
thus x in LSeg(p0,p10) /\ LSeg(p10,p1) implies x = p10
proof
assume
A58: x in LSeg(p0,p10) /\ LSeg(p10,p1);
then
A59: x in LSeg(p0,p10) by XBOOLE_0:def 4;
A60: x in LSeg(p10,p1) by A58,XBOOLE_0:def 4;
A61: x in { p : p`1 <= b & p`1 >= a & p`2 = c} by A1,A3,A6,A59,Th30;
A62: x in { p2 : p2`1 = b & p2`2 <= d & p2`2 >= c} by A2,A4,A6,A60,Th30;
A63: ex p st p = x & p`1 <= b & p`1 >= a & p`2 = c by A61;
ex p2 st p2=x & p2`1=b & p2`2<=d & p2`2>=c by A62;
hence thesis by A6,A63,EUCLID:53;
end;
assume
A64: x = p10;
then
A65: x in LSeg(p0,p10) by RLTOPSP1:68;
x in LSeg(p10,p1) by A64,RLTOPSP1:68;
hence thesis by A65,XBOOLE_0:def 4;
end;
hence thesis by A51,A55,A56,A57,TARSKI:def 1;
end;
thus f2 is s.n.c.
proof
let i,j be Nat such that
A66: i+1 < j;
now per cases;
suppose 1 <= i;
then
A67: 1+1 <= i+1 by XREAL_1:6;
now per cases;
case 1 <= j & j+1 <= len f2;
then j <= 2 by A49,XREAL_1:6;
hence contradiction by A66,A67,XXREAL_0:2;
end;
case not (1 <= j & j+1 <= len f2);
then LSeg(f2,j) = {} by TOPREAL1:def 3;
hence LSeg(f2,i) /\ LSeg(f2,j) = {};
end;
end;
hence LSeg(f2,i) /\ LSeg(f2,j) = {};
end;
suppose not (1 <= i & i+1 <= len f2);
then LSeg(f2,i) = {} by TOPREAL1:def 3;
hence LSeg(f2,i) /\ LSeg(f2,j) = {};
end;
end;
hence LSeg(f2,i) /\ LSeg(f2,j) = {};
end;
let i be Nat;
assume that
A68: 1 <= i and
A69: i + 1 <= len f2;
A70: i <= 1 + 1 by A49,A69,XREAL_1:6;
per cases by A68,A70,NAT_1:9;
suppose
A71: i = 1;
then (f2/.i)`2 = p0`2 by A8,FINSEQ_4:18
.= c by A3,EUCLID:52
.= (f2/.(i+1))`2 by A6,A51,A71,EUCLID:52;
hence thesis;
end;
suppose
A72: i = 2;
then (f2/.i)`1 = p10`1 by A8,FINSEQ_4:18
.= b by A6,EUCLID:52
.= (f2/.(i+1))`1 by A4,A52,A72,EUCLID:52;
hence thesis;
end;
end;
A73: 1+1 in Seg len f2 by A49,FINSEQ_1:1;
A74: 1+1 <= len f2 by A49;
LSeg(p0,p10) = LSeg(f2,1) by A49,A50,A51,A73,TOPREAL1:def 3;
then
A75: LSeg(p0,p10) in {LSeg(f2,i): 1 <= i & i+1 <= len f2} by A74;
LSeg(p10,p1) = LSeg(f2,2) by A49,A51,A52,TOPREAL1:def 3;
then LSeg(p10,p1) in {LSeg(f2,i): 1 <= i & i+1 <= len f2} by A49;
then
A76: {LSeg(p0,p10),LSeg(p10,p1)} c= {LSeg(f2,i):1<=i & i+1<=len f2}
by A75,ZFMISC_1:32;
{LSeg(f2,i): 1 <= i & i+1 <= len f2} c= {LSeg(p0,p10),LSeg(p10,p1)}
proof
let ax be object;
assume ax in {LSeg(f2,i): 1 <= i & i+1 <= len f2};
then consider i such that
A77: ax = LSeg(f2,i) and
A78: 1<=i and
A79: i+1<=len f2;
i+1 <= 2 + 1 by A8,A79,FINSEQ_1:45;
then i <= 1 + 1 by XREAL_1:6;
then i = 1 or i = 2 by A78,NAT_1:9;
then ax = LSeg(p0,p10) or ax = LSeg(p10,p1) by A50,A51,A52,A77,A79,
TOPREAL1:def 3;
hence thesis by TARSKI:def 2;
end;
then
A80: L~f2 = union {LSeg(p0,p10),LSeg(p10,p1)} by A76,XBOOLE_0:def 10;
hence L~f2 = LSeg(p0,p10) \/ LSeg(p10,p1) by ZFMISC_1:75;
L~f2 = (LSeg(p0,p10) \/ LSeg(p10,p1)) by A80,ZFMISC_1:75;
then
A81: L~f2=L3 \/ LSeg(p10,p1) by A1,A3,A6,Th30
.=L3 \/ L4 by A2,A4,A6,Th30;
P = LSeg(p0,p01) \/ LSeg(p01,p1) \/ (LSeg(p0,p10) \/ LSeg(p10,p1))
by A3,A4,A5,A6,SPPOL_2:def 3;
hence P = L~f1 \/ L~f2 by A47,A80,ZFMISC_1:75;
now
assume L2 meets L3;
then consider x being object such that
A82: x in L2 and
A83: x in L3 by XBOOLE_0:3;
A84: ex p st p = x & p`1 <= b & p`1 >= a & p`2 = d by A82;
ex p2 st p2 = x & p2`1 <= b & p2`1 >= a & p2`2 = c by A83;
hence contradiction by A2,A84;
end;
then
A85: L2 /\ L3 = {};
A86: LSeg(|[ a,c ]|, |[ a,d ]|) = { p3 : p3`1 = a & p3`2 <= d & p3`2 >= c}
by A2,Th30;
A87: LSeg(|[ a,d ]|, |[ b,d ]|) = { p2 : p2`1 <= b & p2`1 >= a & p2`2 = d}
by A1,Th30;
A88: LSeg(|[ a,c ]|, |[ b,c ]|) = { q1 : q1`1 <= b & q1`1 >= a & q1`2 = c}
by A1,Th30;
A89: LSeg(|[ b,c ]|, |[ b,d ]|) = { q2 : q2`1 = b & q2`2 <= d & q2`2 >= c}
by A2,Th30;
A90: LSeg(|[a,c]|,|[a,d]|) /\ LSeg(|[a,c]|,|[b,c]|) = {|[a,c]|} by A1,A2,Th31;
A91: LSeg(|[a,d]|,|[b,d]|) /\ LSeg(|[b,c]|,|[b,d]|) = {|[b,d]|} by A1,A2,Th33;
now
assume L1 meets L4;
then consider x being object such that
A92: x in L1 and
A93: x in L4 by XBOOLE_0:3;
A94: ex p st p = x & p`1 = a & p`2 <= d & p`2 >= c by A92;
ex p2 st p2 = x & p2`1 = b & p2`2 <= d & p2`2 >= c by A93;
hence contradiction by A1,A94;
end;
then
A95: L1 /\ L4 = {};
thus L~f1 /\ L~f2
= (L1 \/ L2) /\ L3 \/ (L1 \/ L2) /\ L4 by A48,A81,XBOOLE_1:23
.= L1 /\ L3 \/ L2 /\ L3 \/ (L1 \/ L2) /\ L4 by XBOOLE_1:23
.= L1 /\ L3 \/ (L1 /\ L4 \/ L2 /\ L4) by A85,XBOOLE_1:23
.= {p0, p1} by A3,A4,A86,A87,A88,A89,A90,A91,A95,ENUMSET1:1;
thus thesis by A7,A8,A15,A49,FINSEQ_4:18;
end;
theorem Th49:
for P1,P2 being Subset of TOP-REAL 2, a,b,c,d being Real,
f1,f2 being FinSequence of TOP-REAL 2,p1,p2 being Point of TOP-REAL 2 st
a < b & c < d & p1=|[a,c]| & p2=|[b,d]| & f1=<*|[a,c]|,|[a,d]|,|[b,d]|*>
& f2=<*|[a,c]|,|[b,c]|,|[b,d]|*> & P1=L~f1 & P2=L~f2
holds P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2
& P1 is non empty & P2 is non empty &
rectangle(a,b,c,d) = P1 \/ P2 & P1 /\ P2 = {p1,p2}
proof
let P1,P2 be Subset of TOP-REAL 2, a,b,c,d be Real,
f1,f2 be FinSequence of TOP-REAL 2,p1,p2 be Point of TOP-REAL 2;
assume that
A1: a < b and
A2: c < d and
A3: p1=|[a,c]| and
A4: p2=|[b,d]| and
A5: f1=<*|[a,c]|,|[a,d]|,|[b,d]|*> and
A6: f2=<*|[a,c]|,|[b,c]|,|[b,d]|*> and
A7: P1=L~f1 and
A8: P2=L~f2;
(|[a,c]|)`2=c by EUCLID:52;
then
A9: |[a,c]|<>|[a,d]| or |[a,d]|<>|[b,d]| by A2,EUCLID:52;
A10: P1=LSeg(|[a,c]|,|[a,d]|) \/ LSeg(|[a,d]|,|[b,d]|) by A1,A2,A5,A6,A7,Th48;
A11: LSeg(|[a,c]|,|[a,d]|) /\ LSeg(|[a,d]|,|[b,d]|)={|[a,d]|} by A1,A2,Th34;
(|[b,c]|)`2=c by EUCLID:52;
then
A12: |[a,c]|<>|[b,c]| or |[b,c]|<>|[b,d]| by A2,EUCLID:52;
A13: P2=LSeg(|[a,c]|,|[b,c]|) \/ LSeg(|[b,c]|,|[b,d]|) by A1,A2,A5,A6,A8,Th48;
LSeg(|[a,c]|,|[b,c]|) /\ LSeg(|[b,c]|,|[b,d]|)={|[b,c]|} by A1,A2,Th32;
hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A12,A13,Th48,TOPREAL1:12;
end;
theorem Th50:
for a,b,c,d being Real st a < b & c < d
holds rectangle(a,b,c,d) is being_simple_closed_curve
proof
let a,b,c,d be Real;
assume that
A1: a < b and
A2: c < d;
set P=rectangle(a,b,c,d);
set p1=|[a,c]|,p2=|[b,d]|;
reconsider f1=<*|[a,c]|,|[a,d]|,|[b,d]|*> as FinSequence of TOP-REAL 2;
reconsider f2=<*|[a,c]|,|[b,c]|,|[b,d]|*> as FinSequence of TOP-REAL 2;
set P1=L~f1,P2=L~f2;
A3: a < b & c < d &
P={p: p`1=a & c <=p`2 & p`2<=d or p`2=d & a<=p`1 & p`1<=b or
p`1=b & c <=p`2 & p`2<=d or p`2=c & a<=p`1 & p`1<=b} &
p1=|[a,c]| & p2=|[b,d]| & f1=<*|[a,c]|,|[a,d]|,|[b,d]|*>
& f2=<*|[a,c]|,|[b,c]|,|[b,d]|*> & P1=L~f1 & P2=L~f2
implies P1 is_an_arc_of p1,p2 & P2 is_an_arc_of p1,p2
& P1 is non empty & P2 is non empty &
P = P1 \/ P2 & P1 /\ P2 = {p1,p2} by Th49;
(|[a,c]|)`1=a by EUCLID:52;
then
A4: p1<>p2 by A1,EUCLID:52;
p1 in P1 /\ P2 by A1,A2,A3,Lm15,TARSKI:def 2;
then p1 in P1 by XBOOLE_0:def 4;
then
A5: p1 in P by A1,A2,A3,Lm15,XBOOLE_0:def 3;
p2 in P1 /\ P2 by A1,A2,A3,Lm15,TARSKI:def 2;
then p2 in P1 by XBOOLE_0:def 4;
then p2 in P by A1,A2,A3,Lm15,XBOOLE_0:def 3;
hence thesis by A1,A2,A3,A4,A5,Lm15,TOPREAL2:6;
end;
theorem Th51:
for a,b,c,d being Real st a ,
f2=<* |[a,c]|,|[b,c]|,|[b,d]| *> as FinSequence of TOP-REAL 2;
set p0=|[a,c]|,p01=|[a,d]|,p10=|[b,c]|,p1=|[b,d]|;
A8: a < b & c < d & p0=|[a,c]| & p1=|[b,d]| & p01=|[a,d]| & p10=|[b,c]|
& f1=<*p0,p01,p1*> & f2=<*p0,p10,p1*> implies f1 is being_S-Seq &
L~f1 = LSeg(p0,p01) \/ LSeg(p01,p1) & f2 is being_S-Seq &
L~f2 = LSeg(p0,p10) \/ LSeg(p10,p1) & K = L~f1 \/ L~f2 &
L~f1 /\ L~f2 = {p0,p1} & f1/.1 = p0 &
f1/.len f1=p1 & f2/.1 = p0 & f2/.len f2 = p1 by Th48;
A9: Vertical_Line((W-bound(P)+E-bound(P))/2)
= Vertical_Line((a+E-bound(P))/2) by A1,A2,Th36
.= Vertical_Line((a+b)/2) by A1,A2,Th38;
set Q=Vertical_Line((W-bound(P)+E-bound(P))/2);
reconsider a2=a,b2=b,c2=c,d2=d as Real;
A10: U /\ Vertical_Line((W-bound(P)+E-bound(P))/2) ={|[(a+b)/2,d]|}
proof
thus
U /\ Vertical_Line((W-bound(P)+E-bound(P))/2) c= {|[(a+b)/2,d]|}
proof
let x be object;
assume
A11: x in U /\ Vertical_Line((W-bound(P)+E-bound(P))/2);
then
A12: x in U by XBOOLE_0:def 4;
x in Vertical_Line((W-bound(P)+E-bound(P))/2) by A11,XBOOLE_0:def 4;
then x in {p where p is Point of TOP-REAL 2: p`1=(a+b)/2}
by A9,JORDAN6:def 6;
then consider p such that
A13: x=p and
A14: p`1=(a+b)/2;
now
assume p in LSeg(|[a,c]|,|[a,d]|);
then p`1=a by TOPREAL3:11;
hence contradiction by A1,A14;
end;
then p in LSeg(|[a2,d2]|,|[b2,d2]|) by A12,A13,XBOOLE_0:def 3;
then p`2=d by TOPREAL3:12;
then x=|[(a+b)/2,d]| by A13,A14,EUCLID:53;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {|[(a+b)/2,d]|};
then
A15: x= |[(a+b)/2,d]| by TARSKI:def 1;
(|[(a+b)/2,d]|)`1= (a+b)/2 by EUCLID:52;
then x in {p where p is Point of TOP-REAL 2: p`1=(a+b)/2} by A15;
then
A16: x in Vertical_Line((W-bound(P)+E-bound(P))/2) by A9,JORDAN6:def 6;
A17: (|[b,d]|)`1=b by EUCLID:52;
A18: (|[b,d]|)`2=d by EUCLID:52;
A19: (|[a,d]|)`1=a by EUCLID:52;
(|[a,d]|)`2=d by EUCLID:52;
then x in LSeg(|[b,d]|,|[a,d]|) by A1,A15,A17,A18,A19,TOPREAL3:13;
then x in U by XBOOLE_0:def 3;
hence thesis by A16,XBOOLE_0:def 4;
end;
then |[(a+b)/2,d]| in U /\ Q by TARSKI:def 1;
then U meets Q;
then First_Point(U,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2)) in {|[(a+b)/2,d]|}
by A6,A10,JORDAN5C:def 1;
then First_Point(U,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2)) = |[(a+b)/2,d]| by TARSKI:def 1;
then
A20: First_Point(U,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2=d by EUCLID:52;
A21: P3 /\ Vertical_Line((W-bound(P)+E-bound(P))/2) ={|[(a+b)/2,c]|}
proof
thus
P3 /\ Vertical_Line((W-bound(P)+E-bound(P))/2) c= {|[(a+b)/2,c]|}
proof
let x be object;
assume
A22: x in P3 /\ Vertical_Line((W-bound(P)+E-bound(P))/2);
then
A23: x in P3 by XBOOLE_0:def 4;
x in Vertical_Line((W-bound(P)+E-bound(P))/2) by A22,XBOOLE_0:def 4;
then x in {p where p is Point of TOP-REAL 2: p`1=(a+b)/2}
by A9,JORDAN6:def 6;
then consider p such that
A24: x=p and
A25: p`1=(a+b)/2;
now
assume p in LSeg(|[b,c]|,|[b,d]|);
then p`1= b by TOPREAL3:11;
hence contradiction by A1,A25;
end;
then p in LSeg(|[a2,c2]|,|[b2,c2]|) by A23,A24,XBOOLE_0:def 3;
then p`2= c by TOPREAL3:12;
then x=|[(a+b)/2,c]| by A24,A25,EUCLID:53;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {|[(a+b)/2,c]|};
then
A26: x= |[(a+b)/2,c]| by TARSKI:def 1;
(|[(a+b)/2,c]|)`1= (a+b)/2 by EUCLID:52;
then x in {p where p is Point of TOP-REAL 2: p`1=(a+b)/2} by A26;
then
A27: x in Vertical_Line((W-bound(P)+E-bound(P))/2) by A9,JORDAN6:def 6;
A28: (|[b,c]|)`1=b by EUCLID:52;
A29: (|[b,c]|)`2=c by EUCLID:52;
A30: (|[a,c]|)`1=a by EUCLID:52;
(|[a,c]|)`2=c by EUCLID:52;
then |[(b+a)/2,c]| in LSeg(|[a,c]|,|[b,c]|) by A1,A28,A29,A30,TOPREAL3:13;
then x in P3 by A26,XBOOLE_0:def 3;
hence thesis by A27,XBOOLE_0:def 4;
end;
then |[(a+b)/2,c]| in P3 /\ Q by TARSKI:def 1;
then P3 meets Q;
then Last_Point(P3,E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2)) in {|[(a+b)/2,c]|}
by A7,A21,JORDAN5C:def 2;
then Last_Point(P3,E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2)) = |[(a+b)/2,c]| by TARSKI:def 1;
then Last_Point(P3,E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2 = c by EUCLID:52;
hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,A20,JORDAN6:def 8;
end;
theorem Th52:
for a,b,c,d being Real st a,
f2=<* |[a,c]|,|[b,c]|,|[b,d]| *> as FinSequence of TOP-REAL 2;
set p0=|[a,c]|,p01=|[a,d]|,p10=|[b,c]|,p1=|[b,d]|;
A8: a < b & c < d & p0=|[a,c]| & p1=|[b,d]| & p01=|[a,d]| & p10=|[b,c]|
& f1=<*p0,p01,p1*> & f2=<*p0,p10,p1*> implies f1 is being_S-Seq &
L~f1 = LSeg(p0,p01) \/ LSeg(p01,p1) & f2 is being_S-Seq &
L~f2 = LSeg(p0,p10) \/ LSeg(p10,p1) & K = L~f1 \/ L~f2 &
L~f1 /\ L~f2 = {p0,p1} & f1/.1 = p0 &
f1/.len f1=p1 & f2/.1 = p0 & f2/.len f2 = p1 by Th48;
A9: Vertical_Line((W-bound(P)+E-bound(P))/2)
= Vertical_Line((a+E-bound(P))/2) by A1,A2,Th36
.= Vertical_Line((a+b)/2) by A1,A2,Th38;
set Q=Vertical_Line((W-bound(P)+E-bound(P))/2);
reconsider a2=a,b2=b,c2=c,d2=d as Real;
A10: U /\ Vertical_Line((W-bound(P)+E-bound(P))/2) ={|[(a+b)/2,d]|}
proof
thus
U /\ Vertical_Line((W-bound(P)+E-bound(P))/2) c= {|[(a+b)/2,d]|}
proof
let x be object;
assume
A11: x in U /\ Vertical_Line((W-bound(P)+E-bound(P))/2);
then
A12: x in U by XBOOLE_0:def 4;
x in Vertical_Line((W-bound(P)+E-bound(P))/2) by A11,XBOOLE_0:def 4;
then x in {p where p is Point of TOP-REAL 2: p`1=(a+b)/2}
by A9,JORDAN6:def 6;
then consider p such that
A13: x=p and
A14: p`1=(a+b)/2;
now
assume p in LSeg(|[a,c]|,|[a,d]|);
then p`1=a by TOPREAL3:11;
hence contradiction by A1,A14;
end;
then p in LSeg(|[a2,d2]|,|[b2,d2]|) by A12,A13,XBOOLE_0:def 3;
then p`2=d by TOPREAL3:12;
then x=|[(a+b)/2,d]| by A13,A14,EUCLID:53;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {|[(a+b)/2,d]|};
then
A15: x= |[(a+b)/2,d]| by TARSKI:def 1;
(|[(a+b)/2,d]|)`1= (a+b)/2 by EUCLID:52;
then x in {p where p is Point of TOP-REAL 2: p`1=(a+b)/2} by A15;
then
A16: x in Vertical_Line((W-bound(P)+E-bound(P))/2) by A9,JORDAN6:def 6;
A17: (|[b,d]|)`1=b by EUCLID:52;
A18: (|[b,d]|)`2=d by EUCLID:52;
A19: (|[a,d]|)`1=a by EUCLID:52;
(|[a,d]|)`2=d by EUCLID:52;
then x in LSeg(|[b,d]|,|[a,d]|) by A1,A15,A17,A18,A19,TOPREAL3:13;
then x in U by XBOOLE_0:def 3;
hence thesis by A16,XBOOLE_0:def 4;
end;
then |[(a+b)/2,d]| in U /\ Q by TARSKI:def 1;
then U meets Q;
then First_Point(U,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2)) in {|[(a+b)/2,d]|}
by A6,A10,JORDAN5C:def 1;
then First_Point(U,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2)) = |[(a+b)/2,d]| by TARSKI:def 1;
then
A20: First_Point(U,W-min(P),E-max(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2=d by EUCLID:52;
A21: P3 /\ Vertical_Line((W-bound(P)+E-bound(P))/2) ={|[(a+b)/2,c]|}
proof
thus
P3 /\ Vertical_Line((W-bound(P)+E-bound(P))/2) c= {|[(a+b)/2,c]|}
proof
let x be object;
assume
A22: x in P3 /\ Vertical_Line((W-bound(P)+E-bound(P))/2);
then
A23: x in P3 by XBOOLE_0:def 4;
x in Vertical_Line((W-bound(P)+E-bound(P))/2) by A22,XBOOLE_0:def 4;
then x in {p where p is Point of TOP-REAL 2: p`1=(a+b)/2}
by A9,JORDAN6:def 6;
then consider p such that
A24: x=p and
A25: p`1=(a+b)/2;
now
assume p in LSeg(|[b,c]|,|[b,d]|);
then p`1= b by TOPREAL3:11;
hence contradiction by A1,A25;
end;
then p in LSeg(|[a2,c2]|,|[b2,c2]|) by A23,A24,XBOOLE_0:def 3;
then p`2= c by TOPREAL3:12;
then x=|[(a+b)/2,c]| by A24,A25,EUCLID:53;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {|[(a+b)/2,c]|};
then
A26: x= |[(a+b)/2,c]| by TARSKI:def 1;
(|[(a+b)/2,c]|)`1= (a+b)/2 by EUCLID:52;
then x in {p where p is Point of TOP-REAL 2: p`1=(a+b)/2} by A26;
then
A27: x in Vertical_Line((W-bound(P)+E-bound(P))/2) by A9,JORDAN6:def 6;
A28: (|[b,c]|)`1=b by EUCLID:52;
A29: (|[b,c]|)`2=c by EUCLID:52;
A30: (|[a,c]|)`1=a by EUCLID:52;
(|[a,c]|)`2=c by EUCLID:52;
then |[(a+b)/2,c]| in LSeg(|[a,c]|,|[b,c]|) by A1,A28,A29,A30,TOPREAL3:13;
then x in P3 by A26,XBOOLE_0:def 3;
hence thesis by A27,XBOOLE_0:def 4;
end;
then |[(a+b)/2,c]| in P3 /\ Q by TARSKI:def 1;
then P3 meets Q;
then Last_Point(P3,E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2)) in {|[(a+b)/2,c]|}
by A7,A21,JORDAN5C:def 2;
then Last_Point(P3,E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2)) = |[(a+b)/2,c]| by TARSKI:def 1;
then
A31: Last_Point(P3,E-max(P),W-min(P),
Vertical_Line((W-bound(P)+E-bound(P))/2))`2 = c by EUCLID:52;
A32: P3 is_an_arc_of E-max(P),W-min(P) by A1,A2,Th47;
A33: Upper_Arc(P) /\ P3={W-min(P),E-max(P)} by A1,A2,A4,A5,A8,Th51;
A34: Upper_Arc(P) \/ P3=P by A1,A2,A8,Th51;
First_Point(Upper_Arc(P),W-min(P),E-max(P), Vertical_Line((W-bound(P)+
E-bound(P))/2))`2> Last_Point(P3,E-max(P),W-min(P), Vertical_Line((W-bound(P)+
E-bound(P))/2))`2 by A1,A2,A20,A31,Th51;
hence thesis by A3,A32,A33,A34,JORDAN6:def 9;
end;
theorem Th53:
for a,b,c,d being Real st a=1/2*2 by A23,XREAL_1:64;
then
A25: 2*r-1>=0 by XREAL_1:48;
2*1>=2*r by A24,XREAL_1:64;
then
A26: 1+1-1>=2*r-1 by XREAL_1:9;
f2.x= (1-(2*r-1))*|[a,d]|+(2*r-1)*|[b,d]| by A14,A15,A16,A22;
then
A27: y
in { (1-lambda)*|[a,d]| + lambda*|[b,d]| where lambda is Real:
0 <= lambda & lambda <= 1 } by A17,A25,A26;
Upper_Arc(K)= LSeg(|[a,c]|,|[a,d]|) \/ LSeg(|[a,d]|,|[b,d]|)
by A1,A2,Th51;
then y in Upper_Arc(K) by A27,XBOOLE_0:def 3;
hence thesis by PRE_TOPC:8;
end;
end;
hence thesis;
end;
then reconsider f3=f2 as Function of I[01],(TOP-REAL 2)|(Upper_Arc(K))
by A14,BORSUK_1:40,FUNCT_2:2;
A28: 0 in [.0,1.] by XXREAL_1:1;
0 in [.0,1/2.] by XXREAL_1:1;
then
A29: f3.0= (1-2*0)*|[a,c]|+(2*0)*|[a,d]| by A15,A28
.= (1)*|[a,c]|+0.TOP-REAL 2 by RLVECT_1:10
.= |[a,c]|+0.TOP-REAL 2 by RLVECT_1:def 8
.= |[a,c]| by RLVECT_1:4
.= W-min(K) by A1,A2,Th46;
A30: 1 in [.0,1.] by XXREAL_1:1;
1 in [.1/2,1.] by XXREAL_1:1;
then
A31: f3.1= (1-(2*1-1))*|[a,d]|+(2*1-1)*|[b,d]| by A15,A30
.= (0)*|[a,d]|+|[b,d]| by RLVECT_1:def 8
.= (0.TOP-REAL 2) + |[b,d]| by RLVECT_1:10
.= |[b,d]| by RLVECT_1:4
.= E-max(K) by A1,A2,Th46;
A32: for r being Real st r in [.0,1/2.] holds
f3.r=(1-2*r)*|[a,c]|+(2*r)*|[a,d]|
proof
let r be Real;
assume
A33: r in [.0,1/2.];
then
A34: 0<=r by XXREAL_1:1;
r<=1/2 by A33,XXREAL_1:1;
then r<=1 by XXREAL_0:2;
then r in [.0,1.] by A34,XXREAL_1:1;
hence thesis by A15,A33;
end;
A35: for r being Real st r in [.1/2,1.] holds
f3.r=(1-(2*r-1))*|[a,d]|+(2*r-1)*|[b,d]|
proof
let r be Real;
assume
A36: r in [.1/2,1.];
then
A37: 1/2<=r by XXREAL_1:1;
r<=1 by A36,XXREAL_1:1;
then r in [.0,1.] by A37,XXREAL_1:1;
hence thesis by A15,A36;
end;
A38: for p being Point of TOP-REAL 2 st p in LSeg(|[a,c]|,|[a,d]|)
holds 0<=((p`2)-c)/(d-c)/2 & ((p`2)-c)/(d-c)/2<=1
& f3.(((p`2)-c)/(d-c)/2)=p
proof
let p be Point of TOP-REAL 2;
assume
A39: p in LSeg(|[a,c]|,|[a,d]|);
A40: (|[a,c]|)`2= c by EUCLID:52;
A41: (|[a,d]|)`2= d by EUCLID:52;
then
A42: c <=p`2 by A2,A39,A40,TOPREAL1:4;
A43: p`2<=d by A2,A39,A40,A41,TOPREAL1:4;
A44: d-c>0 by A2,XREAL_1:50;
A45: (p`2) -c >=0 by A42,XREAL_1:48;
A46: d-c>0 by A2,XREAL_1:50;
(p`2) -c <=d-c by A43,XREAL_1:9;
then ((p`2) -c)/(d-c) <=(d-c)/(d-c) by A46,XREAL_1:72;
then ((p`2) -c)/(d-c) <=1 by A46,XCMPLX_1:60;
then
A47: ((p`2) -c)/(d-c)/2 <=1/2 by XREAL_1:72;
set r=((p`2)-c)/(d-c)/2;
r in [.0,1/2.] by A44,A45,A47,XXREAL_1:1;
then f3.(((p`2)-c)/(d-c)/2)=(1-2*r)*|[a,c]|+(2*r)*|[a,d]| by A32
.=|[(1-2*r)*a,(1-2*r)*c]|+(2*r)*|[a,d]| by EUCLID:58
.=|[(1-2*r)*a,(1-2*r)*c]|+|[(2*r)*a,(2*r)*d]| by EUCLID:58
.=|[1*a-(2*r)*a+(2*r)*a,(1-2*r)*c+(2*r)*d]| by EUCLID:56
.=|[a,1*c+(((p`2)-c)/(d-c))*(d-c)]|
.=|[a,1*c+((p`2)-c)]| by A46,XCMPLX_1:87
.=|[p`1,p`2]| by A39,TOPREAL3:11
.= p by EUCLID:53;
hence thesis by A44,A45,A47,XXREAL_0:2;
end;
A48: for p being Point of TOP-REAL 2 st p in LSeg(|[a,d]|,|[b,d]|)
holds 0<=((p`1)-a)/(b-a)/2+1/2 & ((p`1)-a)/(b-a)/2+1/2<=1
& f3.(((p`1)-a)/(b-a)/2+1/2)=p
proof
let p be Point of TOP-REAL 2;
assume
A49: p in LSeg(|[a,d]|,|[b,d]|);
A50: (|[a,d]|)`1= a by EUCLID:52;
A51: (|[b,d]|)`1= b by EUCLID:52;
then
A52: a <=p`1 by A1,A49,A50,TOPREAL1:3;
A53: p`1<=b by A1,A49,A50,A51,TOPREAL1:3;
A54: b-a>0 by A1,XREAL_1:50;
A55: (p`1) -a >=0 by A52,XREAL_1:48;
then
A56: ((p`1) -a)/(b-a)/2+1/2 >=0+1/2 by A54,XREAL_1:7;
A57: b-a>0 by A1,XREAL_1:50;
(p`1) -a <=b-a by A53,XREAL_1:9;
then ((p`1) -a)/(b-a) <=(b-a)/(b-a) by A57,XREAL_1:72;
then ((p`1) -a)/(b-a) <=1 by A57,XCMPLX_1:60;
then ((p`1) -a)/(b-a)/2 <=1/2 by XREAL_1:72;
then
A58: ((p`1) -a)/(b-a)/2+1/2 <=1/2+1/2 by XREAL_1:7;
set r=((p`1)-a)/(b-a)/2+1/2;
r in [.1/2,1.] by A56,A58,XXREAL_1:1;
then f3.(((p`1)-a)/(b-a)/2+1/2)=(1-(2*r-1))*|[a,d]|+(2*r-1)*|[b,d]| by A35
.=|[(1-(2*r-1))*a,(1-(2*r-1))*d]|+((2*r-1))*|[b,d]| by EUCLID:58
.=|[(1-(2*r-1))*a,(1-(2*r-1))*d]|+|[((2*r-1))*b,((2*r-1))*d]|
by EUCLID:58
.=|[(1-(2*r-1))*a+((2*r-1))*b,1*d-(2*r-1)*d+((2*r-1))*d]| by EUCLID:56
.=|[1*a+(((p`1)-a)/(b-a))*(b-a),d]|
.=|[1*a+((p`1)-a),d]| by A57,XCMPLX_1:87
.=|[p`1,p`2]| by A49,TOPREAL3:12
.= p by EUCLID:53;
hence thesis by A54,A55,A58;
end;
reconsider B00=[.0,1.] as Subset of R^1 by TOPMETR:17;
reconsider B01=B00 as non empty Subset of R^1 by XXREAL_1:1;
I[01]=(R^1)|B01 by TOPMETR:19,20;
then consider h1 being Function of I[01],R^1 such that
A59: for p being Point of I[01] holds h1.p=p and
A60: h1 is continuous by Th6;
consider h2 being Function of I[01],R^1 such that
A61: for p being Point of I[01],r1 being Real st h1.p=r1 holds h2.p
=2*r1 and
A62: h2 is continuous by A60,JGRAPH_2:23;
consider h5 being Function of I[01],R^1 such that
A63: for p being Point of I[01],r1 being Real st h2.p=r1 holds h5.p
=1-r1 and
A64: h5 is continuous by A62,Th8;
consider h3 being Function of I[01],R^1 such that
A65: for p being Point of I[01],r1 being Real st h2.p=r1 holds h3.p
=r1-1 and
A66: h3 is continuous by A62,Th7;
consider h4 being Function of I[01],R^1 such that
A67: for p being Point of I[01],r1 being Real st h3.p=r1 holds h4.p
=1-r1 and
A68: h4 is continuous by A66,Th8;
consider g1 being Function of I[01],TOP-REAL 2 such that
A69: for r being Point of I[01] holds g1.r=(h5.r)*|[a,c]|+(h2.r)*|[a,d]| and
A70: g1 is continuous by A62,A64,Th13;
A71: for r being Point of I[01],s being Real st r=s holds
g1.r=(1-2*s)*|[a,c]|+(2*s)*|[a,d]|
proof
let r be Point of I[01],s be Real;
assume
A72: r=s;
g1.r=(h5.r)*|[a,c]|+(h2.r)*|[a,d]| by A69
.=(1-2*(h1.r))*|[a,c]|+(h2.r)*|[a,d]| by A61,A63
.=(1-2*(h1.r))*|[a,c]|+(2*(h1.r))*|[a,d]| by A61
.=(1-2*s)*|[a,c]|+(2*(h1.r))*|[a,d]| by A59,A72
.=(1-2*s)*|[a,c]|+(2*s)*|[a,d]| by A59,A72;
hence thesis;
end;
consider g2 being Function of I[01],TOP-REAL 2 such that
A73: for r being Point of I[01] holds g2.r=(h4.r)*|[a,d]|+(h3.r)*|[b,d]| and
A74: g2 is continuous by A66,A68,Th13;
A75: for r being Point of I[01],s being Real st r=s holds
g2.r=(1-(2*s-1))*|[a,d]|+(2*s-1)*|[b,d]|
proof
let r be Point of I[01],s be Real;
assume
A76: r=s;
g2.r=(h4.r)*|[a,d]|+(h3.r)*|[b,d]| by A73
.=(1-((h2.r)-1))*|[a,d]|+(h3.r)*|[b,d]| by A65,A67
.=(1-((h2.r)-1))*|[a,d]|+((h2.r)-1)*|[b,d]| by A65
.=(1-(2*(h1.r)-1))*|[a,d]|+((h2.r)-1)*|[b,d]| by A61
.=(1-(2*(h1.r)-1))*|[a,d]|+(2*(h1.r)-1)*|[b,d]| by A61
.=(1-(2*s-1))*|[a,d]|+(2*(h1.r)-1)*|[b,d]| by A59,A76
.=(1-(2*s-1))*|[a,d]|+(2*s-1)*|[b,d]| by A59,A76;
hence thesis;
end;
reconsider B11=[.0,1/2.] as non empty Subset of I[01]
by A3,BORSUK_1:40,XBOOLE_1:7,XXREAL_1:1;
A77: dom (g1|B11)=dom g1 /\ B11 by RELAT_1:61
.= (the carrier of I[01]) /\ B11 by FUNCT_2:def 1
.=B11 by XBOOLE_1:28
.=the carrier of (I[01]|B11) by PRE_TOPC:8;
rng (g1|B11) c= the carrier of TOP-REAL 2;
then reconsider g11=g1|B11 as Function
of I[01]|B11,TOP-REAL 2 by A77,FUNCT_2:2;
A78: TOP-REAL 2 is SubSpace of TOP-REAL 2 by TSEP_1:2;
then
A79: g11 is continuous by A70,BORSUK_4:44;
reconsider B22=[.1/2,1.] as non empty Subset of I[01] by A3,BORSUK_1:40
,XBOOLE_1:7,XXREAL_1:1;
A80: dom (g2|B22)=dom g2 /\ B22 by RELAT_1:61
.= (the carrier of I[01]) /\ B22 by FUNCT_2:def 1
.=B22 by XBOOLE_1:28
.=the carrier of (I[01]|B22) by PRE_TOPC:8;
rng (g2|B22) c= the carrier of TOP-REAL 2;
then reconsider g22=g2|B22 as Function
of I[01]|B22,TOP-REAL 2 by A80,FUNCT_2:2;
A81: g22 is continuous by A74,A78,BORSUK_4:44;
A82: B11=[#](I[01]|B11) by PRE_TOPC:def 5;
A83: B22=[#](I[01]|B22) by PRE_TOPC:def 5;
A84: B11 is closed by Th4;
A85: B22 is closed by Th4;
A86: [#](I[01]|B11) \/ [#](I[01]|B22)=[#]I[01]
by A82,A83,BORSUK_1:40,XXREAL_1:165;
for p being object st p in ([#](I[01]|B11)) /\ ([#](I[01]|B22))
holds g11.p = g22.p
proof
let p be object;
assume
A87: p in ([#](I[01]|B11)) /\ ([#](I[01]|B22));
then
A88: p in [#](I[01]|B11) by XBOOLE_0:def 4;
A89: p in [#](I[01]|B22) by A87;
A90: p in B11 by A88,PRE_TOPC:def 5;
A91: p in B22 by A89,PRE_TOPC:def 5;
reconsider rp=p as Real by A90;
A92: rp<=1/2 by A90,XXREAL_1:1;
rp>=1/2 by A91,XXREAL_1:1;
then rp=1/2 by A92,XXREAL_0:1;
then
A93: 2*rp=1;
thus g11.p=g1.p by A90,FUNCT_1:49
.= (1-1)*|[a,c]|+(1)*|[a,d]| by A71,A90,A93
.=0.TOP-REAL 2 +1*|[a,d]| by RLVECT_1:10
.=(1-0)*|[a,d]| +(1-1)*|[b,d]| by RLVECT_1:10
.=g2.p by A75,A90,A93
.=g22.p by A91,FUNCT_1:49;
end;
then consider h being Function of I[01],TOP-REAL 2 such that
A94: h=g11+*g22 and
A95: h is continuous by A79,A81,A82,A83,A84,A85,A86,JGRAPH_2:1;
A96: dom f3=dom h by Th5;
A97: dom f3=the carrier of I[01] by Th5;
for x being object st x in dom f2 holds f3.x=h.x
proof
let x be object;
assume
A98: x in dom f2;
then reconsider rx=x as Real by A97;
A99: 0<=rx by A96,A98,BORSUK_1:40,XXREAL_1:1;
A100: rx<=1 by A96,A98,BORSUK_1:40,XXREAL_1:1;
now per cases;
case
A101: rx<1/2;
then
A102: rx in [.0,1/2.] by A99,XXREAL_1:1;
not rx in dom g22 by A83,A101,XXREAL_1:1;
then h.rx=g11.rx by A94,FUNCT_4:11
.=g1.rx by A102,FUNCT_1:49
.=(1-(2*rx))*|[a,c]|+(2*rx)*|[a,d]| by A71,A96,A98
.=f3.rx by A32,A102;
hence thesis;
end;
case rx >=1/2;
then
A103: rx in [.1/2,1.] by A100,XXREAL_1:1;
then rx in [#](I[01]|B22) by PRE_TOPC:def 5;
then h.rx=g22.rx by A80,A94,FUNCT_4:13
.=g2.rx by A103,FUNCT_1:49
.=(1-(2*rx-1))*|[a,d]|+(2*rx-1)*|[b,d]| by A75,A96,A98
.=f3.rx by A35,A103;
hence thesis;
end;
end;
hence thesis;
end;
then
A104: f2=h by A96,FUNCT_1:2;
for x1,x2 being object st x1 in dom f3 & x2 in dom f3 & f3.x1=f3.x2
holds x1=x2
proof
let x1,x2 be object;
assume that
A105: x1 in dom f3 and
A106: x2 in dom f3 and
A107: f3.x1=f3.x2;
reconsider r1=x1 as Real by A105;
reconsider r2=x2 as Real by A106;
A108: LSeg(|[a,c]|,|[a,d]|) /\ LSeg(|[a,d]|,|[b,d]|) = {|[a,d]|} by A1,A2,Th34;
now per cases by A3,A14,A105,A106,XBOOLE_0:def 3;
case
A109: x1 in [.0,1/2.] & x2 in [.0,1/2.];
then f3.r1=(1-2*r1)*|[a,c]|+(2*r1)*|[a,d]| by A32;
then (1-2*r2)*|[a,c]|+(2*r2)*|[a,d]|= (1-2*r1)*|[a,c]|+(2*r1)*|[a,d]|
by A32,A107,A109;
then (1-2*r2)*|[a,c]|+(2*r2)*|[a,d]| -(2*r1)*|[a,d]|
= (1-2*r1)*|[a,c]| by RLVECT_4:1;
then (1-2*r2)*|[a,c]|+((2*r2)*|[a,d]| -(2*r1)*|[a,d]|)
= (1-2*r1)*|[a,c]| by RLVECT_1:def 3;
then (1-2*r2)*|[a,c]|+(2*r2-2*r1)*(|[a,d]|)
= (1-2*r1)*|[a,c]| by RLVECT_1:35;
then (2*r2-2*r1)*(|[a,d]|)+((1-2*r2)*|[a,c]|-(1-2*r1)*|[a,c]|)
= (1-2*r1)*|[a,c]|-(1-2*r1)*|[a,c]| by RLVECT_1:def 3;
then (2*r2-2*r1)*(|[a,d]|)+((1-2*r2)*|[a,c]|-(1-2*r1)*|[a,c]|)
= 0.TOP-REAL 2 by RLVECT_1:5;
then (2*r2-2*r1)*(|[a,d]|)+((1-2*r2)-(1-2*r1))*|[a,c]|
= 0.TOP-REAL 2 by RLVECT_1:35;
then (2*r2-2*r1)*(|[a,d]|)+(-(2*r2-2*r1))*|[a,c]| = 0.TOP-REAL 2;
then (2*r2-2*r1)*(|[a,d]|)+-((2*r2-2*r1)*|[a,c]|)
= 0.TOP-REAL 2 by RLVECT_1:79;
then (2*r2-2*r1)*(|[a,d]|)-((2*r2-2*r1)*|[a,c]|)
= 0.TOP-REAL 2;
then (2*r2-2*r1)*((|[a,d]|)-(|[a,c]|)) = 0.TOP-REAL 2 by RLVECT_1:34;
then (2*r2-2*r1)=0 or (|[a,d]|)-(|[a,c]|)=0.TOP-REAL 2 by RLVECT_1:11;
then (2*r2-2*r1)=0 or |[a,d]|=|[a,c]| by RLVECT_1:21;
then (2*r2-2*r1)=0 or d =|[a,c]|`2 by EUCLID:52;
hence thesis by A2,EUCLID:52;
end;
case
A110: x1 in [.0,1/2.] & x2 in [.1/2,1.];
then
A111: f3.r1=(1-2*r1)*|[a,c]|+(2*r1)*|[a,d]| by A32;
A112: 0<=r1 by A110,XXREAL_1:1;
r1<=1/2 by A110,XXREAL_1:1;
then r1*2<=1/2*2 by XREAL_1:64;
then
A113: f3.r1 in LSeg(|[a,c]|,|[a,d]|) by A111,A112;
A114: f3.r2=(1-(2*r2-1))*|[a,d]|+(2*r2-1)*|[b,d]| by A35,A110;
A115: 1/2<=r2 by A110,XXREAL_1:1;
A116: r2<=1 by A110,XXREAL_1:1;
r2*2>=1/2*2 by A115,XREAL_1:64;
then
A117: 2*r2-1>=0 by XREAL_1:48;
2*1>=2*r2 by A116,XREAL_1:64;
then 1+1-1>=2*r2-1 by XREAL_1:9;
then f3.r2 in { (1-lambda)*|[a,d]| + lambda*|[b,d]|
where lambda is Real :
0 <= lambda & lambda <= 1 } by A114,A117;
then f3.r1 in LSeg(|[a,c]|,|[a,d]|) /\ LSeg(|[a,d]|,|[b,d]|)
by A107,A113,XBOOLE_0:def 4;
then
A118: f3.r1= |[a,d]| by A108,TARSKI:def 1;
then (1-2*r1)*|[a,c]|+(2*r1)*|[a,d]|+-(|[a,d]|)=0.TOP-REAL 2
by A111,RLVECT_1:5;
then (1-2*r1)*|[a,c]|+(2*r1)*|[a,d]|+(-1)*|[a,d]|=0.TOP-REAL 2
by RLVECT_1:16;
then (1-2*r1)*|[a,c]|+((2*r1)*|[a,d]|+(-1)*|[a,d]|)=0.TOP-REAL 2
by RLVECT_1:def 3;
then (1-2*r1)*|[a,c]|+((2*r1)+(-1))*|[a,d]|=0.TOP-REAL 2 by
RLVECT_1:def 6;
then (1-2*r1)*|[a,c]|+(-(1-(2*r1)))*|[a,d]|=0.TOP-REAL 2;
then (1-2*r1)*|[a,c]|+-((1-(2*r1))*|[a,d]|)=0.TOP-REAL 2 by RLVECT_1:79
;
then (1-2*r1)*|[a,c]|-((1-(2*r1))*|[a,d]|)=0.TOP-REAL 2;
then (1-2*r1)*(|[a,c]|-(|[a,d]|))=0.TOP-REAL 2 by RLVECT_1:34;
then 1-2*r1=0 or (|[a,c]|-(|[a,d]|))=0.TOP-REAL 2 by RLVECT_1:11;
then 1-2*r1=0 or |[a,c]|=|[a,d]| by RLVECT_1:21;
then
A119: 1-2*r1=0 or c =|[a,d]|`2 by EUCLID:52;
(1-(2*r2-1))*|[a,d]|+(2*r2-1)*|[b,d]|+-(|[a,d]|)=0.TOP-REAL 2
by A107,A114,A118,RLVECT_1:5;
then
(1-(2*r2-1))*|[a,d]|+((2*r2-1))*|[b,d]|+(-1)*|[a,d]|=0.TOP-REAL 2
by RLVECT_1:16;
then (2*r2-1) *|[b,d]|+((1-(2*r2-1))*|[a,d]|+(-1)*|[a,d]|)
=0.TOP-REAL 2
by RLVECT_1:def 3;
then (2*r2-1) *|[b,d]|+((1-(2*r2-1))+(-1))*|[a,d]|=0.TOP-REAL 2
by RLVECT_1:def 6;
then (2*r2-1) *|[b,d]|+(-(2*r2-1))*|[a,d]|=0.TOP-REAL 2;
then (2*r2-1) *|[b,d]|+-((2*r2-1)*|[a,d]|)=0.TOP-REAL 2 by RLVECT_1:79;
then (2*r2-1) *|[b,d]|-((2*r2-1)*|[a,d]|)=0.TOP-REAL 2;
then (2*r2-1) *(|[b,d]|-(|[a,d]|))=0.TOP-REAL 2 by RLVECT_1:34;
then (2*r2-1)=0 or (|[b,d]|-(|[a,d]|))=0.TOP-REAL 2 by RLVECT_1:11;
then (2*r2-1)=0 or |[b,d]|=|[a,d]| by RLVECT_1:21;
then (2*r2-1)=0 or b =|[a,d]|`1 by EUCLID:52;
hence thesis by A1,A2,A119,EUCLID:52;
end;
case
A120: x1 in [.1/2,1.] & x2 in [.0,1/2.];
then
A121: f3.r2=(1-2*r2)*|[a,c]|+(2*r2)*|[a,d]| by A32;
A122: 0<=r2 by A120,XXREAL_1:1;
r2<=1/2 by A120,XXREAL_1:1;
then r2*2<=1/2*2 by XREAL_1:64;
then
A123: f3.r2 in LSeg(|[a,c]|,|[a,d]|) by A121,A122;
A124: f3.r1=(1-(2*r1-1))*|[a,d]|+(2*r1-1)*|[b,d]| by A35,A120;
A125: 1/2<=r1 by A120,XXREAL_1:1;
A126: r1<=1 by A120,XXREAL_1:1;
r1*2>=1/2*2 by A125,XREAL_1:64;
then
A127: 2*r1-1>=0 by XREAL_1:48;
2*1>=2*r1 by A126,XREAL_1:64;
then 1+1-1>=2*r1-1 by XREAL_1:9;
then f3.r1 in { (1-lambda)*|[a,d]| + lambda*|[b,d]|
where lambda is Real:
0 <= lambda & lambda <= 1 } by A124,A127;
then f3.r2 in LSeg(|[a,c]|,|[a,d]|) /\ LSeg(|[a,d]|,|[b,d]|)
by A107,A123,XBOOLE_0:def 4;
then
A128: f3.r2= |[a,d]| by A108,TARSKI:def 1;
then (1-2*r2)*|[a,c]|+(2*r2)*|[a,d]|+-(|[a,d]|)=0.TOP-REAL 2
by A121,RLVECT_1:5;
then (1-2*r2)*|[a,c]|+(2*r2)*|[a,d]|+(-1)*|[a,d]|=0.TOP-REAL 2
by RLVECT_1:16;
then (1-2*r2)*|[a,c]|+((2*r2)*|[a,d]|+(-1)*|[a,d]|)=0.TOP-REAL 2
by RLVECT_1:def 3;
then (1-2*r2)*|[a,c]|+((2*r2)+(-1))*|[a,d]|=0.TOP-REAL 2 by
RLVECT_1:def 6;
then (1-2*r2)*|[a,c]|+(-(1-(2*r2)))*|[a,d]|=0.TOP-REAL 2;
then (1-2*r2)*|[a,c]|+-((1-(2*r2))*|[a,d]|)=0.TOP-REAL 2 by RLVECT_1:79
;
then (1-2*r2)*|[a,c]|-((1-(2*r2))*|[a,d]|)=0.TOP-REAL 2;
then (1-2*r2)*(|[a,c]|-(|[a,d]|))=0.TOP-REAL 2 by RLVECT_1:34;
then 1-2*r2=0 or (|[a,c]|-(|[a,d]|))=0.TOP-REAL 2 by RLVECT_1:11;
then 1-2*r2=0 or |[a,c]|=|[a,d]| by RLVECT_1:21;
then
A129: 1-2*r2=0 or c =|[a,d]|`2 by EUCLID:52;
(1-(2*r1-1))*|[a,d]|+(2*r1-1)*|[b,d]|+-(|[a,d]|)=0.TOP-REAL 2
by A107,A124,A128,RLVECT_1:5;
then
(1-(2*r1-1))*|[a,d]|+((2*r1-1))*|[b,d]|+(-1)*|[a,d]|=0.TOP-REAL 2
by RLVECT_1:16;
then (2*r1-1) *|[b,d]|+((1-(2*r1-1))*|[a,d]|+(-1)*|[a,d]|)
=0.TOP-REAL 2
by RLVECT_1:def 3;
then (2*r1-1) *|[b,d]|+(-1+(1-(2*r1-1)))*|[a,d]|=0.TOP-REAL 2 by
RLVECT_1:def 6;
then (2*r1-1) *|[b,d]|+(-(2*r1-1))*|[a,d]|=0.TOP-REAL 2;
then (2*r1-1) *|[b,d]|+-((2*r1-1)*|[a,d]|)=0.TOP-REAL 2 by RLVECT_1:79;
then (2*r1-1) *|[b,d]|-((2*r1-1)*|[a,d]|)=0.TOP-REAL 2;
then (2*r1-1) *(|[b,d]|-(|[a,d]|))=0.TOP-REAL 2 by RLVECT_1:34;
then (2*r1-1)=0 or (|[b,d]|-(|[a,d]|))=0.TOP-REAL 2 by RLVECT_1:11;
then (2*r1-1)=0 or |[b,d]|=|[a,d]| by RLVECT_1:21;
then (2*r1-1)=0 or b =|[a,d]|`1 by EUCLID:52;
hence thesis by A1,A2,A129,EUCLID:52;
end;
case
A130: x1 in [.1/2,1.] & x2 in [.1/2,1.];
then f3.r1=(1-(2*r1-1))*|[a,d]|+((2*r1-1))*|[b,d]| by A35;
then (1-(2*r2-1))*|[a,d]|+((2*r2-1))*|[b,d]|
= (1-(2*r1-1))*|[a,d]|+((2*r1-1))*|[b,d]| by A35,A107,A130;
then (1-(2*r2-1))*|[a,d]|+((2*r2-1))*|[b,d]| -((2*r1-1))*|[b,d]|
= (1-(2*r1-1))*|[a,d]| by RLVECT_4:1;
then (1-(2*r2-1))*|[a,d]|+(((2*r2-1))*|[b,d]| -((2*r1-1))*|[b,d]|)
= (1-(2*r1-1))*|[a,d]| by RLVECT_1:def 3;
then (1-(2*r2-1))*|[a,d]|+((2*r2-1)-(2*r1-1))*(|[b,d]|)
= (1-(2*r1-1))*|[a,d]| by RLVECT_1:35;
then ((2*r2-1)-(2*r1-1))*(|[b,d]|)
+((1-(2*r2-1))*|[a,d]|-(1-(2*r1-1))*|[a,d]|)
= (1-(2*r1-1))*|[a,d]|-(1-(2*r1-1))*|[a,d]| by RLVECT_1:def 3;
then ((2*r2-1)-(2*r1-1))*(|[b,d]|)
+((1-(2*r2-1))*|[a,d]|-(1-(2*r1-1))*|[a,d]|) = 0.TOP-REAL 2
by RLVECT_1:5;
then
((2*r2-1)-(2*r1-1))*(|[b,d]|)+((1-(2*r2-1))-(1-(2*r1-1)))*|[a,d]|
= 0.TOP-REAL 2 by RLVECT_1:35;
then ((2*r2-1)-(2*r1-1))*(|[b,d]|)+(-((2*r2-1)-(2*r1-1)))*|[a,d]|
= 0.TOP-REAL 2;
then ((2*r2-1)-(2*r1-1))*(|[b,d]|)+-(((2*r2-1)-(2*r1-1))*|[a,d]|)
= 0.TOP-REAL 2 by RLVECT_1:79;
then ((2*r2-1)-(2*r1-1))*(|[b,d]|)-(((2*r2-1)-(2*r1-1))*|[a,d]|)
= 0.TOP-REAL 2;
then ((2*r2-1)-(2*r1-1))*((|[b,d]|)-(|[a,d]|))
= 0.TOP-REAL 2 by RLVECT_1:34;
then ((2*r2-1)-(2*r1-1))=0 or (|[b,d]|)-(|[a,d]|)=0.TOP-REAL 2
by RLVECT_1:11;
then ((2*r2-1)-(2*r1-1))=0 or |[b,d]|=|[a,d]| by RLVECT_1:21;
then ((2*r2-1)-(2*r1-1))=0 or b =|[a,d]|`1 by EUCLID:52;
hence thesis by A1,EUCLID:52;
end;
end;
hence thesis;
end;
then
A131: f3 is one-to-one by FUNCT_1:def 4;
[#]((TOP-REAL 2)|(Upper_Arc(K))) c= rng f3
proof
let y be object;
assume y in [#]((TOP-REAL 2)|(Upper_Arc(K)));
then
A132: y in Upper_Arc(K) by PRE_TOPC:def 5;
then reconsider q=y as Point of TOP-REAL 2;
A133: Upper_Arc(K)=LSeg(|[a,c]|,|[a,d]|) \/ LSeg(|[a,d]|,|[b,d]|) by A1,A2,Th51
;
now per cases by A132,A133,XBOOLE_0:def 3;
case
A134: q in LSeg(|[a,c]|,|[a,d]|);
then
A135: 0<=((q`2)-c)/(d-c)/2 by A38;
A136: ((q`2)-c)/(d-c)/2<=1 by A38,A134;
A137: f3.(((q`2)-c)/(d-c)/2)=q by A38,A134;
((q`2)-c)/(d-c)/2 in [.0,1.] by A135,A136,XXREAL_1:1;
hence thesis by A14,A137,FUNCT_1:def 3;
end;
case
A138: q in LSeg(|[a,d]|,|[b,d]|);
then
A139: 0<=((q`1)-a)/(b-a)/2+1/2 by A48;
A140: ((q`1)-a)/(b-a)/2+1/2<=1 by A48,A138;
A141: f3.(((q`1)-a)/(b-a)/2+1/2)=q by A48,A138;
((q`1)-a)/(b-a)/2+1/2 in [.0,1.] by A139,A140,XXREAL_1:1;
hence thesis by A14,A141,FUNCT_1:def 3;
end;
end;
hence thesis;
end;
then
A142: rng f3=[#]((TOP-REAL 2)|(Upper_Arc(K)));
I[01] is compact by HEINE:4,TOPMETR:20;
then
A143: f3 is being_homeomorphism
by A95,A104,A131,A142,COMPTS_1:17,JGRAPH_1:45;
rng f3=Upper_Arc(K) by A142,PRE_TOPC:def 5;
hence thesis by A29,A31,A32,A35,A38,A48,A143;
end;
theorem Th54:
for a,b,c,d being Real st a=1/2*2 by A23,XREAL_1:64;
then
A25: 2*r-1>=0 by XREAL_1:48;
2*1>=2*r by A24,XREAL_1:64;
then
A26: 1+1-1>=2*r-1 by XREAL_1:9;
f2.x= (1-(2*r-1))*|[b,c]|+(2*r-1)*|[a,c]| by A14,A15,A16,A22;
then
A27: y in LSeg(|[b,c]|,|[a,c]|) by A17,A25,A26;
Lower_Arc(K)= LSeg(|[a,c]|,|[b,c]|) \/ LSeg(|[b,c]|,|[b,d]|)
by A1,A2,Th52;
then y in Lower_Arc(K) by A27,XBOOLE_0:def 3;
hence thesis by PRE_TOPC:8;
end;
end;
hence thesis;
end;
then reconsider f3=f2 as Function of I[01],(TOP-REAL 2)|(Lower_Arc(K))
by A14,BORSUK_1:40,FUNCT_2:2;
A28: 0 in [.0,1.] by XXREAL_1:1;
0 in [.0,1/2.] by XXREAL_1:1;
then
A29: f3.0= (1-2*0)*|[b,d]|+(2*0)*|[b,c]| by A15,A28
.= (1)*|[b,d]|+0.TOP-REAL 2 by RLVECT_1:10
.= |[b,d]|+0.TOP-REAL 2 by RLVECT_1:def 8
.= |[b,d]| by RLVECT_1:4
.= E-max(K) by A1,A2,Th46;
A30: 1 in [.0,1.] by XXREAL_1:1;
1 in [.1/2,1.] by XXREAL_1:1;
then
A31: f3.1= (1-(2*1-1))*|[b,c]|+(2*1-1)*|[a,c]| by A15,A30
.= (0)*|[b,c]|+|[a,c]| by RLVECT_1:def 8
.= (0.TOP-REAL 2) + |[a,c]| by RLVECT_1:10
.= |[a,c]| by RLVECT_1:4
.= W-min(K) by A1,A2,Th46;
A32: for r being Real st r in [.0,1/2.] holds
f3.r=(1-2*r)*|[b,d]|+(2*r)*|[b,c]|
proof
let r be Real;
assume
A33: r in [.0,1/2.];
then
A34: 0<=r by XXREAL_1:1;
r<=1/2 by A33,XXREAL_1:1;
then r<=1 by XXREAL_0:2;
then r in [.0,1.] by A34,XXREAL_1:1;
hence thesis by A15,A33;
end;
A35: for r being Real st r in [.1/2,1.] holds
f3.r=(1-(2*r-1))*|[b,c]|+(2*r-1)*|[a,c]|
proof
let r be Real;
assume
A36: r in [.1/2,1.];
then
A37: 1/2<=r by XXREAL_1:1;
r<=1 by A36,XXREAL_1:1;
then r in [.0,1.] by A37,XXREAL_1:1;
hence thesis by A15,A36;
end;
A38: for p being Point of TOP-REAL 2 st p in LSeg(|[b,d]|,|[b,c]|)
holds 0<=((p`2)-d)/(c-d)/2 & ((p`2)-d)/(c-d)/2<=1
& f3.(((p`2)-d)/(c-d)/2)=p
proof
let p be Point of TOP-REAL 2;
assume
A39: p in LSeg(|[b,d]|,|[b,c]|);
A40: (|[b,d]|)`2= d by EUCLID:52;
A41: (|[b,c]|)`2= c by EUCLID:52;
then
A42: c <=p`2 by A2,A39,A40,TOPREAL1:4;
A43: p`2<=d by A2,A39,A40,A41,TOPREAL1:4;
d-c>0 by A2,XREAL_1:50;
then
A44: -(d-c)< -0 by XREAL_1:24;
d-(p`2) >=0 by A43,XREAL_1:48;
then
A45: -(d-(p`2)) <= -0;
(p`2) -d >=c-d by A42,XREAL_1:9;
then ((p`2) -d)/(c-d) <=(c-d)/(c-d) by A44,XREAL_1:73;
then ((p`2) -d)/(c-d) <=1 by A44,XCMPLX_1:60;
then
A46: ((p`2) -d)/(c-d)/2 <=1/2 by XREAL_1:72;
set r=((p`2)-d)/(c-d)/2;
r in [.0,1/2.] by A44,A45,A46,XXREAL_1:1;
then f3.(((p`2)-d)/(c-d)/2)=(1-2*r)*|[b,d]|+(2*r)*|[b,c]| by A32
.=|[(1-2*r)*b,(1-2*r)*d]|+(2*r)*|[b,c]| by EUCLID:58
.=|[(1-2*r)*b,(1-2*r)*d]|+|[(2*r)*b,(2*r)*c]| by EUCLID:58
.=|[1*b-(2*r)*b+(2*r)*b,(1-2*r)*d+(2*r)*c]| by EUCLID:56
.=|[b,1*d+(((p`2)-d)/(c-d))*(c-d)]|
.=|[b,1*d+((p`2)-d)]| by A44,XCMPLX_1:87
.=|[p`1,p`2]| by A39,TOPREAL3:11
.= p by EUCLID:53;
hence thesis by A44,A45,A46,XXREAL_0:2;
end;
A47: for p being Point of TOP-REAL 2 st p in LSeg(|[b,c]|,|[a,c]|)
holds 0<=((p`1)-b)/(a-b)/2+1/2 & ((p`1)-b)/(a-b)/2+1/2<=1
& f3.(((p`1)-b)/(a-b)/2+1/2)=p
proof
let p be Point of TOP-REAL 2;
assume
A48: p in LSeg(|[b,c]|,|[a,c]|);
A49: (|[b,c]|)`1= b by EUCLID:52;
A50: (|[a,c]|)`1= a by EUCLID:52;
then
A51: a <=p`1 by A1,A48,A49,TOPREAL1:3;
A52: p`1<=b by A1,A48,A49,A50,TOPREAL1:3;
b-a>0 by A1,XREAL_1:50;
then
A53: -(b-a)< -0 by XREAL_1:24;
b-(p`1) >=0 by A52,XREAL_1:48;
then
A54: -(b-(p`1)) <= -0;
then
A55: ((p`1) -b)/(a-b)/2+1/2 >=0+1/2 by A53,XREAL_1:7;
(p`1) -b >=a-b by A51,XREAL_1:9;
then ((p`1) -b)/(a-b) <=(a-b)/(a-b) by A53,XREAL_1:73;
then ((p`1) -b)/(a-b) <=1 by A53,XCMPLX_1:60;
then ((p`1) -b)/(a-b)/2 <=1/2 by XREAL_1:72;
then
A56: ((p`1) -b)/(a-b)/2+1/2 <=1/2+1/2 by XREAL_1:7;
set r=((p`1)-b)/(a-b)/2+1/2;
r in [.1/2,1.] by A55,A56,XXREAL_1:1;
then f3.(((p`1)-b)/(a-b)/2+1/2)=(1-(2*r-1))*|[b,c]|+(2*r-1)*|[a,c]| by A35
.=|[(1-(2*r-1))*b,(1-(2*r-1))*c]|+((2*r-1))*|[a,c]| by EUCLID:58
.=|[(1-(2*r-1))*b,(1-(2*r-1))*c]|+|[((2*r-1))*a,((2*r-1))*c]|
by EUCLID:58
.=|[(1-(2*r-1))*b+((2*r-1))*a,1*c-(2*r-1)*c+((2*r-1))*c]| by EUCLID:56
.=|[1*b+(((p`1)-b)/(a-b))*(a-b),c]|
.=|[1*b+((p`1)-b),c]| by A53,XCMPLX_1:87
.=|[p`1,p`2]| by A48,TOPREAL3:12
.= p by EUCLID:53;
hence thesis by A53,A54,A56;
end;
reconsider B00=[.0,1.] as Subset of R^1 by TOPMETR:17;
reconsider B01=B00 as non empty Subset of R^1 by XXREAL_1:1;
I[01]=(R^1)|B01 by TOPMETR:19,20;
then consider h1 being Function of I[01],R^1 such that
A57: for p being Point of I[01] holds h1.p=p and
A58: h1 is continuous by Th6;
consider h2 being Function of I[01],R^1 such that
A59: for p being Point of I[01],r1 being Real st h1.p=r1 holds h2.p
=2*r1 and
A60: h2 is continuous by A58,JGRAPH_2:23;
consider h5 being Function of I[01],R^1 such that
A61: for p being Point of I[01],r1 being Real st h2.p=r1 holds h5.p
=1-r1 and
A62: h5 is continuous by A60,Th8;
consider h3 being Function of I[01],R^1 such that
A63: for p being Point of I[01],r1 being Real st h2.p=r1 holds h3.p
=r1-1 and
A64: h3 is continuous by A60,Th7;
consider h4 being Function of I[01],R^1 such that
A65: for p being Point of I[01],r1 being Real st h3.p=r1 holds h4.p
=1-r1 and
A66: h4 is continuous by A64,Th8;
consider g1 being Function of I[01],TOP-REAL 2 such that
A67: for r being Point of I[01] holds g1.r=(h5.r)*|[b,d]|+(h2.r)*|[b,c]| and
A68: g1 is continuous by A60,A62,Th13;
A69: for r being Point of I[01],s being Real st r=s holds
g1.r=(1-2*s)*|[b,d]|+(2*s)*|[b,c]|
proof
let r be Point of I[01],s be Real;
assume
A70: r=s;
g1.r=(h5.r)*|[b,d]|+(h2.r)*|[b,c]| by A67
.=(1-2*(h1.r))*|[b,d]|+(h2.r)*|[b,c]| by A59,A61
.=(1-2*(h1.r))*|[b,d]|+(2*(h1.r))*|[b,c]| by A59
.=(1-2*s)*|[b,d]|+(2*(h1.r))*|[b,c]| by A57,A70
.=(1-2*s)*|[b,d]|+(2*s)*|[b,c]| by A57,A70;
hence thesis;
end;
consider g2 being Function of I[01],TOP-REAL 2 such that
A71: for r being Point of I[01] holds g2.r=(h4.r)*|[b,c]|+(h3.r)*|[a,c]| and
A72: g2 is continuous by A64,A66,Th13;
A73: for r being Point of I[01],s being Real st r=s holds
g2.r=(1-(2*s-1))*|[b,c]|+(2*s-1)*|[a,c]|
proof
let r be Point of I[01],s be Real;
assume
A74: r=s;
g2.r=(h4.r)*|[b,c]|+(h3.r)*|[a,c]| by A71
.=(1-((h2.r)-1))*|[b,c]|+(h3.r)*|[a,c]| by A63,A65
.=(1-((h2.r)-1))*|[b,c]|+((h2.r)-1)*|[a,c]| by A63
.=(1-(2*(h1.r)-1))*|[b,c]|+((h2.r)-1)*|[a,c]| by A59
.=(1-(2*(h1.r)-1))*|[b,c]|+(2*(h1.r)-1)*|[a,c]| by A59
.=(1-(2*s-1))*|[b,c]|+(2*(h1.r)-1)*|[a,c]| by A57,A74
.=(1-(2*s-1))*|[b,c]|+(2*s-1)*|[a,c]| by A57,A74;
hence thesis;
end;
reconsider B11=[.0,1/2.] as non empty Subset of I[01]
by A3,BORSUK_1:40,XBOOLE_1:7,XXREAL_1:1;
A75: dom (g1|B11)=dom g1 /\ B11 by RELAT_1:61
.= (the carrier of I[01]) /\ B11 by FUNCT_2:def 1
.=B11 by XBOOLE_1:28
.=the carrier of (I[01]|B11) by PRE_TOPC:8;
rng (g1|B11) c= the carrier of TOP-REAL 2;
then reconsider g11=g1|B11 as Function
of I[01]|B11,TOP-REAL 2 by A75,FUNCT_2:2;
A76: TOP-REAL 2 is SubSpace of TOP-REAL 2 by TSEP_1:2;
then
A77: g11 is continuous by A68,BORSUK_4:44;
reconsider B22=[.1/2,1.] as non empty Subset of I[01]
by A3,BORSUK_1:40,XBOOLE_1:7,XXREAL_1:1;
A78: dom (g2|B22)=dom g2 /\ B22 by RELAT_1:61
.= (the carrier of I[01]) /\ B22 by FUNCT_2:def 1
.=B22 by XBOOLE_1:28
.=the carrier of (I[01]|B22) by PRE_TOPC:8;
rng (g2|B22) c= the carrier of TOP-REAL 2;
then reconsider g22=g2|B22 as Function
of I[01]|B22,TOP-REAL 2 by A78,FUNCT_2:2;
A79: g22 is continuous by A72,A76,BORSUK_4:44;
A80: B11=[#](I[01]|B11) by PRE_TOPC:def 5;
A81: B22=[#](I[01]|B22) by PRE_TOPC:def 5;
A82: B11 is closed by Th4;
A83: B22 is closed by Th4;
A84: [#](I[01]|B11) \/ [#](I[01]|B22)=[#]I[01]
by A80,A81,BORSUK_1:40,XXREAL_1:165;
for p being object st p in ([#](I[01]|B11)) /\ ([#](I[01]|B22))
holds g11.p = g22.p
proof
let p be object;
assume
A85: p in ([#](I[01]|B11)) /\ ([#](I[01]|B22));
then
A86: p in [#](I[01]|B11) by XBOOLE_0:def 4;
A87: p in [#](I[01]|B22) by A85;
A88: p in B11 by A86,PRE_TOPC:def 5;
A89: p in B22 by A87,PRE_TOPC:def 5;
reconsider rp=p as Real by A88;
A90: rp<=1/2 by A88,XXREAL_1:1;
rp>=1/2 by A89,XXREAL_1:1;
then rp=1/2 by A90,XXREAL_0:1;
then
A91: 2*rp=1;
thus g11.p=g1.p by A88,FUNCT_1:49
.= (1-1)*|[b,d]|+(1)*|[b,c]| by A69,A88,A91
.=0.TOP-REAL 2 +1*|[b,c]| by RLVECT_1:10
.=(1-0)*|[b,c]| +(1-1)*|[a,c]| by RLVECT_1:10
.=g2.p by A73,A88,A91
.=g22.p by A89,FUNCT_1:49;
end;
then consider h being Function of I[01],TOP-REAL 2 such that
A92: h=g11+*g22 and
A93: h is continuous by A77,A79,A80,A81,A82,A83,A84,JGRAPH_2:1;
A94: dom f3=dom h by Th5;
A95: dom f3=the carrier of I[01] by Th5;
for x being object st x in dom f2 holds f3.x=h.x
proof
let x be object;
assume
A96: x in dom f2;
then reconsider rx=x as Real by A95;
A97: 0<=rx by A94,A96,BORSUK_1:40,XXREAL_1:1;
A98: rx<=1 by A94,A96,BORSUK_1:40,XXREAL_1:1;
per cases;
suppose
A99: rx<1/2;
then
A100: rx in [.0,1/2.] by A97,XXREAL_1:1;
not rx in dom g22 by A81,A99,XXREAL_1:1;
then h.rx=g11.rx by A92,FUNCT_4:11
.=g1.rx by A100,FUNCT_1:49
.=(1-(2*rx))*|[b,d]|+(2*rx)*|[b,c]| by A69,A94,A96
.=f3.rx by A32,A100;
hence thesis;
end;
suppose rx >=1/2;
then
A101: rx in [.1/2,1.] by A98,XXREAL_1:1;
then rx in [#](I[01]|B22) by PRE_TOPC:def 5;
then h.rx=g22.rx by A78,A92,FUNCT_4:13
.=g2.rx by A101,FUNCT_1:49
.=(1-(2*rx-1))*|[b,c]|+(2*rx-1)*|[a,c]| by A73,A94,A96
.=f3.rx by A35,A101;
hence thesis;
end;
end;
then
A102: f2=h by A94,FUNCT_1:2;
for x1,x2 being object st x1 in dom f3 & x2 in dom f3 & f3.x1=f3.x2
holds x1=x2
proof
let x1,x2 be object;
assume that
A103: x1 in dom f3 and
A104: x2 in dom f3 and
A105: f3.x1=f3.x2;
reconsider r1=x1 as Real by A103;
reconsider r2=x2 as Real by A104;
A106: LSeg(|[b,d]|,|[b,c]|) /\ LSeg(|[b,c]|,|[a,c]|) = {|[b,c]|} by A1,A2,Th32;
now per cases by A3,A14,A103,A104,XBOOLE_0:def 3;
case
A107: x1 in [.0,1/2.] & x2 in [.0,1/2.];
then f3.r1=(1-2*r1)*|[b,d]|+(2*r1)*|[b,c]| by A32;
then (1-2*r2)*|[b,d]|+(2*r2)*|[b,c]|= (1-2*r1)*|[b,d]|+(2*r1)*|[b,c]|
by A32,A105,A107;
then (1-2*r2)*|[b,d]|+(2*r2)*|[b,c]| -(2*r1)*|[b,c]|
= (1-2*r1)*|[b,d]| by RLVECT_4:1;
then (1-2*r2)*|[b,d]|+((2*r2)*|[b,c]| -(2*r1)*|[b,c]|)
= (1-2*r1)*|[b,d]| by RLVECT_1:def 3;
then (1-2*r2)*|[b,d]|+(2*r2-2*r1)*(|[b,c]|)
= (1-2*r1)*|[b,d]| by RLVECT_1:35;
then (2*r2-2*r1)*(|[b,c]|)+((1-2*r2)*|[b,d]|-(1-2*r1)*|[b,d]|)
= (1-2*r1)*|[b,d]|-(1-2*r1)*|[b,d]| by RLVECT_1:def 3;
then (2*r2-2*r1)*(|[b,c]|)+((1-2*r2)*|[b,d]|-(1-2*r1)*|[b,d]|)
= 0.TOP-REAL 2 by RLVECT_1:5;
then (2*r2-2*r1)*(|[b,c]|)+((1-2*r2)-(1-2*r1))*|[b,d]|
= 0.TOP-REAL 2 by RLVECT_1:35;
then (2*r2-2*r1)*(|[b,c]|)+(-(2*r2-2*r1))*|[b,d]| = 0.TOP-REAL 2;
then (2*r2-2*r1)*(|[b,c]|)+-((2*r2-2*r1)*|[b,d]|)
= 0.TOP-REAL 2 by RLVECT_1:79;
then (2*r2-2*r1)*(|[b,c]|)-((2*r2-2*r1)*|[b,d]|)
= 0.TOP-REAL 2;
then (2*r2-2*r1)*((|[b,c]|)-(|[b,d]|)) = 0.TOP-REAL 2 by RLVECT_1:34;
then (2*r2-2*r1)=0 or (|[b,c]|)-(|[b,d]|)=0.TOP-REAL 2 by RLVECT_1:11;
then (2*r2-2*r1)=0 or |[b,c]|=|[b,d]| by RLVECT_1:21;
then (2*r2-2*r1)=0 or d =|[b,c]|`2 by EUCLID:52;
hence thesis by A2,EUCLID:52;
end;
case
A108: x1 in [.0,1/2.] & x2 in [.1/2,1.];
then
A109: f3.r1=(1-2*r1)*|[b,d]|+(2*r1)*|[b,c]| by A32;
A110: 0<=r1 by A108,XXREAL_1:1;
r1<=1/2 by A108,XXREAL_1:1;
then r1*2<=1/2*2 by XREAL_1:64;
then
A111: f3.r1 in LSeg(|[b,d]|,|[b,c]|) by A109,A110;
A112: f3.r2=(1-(2*r2-1))*|[b,c]|+(2*r2-1)*|[a,c]| by A35,A108;
A113: 1/2<=r2 by A108,XXREAL_1:1;
A114: r2<=1 by A108,XXREAL_1:1;
r2*2>=1/2*2 by A113,XREAL_1:64;
then
A115: 2*r2-1>=0 by XREAL_1:48;
2*1>=2*r2 by A114,XREAL_1:64;
then 1+1-1>=2*r2-1 by XREAL_1:9;
then f3.r2 in { (1-lambda)*|[b,c]| + lambda*|[a,c]|
where lambda is Real:
0 <= lambda & lambda <= 1 } by A112,A115;
then f3.r1 in LSeg(|[b,d]|,|[b,c]|) /\ LSeg(|[b,c]|,|[a,c]|)
by A105,A111,XBOOLE_0:def 4;
then
A116: f3.r1= |[b,c]| by A106,TARSKI:def 1;
then (1-2*r1)*|[b,d]|+(2*r1)*|[b,c]|+-(|[b,c]|)=0.TOP-REAL 2
by A109,RLVECT_1:5;
then (1-2*r1)*|[b,d]|+(2*r1)*|[b,c]|+(-1)*|[b,c]|=0.TOP-REAL 2
by RLVECT_1:16;
then (1-2*r1)*|[b,d]|+((2*r1)*|[b,c]|+(-1)*|[b,c]|)=0.TOP-REAL 2
by RLVECT_1:def 3;
then (1-2*r1)*|[b,d]|+((2*r1)+(-1))*|[b,c]|=0.TOP-REAL 2 by
RLVECT_1:def 6;
then (1-2*r1)*|[b,d]|+(-(1-(2*r1)))*|[b,c]|=0.TOP-REAL 2;
then (1-2*r1)*|[b,d]|+-((1-(2*r1))*|[b,c]|)=0.TOP-REAL 2 by RLVECT_1:79
;
then (1-2*r1)*|[b,d]|-((1-(2*r1))*|[b,c]|)=0.TOP-REAL 2;
then (1-2*r1)*(|[b,d]|-(|[b,c]|))=0.TOP-REAL 2 by RLVECT_1:34;
then 1-2*r1=0 or (|[b,d]|-(|[b,c]|))=0.TOP-REAL 2 by RLVECT_1:11;
then 1-2*r1=0 or |[b,d]|=|[b,c]| by RLVECT_1:21;
then
A117: 1-2*r1=0 or d =|[b,c]|`2 by EUCLID:52;
(1-(2*r2-1))*|[b,c]|+(2*r2-1)*|[a,c]|+-(|[b,c]|)=0.TOP-REAL 2
by A105,A112,A116,RLVECT_1:5;
then
(1-(2*r2-1))*|[b,c]|+((2*r2-1))*|[a,c]|+(-1)*|[b,c]|=0.TOP-REAL 2
by RLVECT_1:16;
then (2*r2-1) *|[a,c]|+((1-(2*r2-1))*|[b,c]|+(-1)*|[b,c]|)
=0.TOP-REAL 2
by RLVECT_1:def 3;
then (2*r2-1) *|[a,c]|+((1-(2*r2-1))+(-1))*|[b,c]|=0.TOP-REAL 2
by RLVECT_1:def 6;
then (2*r2-1) *|[a,c]|+(-(2*r2-1))*|[b,c]|=0.TOP-REAL 2;
then (2*r2-1) *|[a,c]|+-((2*r2-1)*|[b,c]|)=0.TOP-REAL 2 by RLVECT_1:79;
then (2*r2-1) *|[a,c]|-((2*r2-1)*|[b,c]|)=0.TOP-REAL 2;
then (2*r2-1) *(|[a,c]|-(|[b,c]|))=0.TOP-REAL 2 by RLVECT_1:34;
then (2*r2-1)=0 or (|[a,c]|-(|[b,c]|))=0.TOP-REAL 2 by RLVECT_1:11;
then (2*r2-1)=0 or |[a,c]|=|[b,c]| by RLVECT_1:21;
then (2*r2-1)=0 or a =|[b,c]|`1 by EUCLID:52;
hence thesis by A1,A2,A117,EUCLID:52;
end;
case
A118: x1 in [.1/2,1.] & x2 in [.0,1/2.];
then
A119: f3.r2=(1-2*r2)*|[b,d]|+(2*r2)*|[b,c]| by A32;
A120: 0<=r2 by A118,XXREAL_1:1;
r2<=1/2 by A118,XXREAL_1:1;
then r2*2<=1/2*2 by XREAL_1:64;
then
A121: f3.r2 in LSeg(|[b,d]|,|[b,c]|) by A119,A120;
A122: f3.r1=(1-(2*r1-1))*|[b,c]|+(2*r1-1)*|[a,c]| by A35,A118;
A123: 1/2<=r1 by A118,XXREAL_1:1;
A124: r1<=1 by A118,XXREAL_1:1;
r1*2>=1/2*2 by A123,XREAL_1:64;
then
A125: 2*r1-1>=0 by XREAL_1:48;
2*1>=2*r1 by A124,XREAL_1:64;
then 1+1-1>=2*r1-1 by XREAL_1:9;
then f3.r1 in { (1-lambda)*|[b,c]| + lambda*|[a,c]|
where lambda is Real:
0 <= lambda & lambda <= 1 } by A122,A125;
then f3.r2 in LSeg(|[b,d]|,|[b,c]|) /\ LSeg(|[b,c]|,|[a,c]|)
by A105,A121,XBOOLE_0:def 4;
then
A126: f3.r2= |[b,c]| by A106,TARSKI:def 1;
then (1-2*r2)*|[b,d]|+(2*r2)*|[b,c]|+-(|[b,c]|)=0.TOP-REAL 2
by A119,RLVECT_1:5;
then (1-2*r2)*|[b,d]|+(2*r2)*|[b,c]|+(-1)*|[b,c]|=0.TOP-REAL 2
by RLVECT_1:16;
then (1-2*r2)*|[b,d]|+((2*r2)*|[b,c]|+(-1)*|[b,c]|)=0.TOP-REAL 2
by RLVECT_1:def 3;
then (1-2*r2)*|[b,d]|+((2*r2)+(-1))*|[b,c]|=0.TOP-REAL 2 by
RLVECT_1:def 6;
then (1-2*r2)*|[b,d]|+(-(1-(2*r2)))*|[b,c]|=0.TOP-REAL 2;
then (1-2*r2)*|[b,d]|+-((1-(2*r2))*|[b,c]|)=0.TOP-REAL 2 by RLVECT_1:79
;
then (1-2*r2)*|[b,d]|-((1-(2*r2))*|[b,c]|)=0.TOP-REAL 2;
then (1-2*r2)*(|[b,d]|-(|[b,c]|))=0.TOP-REAL 2 by RLVECT_1:34;
then 1-2*r2=0 or (|[b,d]|-(|[b,c]|))=0.TOP-REAL 2 by RLVECT_1:11;
then 1-2*r2=0 or |[b,d]|=|[b,c]| by RLVECT_1:21;
then
A127: 1-2*r2=0 or d =|[b,c]|`2 by EUCLID:52;
(1-(2*r1-1))*|[b,c]|+(2*r1-1)*|[a,c]|+-(|[b,c]|)=0.TOP-REAL 2
by A105,A122,A126,RLVECT_1:5;
then
(1-(2*r1-1))*|[b,c]|+((2*r1-1))*|[a,c]|+(-1)*|[b,c]|=0.TOP-REAL 2
by RLVECT_1:16;
then (2*r1-1) *|[a,c]|+((1-(2*r1-1))*|[b,c]|+(-1)*|[b,c]|)
=0.TOP-REAL 2
by RLVECT_1:def 3;
then (2*r1-1) *|[a,c]|+((1-(2*r1-1))+(-1))*|[b,c]|=0.TOP-REAL 2
by RLVECT_1:def 6;
then (2*r1-1) *|[a,c]|+(-(2*r1-1))*|[b,c]|=0.TOP-REAL 2;
then (2*r1-1) *|[a,c]|+-((2*r1-1)*|[b,c]|)=0.TOP-REAL 2 by RLVECT_1:79;
then (2*r1-1) *|[a,c]|-((2*r1-1)*|[b,c]|)=0.TOP-REAL 2;
then (2*r1-1) *(|[a,c]|-(|[b,c]|))=0.TOP-REAL 2 by RLVECT_1:34;
then (2*r1-1)=0 or (|[a,c]|-(|[b,c]|))=0.TOP-REAL 2 by RLVECT_1:11;
then (2*r1-1)=0 or |[a,c]|=|[b,c]| by RLVECT_1:21;
then (2*r1-1)=0 or a =|[b,c]|`1 by EUCLID:52;
hence thesis by A1,A2,A127,EUCLID:52;
end;
case
A128: x1 in [.1/2,1.] & x2 in [.1/2,1.];
then f3.r1=(1-(2*r1-1))*|[b,c]|+((2*r1-1))*|[a,c]| by A35;
then (1-(2*r2-1))*|[b,c]|+((2*r2-1))*|[a,c]|
= (1-(2*r1-1))*|[b,c]|+((2*r1-1))*|[a,c]| by A35,A105,A128;
then (1-(2*r2-1))*|[b,c]|+((2*r2-1))*|[a,c]| -((2*r1-1))*|[a,c]|
= (1-(2*r1-1))*|[b,c]| by RLVECT_4:1;
then (1-(2*r2-1))*|[b,c]|+(((2*r2-1))*|[a,c]| -((2*r1-1))*|[a,c]|)
= (1-(2*r1-1))*|[b,c]| by RLVECT_1:def 3;
then (1-(2*r2-1))*|[b,c]|+((2*r2-1)-(2*r1-1))*(|[a,c]|)
= (1-(2*r1-1))*|[b,c]| by RLVECT_1:35;
then ((2*r2-1)-(2*r1-1))*(|[a,c]|)
+((1-(2*r2-1))*|[b,c]|-(1-(2*r1-1))*|[b,c]|)
= (1-(2*r1-1))*|[b,c]|-(1-(2*r1-1))*|[b,c]| by RLVECT_1:def 3;
then ((2*r2-1)-(2*r1-1))*(|[a,c]|)
+((1-(2*r2-1))*|[b,c]|-(1-(2*r1-1))*|[b,c]|) = 0.TOP-REAL 2
by RLVECT_1:5;
then
((2*r2-1)-(2*r1-1))*(|[a,c]|)+((1-(2*r2-1))-(1-(2*r1-1)))*|[b,c]|
= 0.TOP-REAL 2 by RLVECT_1:35;
then ((2*r2-1)-(2*r1-1))*(|[a,c]|)+(-((2*r2-1)-(2*r1-1)))*|[b,c]|
= 0.TOP-REAL 2;
then ((2*r2-1)-(2*r1-1))*(|[a,c]|)+-(((2*r2-1)-(2*r1-1))*|[b,c]|)
= 0.TOP-REAL 2 by RLVECT_1:79;
then ((2*r2-1)-(2*r1-1))*(|[a,c]|)-(((2*r2-1)-(2*r1-1))*|[b,c]|)
= 0.TOP-REAL 2;
then ((2*r2-1)-(2*r1-1))*((|[a,c]|)-(|[b,c]|))
= 0.TOP-REAL 2 by RLVECT_1:34;
then ((2*r2-1)-(2*r1-1))=0 or (|[a,c]|)-(|[b,c]|)=0.TOP-REAL 2
by RLVECT_1:11;
then ((2*r2-1)-(2*r1-1))=0 or |[a,c]|=|[b,c]| by RLVECT_1:21;
then ((2*r2-1)-(2*r1-1))=0 or a =|[b,c]|`1 by EUCLID:52;
hence thesis by A1,EUCLID:52;
end;
end;
hence thesis;
end;
then
A129: f3 is one-to-one by FUNCT_1:def 4;
[#]((TOP-REAL 2)|(Lower_Arc(K))) c= rng f3
proof
let y be object;
assume y in [#]((TOP-REAL 2)|(Lower_Arc(K)));
then
A130: y in Lower_Arc(K) by PRE_TOPC:def 5;
then reconsider q=y as Point of TOP-REAL 2;
A131: Lower_Arc(K)=LSeg(|[b,d]|,|[b,c]|) \/ LSeg(|[b,c]|,|[a,c]|) by A1,A2,Th52
;
now per cases by A130,A131,XBOOLE_0:def 3;
case
A132: q in LSeg(|[b,d]|,|[b,c]|);
then
A133: 0<=((q`2)-d)/(c-d)/2 by A38;
A134: ((q`2)-d)/(c-d)/2<=1 by A38,A132;
A135: f3.(((q`2)-d)/(c-d)/2)=q by A38,A132;
((q`2)-d)/(c-d)/2 in [.0,1.] by A133,A134,XXREAL_1:1;
hence thesis by A14,A135,FUNCT_1:def 3;
end;
case
A136: q in LSeg(|[b,c]|,|[a,c]|);
then
A137: 0<=((q`1)-b)/(a-b)/2+1/2 by A47;
A138: ((q`1)-b)/(a-b)/2+1/2<=1 by A47,A136;
A139: f3.(((q`1)-b)/(a-b)/2+1/2)=q by A47,A136;
((q`1)-b)/(a-b)/2+1/2 in [.0,1.] by A137,A138,XXREAL_1:1;
hence thesis by A14,A139,FUNCT_1:def 3;
end;
end;
hence thesis;
end;
then
A140: rng f3=[#]((TOP-REAL 2)|(Lower_Arc K));
I[01] is compact by HEINE:4,TOPMETR:20;
then
A141: f3 is being_homeomorphism
by A93,A102,A129,A140,COMPTS_1:17,JGRAPH_1:45;
rng f3=Lower_Arc(K) by A140,PRE_TOPC:def 5;
hence thesis by A29,A31,A32,A35,A38,A47,A141;
end;
theorem Th55:
for a,b,c,d being Real,p1,p2 being Point of TOP-REAL 2 st a0 by A2,XREAL_1:50;
A23: s1<=1 by A3,A19;
A24: 0<=s2 by A4,A19;
s2<=1 by A4,A19;
then s1<=s2 by A13,A15,A16,A17,A18,A20,A21,A23,A24,JORDAN5C:def 3;
then ((p1`2)-c)/(d-c)/2*2<=((p2`2)-c)/(d-c)/2*2 by XREAL_1:64;
then ((p1`2)-c)/(d-c)*(d-c)<= ((p2`2)-c)/(d-c)*(d-c) by A22,XREAL_1:64;
then ((p1`2)-c)<= ((p2`2)-c)/(d-c)*(d-c) by A22,XCMPLX_1:87;
then ((p1`2)-c)<= ((p2`2)-c) by A22,XCMPLX_1:87;
then ((p1`2)-c)+c <= ((p2`2)-c)+c by XREAL_1:7;
hence thesis;
end;
thus p1`2<=p2`2 implies LE p1,p2,K
proof
assume
A25: p1`2<=p2`2;
for g being Function of I[01], (TOP-REAL 2)|Upper_Arc(K),
s1, s2 being Real st g is being_homeomorphism & g.0 = W-min(K) &
g.1 = E-max(K)
& g.s1 = p1 & 0 <= s1 & s1 <= 1 & g.s2 = p2 & 0 <= s2 & s2 <= 1
holds s1 <= s2
proof
let g be Function of I[01], (TOP-REAL 2)|Upper_Arc(K),
s1, s2 be Real;
assume that
A26: g is being_homeomorphism and
A27: g.0 = W-min(K) and g.1 = E-max(K) and
A28: g.s1 = p1 and
A29: 0 <= s1 and
A30: s1 <= 1 and
A31: g.s2 = p2 and
A32: 0 <= s2 and
A33: s2 <= 1;
A34: dom g=the carrier of I[01] by FUNCT_2:def 1;
A35: g is one-to-one by A26,TOPS_2:def 5;
A36: the
carrier of ((TOP-REAL 2)|Upper_Arc(K)) =Upper_Arc(K) by PRE_TOPC:8;
then reconsider g1=g as Function of I[01],TOP-REAL 2 by FUNCT_2:7;
g is continuous by A26,TOPS_2:def 5;
then
A37: g1 is continuous by PRE_TOPC:26;
reconsider h1=proj1 as Function of TOP-REAL 2,R^1 by TOPMETR:17;
reconsider h2=proj2 as Function of TOP-REAL 2,R^1 by TOPMETR:17;
reconsider hh1=h1 as Function of the TopStruct of TOP-REAL 2,R^1;
reconsider hh2=h2 as Function of the TopStruct of TOP-REAL 2,R^1;
A38: the TopStruct of TOP-REAL 2
= (the TopStruct of TOP-REAL 2)|([#](the TopStruct of TOP-REAL 2))
by TSEP_1:3
.= the TopStruct of ((TOP-REAL 2)|([#](TOP-REAL 2))) by PRE_TOPC:36
.= (TOP-REAL 2)|([#](TOP-REAL 2));
then (for p being Point of (TOP-REAL 2)|([#](TOP-REAL 2)) holds
hh1.p=proj1.p) implies hh1 is continuous by JGRAPH_2:29;
then
A39: (for p being Point of (TOP-REAL 2)|([#]TOP-REAL 2)holds
hh1.p=proj1.p) implies h1 is continuous by PRE_TOPC:32;
(for p being Point of (TOP-REAL 2)|([#](TOP-REAL 2)) holds
hh2.p=proj2.p) implies hh2 is continuous by A38,JGRAPH_2:30;
then (for p being Point of (TOP-REAL 2)|([#](TOP-REAL 2)) holds
hh2.p=proj2.p) implies h2 is continuous by PRE_TOPC:32;
then consider h being Function of TOP-REAL 2,R^1 such that
A40: for p being Point of TOP-REAL 2, r1,r2 being Real st hh1.p=r1 &
hh2.p=r2 holds h.p=r1+r2 and
A41: h is continuous by A39,JGRAPH_2:19;
reconsider k=h*g1 as Function of I[01],R^1;
A42: W-min K=|[a,c]| by A1,A2,Th46;
now
assume
A43: s1>s2;
A44: dom g=[.0,1.] by BORSUK_1:40,FUNCT_2:def 1;
0 in [.0,1.] by XXREAL_1:1;
then
A45: k.0=h.(W-min(K)) by A27,A44,FUNCT_1:13
.=h1.(W-min(K))+h2.(W-min(K)) by A40
.=(W-min(K))`1+proj2.(W-min(K)) by PSCOMP_1:def 5
.=(W-min(K))`1+(W-min(K))`2 by PSCOMP_1:def 6
.=a+(W-min(K))`2 by A42,EUCLID:52
.=a+c by A42,EUCLID:52;
s1 in [.0,1.] by A29,A30,XXREAL_1:1;
then
A46: k.s1=h.p1 by A28,A44,FUNCT_1:13
.=h1.p1+h2.p1 by A40
.=p1`1+proj2.p1 by PSCOMP_1:def 5
.=a+p1`2 by A6,PSCOMP_1:def 6;
A47: s2 in [.0,1.] by A32,A33,XXREAL_1:1;
then
A48: k.s2=h.p2 by A31,A44,FUNCT_1:13
.=h1.p2+h2.p2 by A40
.=p2`1+proj2.p2 by PSCOMP_1:def 5
.=a+p2`2 by A8,PSCOMP_1:def 6;
A49: k.0<=k.s1 by A7,A45,A46,XREAL_1:7;
A50: k.s1<=k.s2 by A25,A46,A48,XREAL_1:7;
A51: 0 in [.0,1.] by XXREAL_1:1;
then
A52: [.0,s2.] c= [.0,1.] by A47,XXREAL_2:def 12;
reconsider B=[.0,s2.] as Subset of I[01] by A47,A51,BORSUK_1:40
,XXREAL_2:def 12;
A53: B is connected by A32,A47,A51,BORSUK_1:40,BORSUK_4:24;
A54: 0 in B by A32,XXREAL_1:1;
A55: s2 in B by A32,XXREAL_1:1;
consider xc being Point of I[01] such that
A56: xc in B and
A57: k.xc =k.s1 by A37,A41,A49,A50,A53,A54,A55,TOPREAL5:5;
reconsider rxc=xc as Real;
A58: for x1,x2 being set st x1 in dom k & x2 in dom k &
k.x1=k.x2 holds x1=x2
proof
let x1,x2 be set;
assume that
A59: x1 in dom k and
A60: x2 in dom k and
A61: k.x1=k.x2;
reconsider r1=x1 as Point of I[01] by A59;
reconsider r2=x2 as Point of I[01] by A60;
A62: k.x1=h.(g1.x1) by A59,FUNCT_1:12
.=h1.(g1.r1)+h2.(g1.r1) by A40
.=(g1.r1)`1+proj2.(g1.r1) by PSCOMP_1:def 5
.=(g1.r1)`1+(g1.r1)`2 by PSCOMP_1:def 6;
A63: k.x2=h.(g1.x2) by A60,FUNCT_1:12
.=h1.(g1.r2)+h2.(g1.r2) by A40
.=(g1.r2)`1+proj2.(g1.r2) by PSCOMP_1:def 5
.=(g1.r2)`1+(g1.r2)`2 by PSCOMP_1:def 6;
A64: g.r1 in Upper_Arc(K) by A36;
A65: g.r2 in Upper_Arc(K) by A36;
reconsider gr1=g.r1 as Point of TOP-REAL 2 by A64;
reconsider gr2=g.r2 as Point of TOP-REAL 2 by A65;
now per cases by A10,A36,XBOOLE_0:def 3;
case
A66: g
.r1 in LSeg(|[a,c]|,|[a,d]|) & g.r2 in LSeg(|[a,c]|,|[a,d]|);
then
A67: (gr1)`1=a by A2,Th1;
(gr2)`1=a by A2,A66,Th1;
then |[(gr1)`1,(gr1)`2]|=g.r2 by A61,A62,A63,A67,EUCLID:53;
then g.r1=g.r2 by EUCLID:53;
hence thesis by A34,A35,FUNCT_1:def 4;
end;
case
A68: g
.r1 in LSeg(|[a,c]|,|[a,d]|) & g.r2 in LSeg(|[a,d]|,|[b,d]|);
then
A69: (gr1)`1=a by A2,Th1;
A70: (gr1)`2 <=d by A2,A68,Th1;
A71: (gr2)`2=d by A1,A68,Th3;
A72: a <=(gr2)`1 by A1,A68,Th3;
A73: a+(gr1)`2=(gr2)`1 +d by A1,A61,A62,A63,A68,A69,Th3;
A74: now
assume a<>gr2`1;
then a**