:: On Some Points of a Simple Closed Curve
:: by Artur Korni{\l}owicz
::
:: Received October 6, 2004
:: Copyright (c) 2004-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies TOPREAL2, SUBSET_1, EUCLID, PRE_TOPC, NUMBERS, RELAT_1, STRUCT_0,
FUNCT_1, XBOOLE_0, JORDAN2C, XXREAL_2, REAL_1, ARYTM_3, CONVEX1, MCART_1,
RLTOPSP1, ARYTM_1, CARD_1, XXREAL_0, TOPREAL1, TARSKI, JORDAN6, PSCOMP_1,
RCOMP_1, RELAT_2, SPPOL_1, JORDAN3, JORDAN21, SEQ_4;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, XXREAL_0,
XCMPLX_0, REAL_1, FUNCT_1, RELSET_1, SEQ_4, DOMAIN_1, XXREAL_2, STRUCT_0,
PRE_TOPC, COMPTS_1, CONNSP_1, TBSP_1, RCOMP_1, PSCOMP_1, RLVECT_1,
RLTOPSP1, EUCLID, TOPREAL1, TOPREAL2, JORDAN2C, SPPOL_1, JORDAN6,
JORDAN5C;
constructors REAL_1, RCOMP_1, CONNSP_1, COMPTS_1, TBSP_1, TOPREAL1, SPPOL_1,
PSCOMP_1, JORDAN5C, JORDAN6, JORDAN2C, SEQ_4, CONVEX1, BINOP_2, TOPMETR,
COMPLEX1;
registrations XBOOLE_0, RELSET_1, NUMBERS, XREAL_0, MEMBERED, STRUCT_0,
COMPTS_1, EUCLID, TOPREAL1, TOPREAL2, TOPREAL5, JORDAN6, TOPREAL6,
RLTOPSP1, JORDAN2C;
requirements SUBSET, BOOLE, NUMERALS, ARITHM;
definitions TARSKI, XBOOLE_0, JORDAN1;
equalities RLTOPSP1, PSCOMP_1, SUBSET_1;
expansions TARSKI, XBOOLE_0;
theorems XBOOLE_1, JORDAN6, XBOOLE_0, EUCLID, TOPREAL1, BORSUK_4, TARSKI,
TOPREAL5, JORDAN16, JORDAN7, JGRAPH_1, TBSP_1, JORDAN2C, PSCOMP_1,
SPRECT_1, JORDAN5B, SPPOL_1, TOPREAL3, SEQ_4, FUNCT_2, RELAT_1, TOPS_1,
RCOMP_1, JCT_MISC, XREAL_1, TOPREAL6, XXREAL_0, XXREAL_2, RLTOPSP1;
begin :: On the Subsets of TOP-REAL 2
reserve C for Simple_closed_curve,
P for Subset of TOP-REAL 2,
p for Point of TOP-REAL 2,
n for Element of NAT;
Lm1: dom proj2 = the carrier of TOP-REAL 2 by FUNCT_2:def 1;
Lm2: for r being Real, X being Subset of TOP-REAL 2 st r in proj2.:X ex
x being Point of TOP-REAL 2 st x in X & proj2.x = r
proof
let r be Real, X be Subset of TOP-REAL 2;
assume r in proj2.:X;
then
ex x being object st x in the carrier of TOP-REAL 2 & x in X & proj2.x = r
by FUNCT_2:64;
hence thesis;
end;
Lm3: now
let a,A,B,C be set;
assume a in A \/ B \/ C;
then a in A \/ B or a in C by XBOOLE_0:def 3;
hence a in A or a in B or a in C by XBOOLE_0:def 3;
end;
Lm4: for A,B,C,D being set st A misses D & B misses D & C misses D holds A \/
B \/ C misses D
proof
let A,B,C,D be set;
assume A misses D & B misses D;
then
A1: A \/ B misses D by XBOOLE_1:70;
assume C misses D;
hence thesis by A1,XBOOLE_1:70;
end;
theorem
for p being Point of TOP-REAL n holds {p} is bounded
proof
let p be Point of TOP-REAL n;
reconsider a = p as Point of Euclid n by EUCLID:67;
{a} is bounded by TBSP_1:15;
hence thesis by JORDAN2C:11;
end;
theorem Th2: :: P is an open east halfline
for s1,t being Real, P being Subset of TOP-REAL 2 st P = {
|[ s,t ]| where s is Real: s1 < s } holds P is convex
proof
let s1,t be Real, P be Subset of TOP-REAL 2;
assume
A1: P = { |[ s,t ]| where s is Real: s1<s };
let w1,w2 be Point of TOP-REAL 2 such that
A2: w1 in P and
A3: w2 in P;
consider s3 being Real such that
A4: |[ s3,t ]|=w1 and
A5: s1<s3 by A1,A2;
consider s4 being Real such that
A6: |[ s4,t ]|=w2 and
A7: s1<s4 by A1,A3;
A8: w2`1=s4 by A6,EUCLID:52;
let x be object;
assume x in LSeg(w1,w2);
then consider l being Real such that
A9: x = (1-l)*w1 + l*w2 and
A10: 0 <= l & l <= 1;
set w = (1-l)*w1 + l*w2;
A11: w = |[((1-l)*w1)`1+(l*w2)`1,((1-l)*w1)`2+ (l*w2)`2]| by EUCLID:55;
A12: l*w2=|[ l*w2`1 ,l*w2`2 ]| by EUCLID:57;
then
A13: (l*w2)`1=l*w2`1 by EUCLID:52;
A14: (1-l)*w1=|[ (1-l)*w1`1 ,(1-l)*w1`2 ]| by EUCLID:57;
then ((1-l)*w1)`1= (1-l)*w1`1 by EUCLID:52;
then
A15: w`1=(1-l)* w1`1+ l* w2`1 by A11,A13,EUCLID:52;
A16: (l*w2)`2=l*w2`2 by A12,EUCLID:52;
((1-l)*w1)`2= (1-l)*w1`2 by A14,EUCLID:52;
then
A17: w`2=(1-l)* w1`2+ l* w2`2 by A11,A16,EUCLID:52;
w2`2=t by A6,EUCLID:52;
then
A18: w`2 = (1-l)*t + l*t by A4,A17,EUCLID:52
.= t - 0;
A19: w = |[w`1, w`2]| by EUCLID:53;
w1`1=s3 by A4,EUCLID:52;
then s1 < w`1 by A5,A7,A8,A10,A15,XREAL_1:175;
hence thesis by A1,A9,A19,A18;
end;
theorem Th3: :: P is an open west halfline
for s2,t being Real, P being Subset of TOP-REAL 2 st P = {
|[ s,t ]| where s is Real : s < s2 } holds P is convex
proof
let s2,t be Real, P be Subset of TOP-REAL 2;
assume
A1: P = { |[ s,t ]| where s is Real: s<s2 };
let w1,w2 be Point of TOP-REAL 2 such that
A2: w1 in P and
A3: w2 in P;
consider s3 being Real such that
A4: |[ s3,t ]|=w1 and
A5: s3<s2 by A1,A2;
consider s4 being Real such that
A6: |[ s4,t ]|=w2 and
A7: s4<s2 by A1,A3;
A8: w2`1=s4 by A6,EUCLID:52;
let x be object;
assume x in LSeg(w1,w2);
then consider l being Real such that
A9: x = (1-l)*w1 + l*w2 and
A10: 0 <= l & l <= 1;
set w = (1-l)*w1 + l*w2;
A11: w = |[((1-l)*w1)`1+(l*w2)`1,((1-l)*w1)`2+ (l*w2)`2]| by EUCLID:55;
A12: l*w2=|[ l*w2`1 ,l*w2`2 ]| by EUCLID:57;
then
A13: (l*w2)`1=l*w2`1 by EUCLID:52;
A14: (1-l)*w1=|[ (1-l)*w1`1 ,(1-l)*w1`2 ]| by EUCLID:57;
then ((1-l)*w1)`1= (1-l)*w1`1 by EUCLID:52;
then
A15: w`1=(1-l)* w1`1+ l* w2`1 by A11,A13,EUCLID:52;
A16: (l*w2)`2=l*w2`2 by A12,EUCLID:52;
((1-l)*w1)`2= (1-l)*w1`2 by A14,EUCLID:52;
then
A17: w`2=(1-l)* w1`2+ l* w2`2 by A11,A16,EUCLID:52;
w2`2=t by A6,EUCLID:52;
then
A18: w`2 = (1-l)*t + l*t by A4,A17,EUCLID:52
.= t - 0;
A19: w = |[w`1, w`2]| by EUCLID:53;
w1`1=s3 by A4,EUCLID:52;
then s2 > w`1 by A5,A7,A8,A10,A15,XREAL_1:176;
hence thesis by A1,A9,A19,A18;
end;
theorem Th4: :: P is an open north halfline
for s,t1 being Real, P being Subset of TOP-REAL 2 st P = {
|[ s,t ]| where t is Real : t1 < t } holds P is convex
proof
let s,t1 be Real, P be Subset of TOP-REAL 2;
assume
A1: P = { |[ s,t ]| where t is Real : t1<t };
let w1,w2 be Point of TOP-REAL 2 such that
A2: w1 in P and
A3: w2 in P;
consider t3 being Real such that
A4: |[ s,t3 ]|=w1 and
A5: t1<t3 by A1,A2;
A6: w1`1=s by A4,EUCLID:52;
let x be object;
assume x in LSeg(w1,w2);
then consider l being Real such that
A7: x = (1-l)*w1 + l*w2 and
A8: 0 <= l & l <= 1;
set w = (1-l)*w1 + l*w2;
A9: w = |[((1-l)*w1)`1+(l*w2)`1,((1-l)*w1)`2+ (l*w2)`2]| by EUCLID:55;
consider t4 being Real such that
A10: |[ s,t4 ]|=w2 and
A11: t1<t4 by A1,A3;
A12: w2`1=s by A10,EUCLID:52;
A13: l*w2=|[ l*w2`1 ,l*w2`2 ]| by EUCLID:57;
then
A14: (l*w2)`1=l*w2`1 by EUCLID:52;
A15: (l*w2)`2=l*w2`2 by A13,EUCLID:52;
A16: (1-l)*w1=|[ (1-l)*w1`1 ,(1-l)*w1`2 ]| by EUCLID:57;
then ((1-l)*w1)`2= (1-l)*w1`2 by EUCLID:52;
then
A17: w`2=(1-l)* w1`2+ l* w2`2 by A9,A15,EUCLID:52;
A18: w2`2=t4 by A10,EUCLID:52;
((1-l)*w1)`1= (1-l)*w1`1 by A16,EUCLID:52;
then
A19: w = |[w`1, w`2]| & w`1 = s - 0 by A6,A12,A9,A14,EUCLID:52,53;
w1`2=t3 by A4,EUCLID:52;
then t1 < w`2 by A5,A11,A18,A8,A17,XREAL_1:175;
hence thesis by A1,A7,A19;
end;
theorem Th5: :: P is an open south halfline
for s,t2 being Real, P being Subset of TOP-REAL 2 st P = {
|[ s,t ]| where t is Real : t < t2 } holds P is convex
proof
let s,t2 be Real, P be Subset of TOP-REAL 2;
assume
A1: P = { |[ s,t ]| where t is Real: t<t2 };
let w1,w2 be Point of TOP-REAL 2 such that
A2: w1 in P and
A3: w2 in P;
consider t3 being Real such that
A4: |[ s,t3 ]|=w1 and
A5: t3<t2 by A1,A2;
consider t4 being Real such that
A6: |[ s,t4 ]|=w2 and
A7: t4<t2 by A1,A3;
A8: w2`2=t4 by A6,EUCLID:52;
let x be object;
assume x in LSeg(w1,w2);
then consider l being Real such that
A9: x = (1-l)*w1 + l*w2 and
A10: 0 <= l & l <= 1;
set w = (1-l)*w1 + l*w2;
A11: w = |[((1-l)*w1)`1+(l*w2)`1,((1-l)*w1)`2+ (l*w2)`2]| by EUCLID:55;
A12: l*w2=|[ l*w2`1 ,l*w2`2 ]| by EUCLID:57;
then
A13: (l*w2)`1=l*w2`1 by EUCLID:52;
A14: (1-l)*w1=|[ (1-l)*w1`1 ,(1-l)*w1`2 ]| by EUCLID:57;
then ((1-l)*w1)`1= (1-l)*w1`1 by EUCLID:52;
then
A15: w`1=(1-l)* w1`1+ l* w2`1 by A11,A13,EUCLID:52;
w2`1=s by A6,EUCLID:52;
then
A16: w`1 = (1-l)*s + l*s by A4,A15,EUCLID:52
.= s - 0;
A17: w = |[w`1, w`2]| by EUCLID:53;
A18: (l*w2)`2=l*w2`2 by A12,EUCLID:52;
((1-l)*w1)`2= (1-l)*w1`2 by A14,EUCLID:52;
then
A19: w`2=(1-l)* w1`2+ l* w2`2 by A11,A18,EUCLID:52;
w1`2=t3 by A4,EUCLID:52;
then t2 > w`2 by A5,A7,A8,A10,A19,XREAL_1:176;
hence thesis by A1,A9,A17,A16;
end;
theorem
north_halfline p \ {p} is convex
proof
set P = north_halfline p \ {p};
P = {|[ p`1,r ]| where r is Real: r > p`2 }
proof
hereby
let x be object;
assume
A1: x in P;
then reconsider y = x as Point of TOP-REAL 2;
A2: x in north_halfline p by A1,XBOOLE_0:def 5;
then
A3: y`1 = p`1 by TOPREAL1:def 10;
then
A4: x = |[ p`1,y`2 ]| by EUCLID:53;
A5: not x in {p} by A1,XBOOLE_0:def 5;
A6: now
assume y`2 = p`2;
then x = p by A3,TOPREAL3:6;
hence contradiction by A5,TARSKI:def 1;
end;
y`2 >= p`2 by A2,TOPREAL1:def 10;
then y`2 > p`2 by A6,XXREAL_0:1;
hence x in {|[ p`1,r ]| where r is Real : r > p`2} by A4;
end;
let x be object;
assume x in {|[ p`1,r ]| where r is Real : r > p`2 };
then consider r being Real such that
A7: x = |[ p`1,r ]| and
A8: r > p`2;
reconsider y = x as Point of TOP-REAL 2 by A7;
A9: y`2 = r by A7,EUCLID:52;
then
A10: not x in {p} by A8,TARSKI:def 1;
y`1 = p`1 by A7,EUCLID:52;
then x in north_halfline p by A8,A9,TOPREAL1:def 10;
hence thesis by A10,XBOOLE_0:def 5;
end;
hence thesis by Th4;
end;
theorem
south_halfline p \ {p} is convex
proof
set P = south_halfline p \ {p};
P = {|[ p`1,r ]| where r is Real: r < p`2 }
proof
hereby
let x be object;
assume
A1: x in P;
then reconsider y = x as Point of TOP-REAL 2;
A2: x in south_halfline p by A1,XBOOLE_0:def 5;
then
A3: y`1 = p`1 by TOPREAL1:def 12;
then
A4: x = |[ p`1,y`2 ]| by EUCLID:53;
A5: not x in {p} by A1,XBOOLE_0:def 5;
A6: now
assume y`2 = p`2;
then x = p by A3,TOPREAL3:6;
hence contradiction by A5,TARSKI:def 1;
end;
y`2 <= p`2 by A2,TOPREAL1:def 12;
then y`2 < p`2 by A6,XXREAL_0:1;
hence x in {|[ p`1,r ]| where r is Real : r < p`2} by A4;
end;
let x be object;
assume x in {|[ p`1,r ]| where r is Real : r < p`2 };
then consider r being Real such that
A7: x = |[ p`1,r ]| and
A8: r < p`2;
reconsider y = x as Point of TOP-REAL 2 by A7;
A9: y`2 = r by A7,EUCLID:52;
then
A10: not x in {p} by A8,TARSKI:def 1;
y`1 = p`1 by A7,EUCLID:52;
then x in south_halfline p by A8,A9,TOPREAL1:def 12;
hence thesis by A10,XBOOLE_0:def 5;
end;
hence thesis by Th5;
end;
theorem
west_halfline p \ {p} is convex
proof
set P = west_halfline p \ {p};
P = {|[ r,p`2 ]| where r is Real : r < p`1 }
proof
hereby
let x be object;
assume
A1: x in P;
then reconsider y = x as Point of TOP-REAL 2;
A2: x in west_halfline p by A1,XBOOLE_0:def 5;
then
A3: y`2 = p`2 by TOPREAL1:def 13;
then
A4: x = |[ y`1,p`2 ]| by EUCLID:53;
A5: not x in {p} by A1,XBOOLE_0:def 5;
A6: now
assume y`1 = p`1;
then x = p by A3,TOPREAL3:6;
hence contradiction by A5,TARSKI:def 1;
end;
y`1 <= p`1 by A2,TOPREAL1:def 13;
then y`1 < p`1 by A6,XXREAL_0:1;
hence x in {|[ r,p`2 ]| where r is Real : r < p`1} by A4;
end;
let x be object;
assume x in {|[ r,p`2 ]| where r is Real : r < p`1 };
then consider r being Real such that
A7: x = |[ r,p`2 ]| and
A8: r < p`1;
reconsider y = x as Point of TOP-REAL 2 by A7;
A9: y`1 = r by A7,EUCLID:52;
then
A10: not x in {p} by A8,TARSKI:def 1;
y`2 = p`2 by A7,EUCLID:52;
then x in west_halfline p by A8,A9,TOPREAL1:def 13;
hence thesis by A10,XBOOLE_0:def 5;
end;
hence thesis by Th3;
end;
theorem
east_halfline p \ {p} is convex
proof
set P = east_halfline p \ {p};
P = {|[ r,p`2 ]| where r is Real : r > p`1 }
proof
hereby
let x be object;
assume
A1: x in P;
then reconsider y = x as Point of TOP-REAL 2;
A2: x in east_halfline p by A1,XBOOLE_0:def 5;
then
A3: y`2 = p`2 by TOPREAL1:def 11;
then
A4: x = |[ y`1,p`2 ]| by EUCLID:53;
A5: not x in {p} by A1,XBOOLE_0:def 5;
A6: now
assume y`1 = p`1;
then x = p by A3,TOPREAL3:6;
hence contradiction by A5,TARSKI:def 1;
end;
y`1 >= p`1 by A2,TOPREAL1:def 11;
then y`1 > p`1 by A6,XXREAL_0:1;
hence x in {|[ r,p`2 ]| where r is Real : r > p`1} by A4;
end;
let x be object;
assume x in {|[ r,p`2 ]| where r is Real : r > p`1 };
then consider r being Real such that
A7: x = |[ r,p`2 ]| and
A8: r > p`1;
reconsider y = x as Point of TOP-REAL 2 by A7;
A9: y`1 = r by A7,EUCLID:52;
then
A10: not x in {p} by A8,TARSKI:def 1;
y`2 = p`2 by A7,EUCLID:52;
then x in east_halfline p by A8,A9,TOPREAL1:def 11;
hence thesis by A10,XBOOLE_0:def 5;
end;
hence thesis by Th2;
end;
theorem
for A being Subset of the carrier of TOP-REAL 2 holds UBD A misses A
proof
let A be Subset of the carrier of TOP-REAL 2;
UBD A c= A` by JORDAN2C:26;
hence thesis by XBOOLE_1:63,79;
end;
theorem Th11:
for P being Subset of the carrier of TOP-REAL 2, p1,p2,q1,q2
being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 & p1 <> q1 & p2 <> q2 holds
not p1 in Segment(P,p1,p2,q1,q2) & not p2 in Segment(P,p1,p2,q1,q2)
proof
let P be Subset of the carrier of TOP-REAL 2, p1,p2,q1,q2 be Point of
TOP-REAL 2;
assume P is_an_arc_of p1,p2 & p1 <> q1 & p2 <> q2;
then
A1: ( not p2 in L_Segment(P,p1,p2,q2))& not p1 in R_Segment(P,p1,p2,q1) by
JORDAN6:59,60;
Segment(P,p1,p2,q1,q2) = R_Segment(P,p1,p2,q1) /\ L_Segment(P,p1,p2,q2)
by JORDAN6:def 5;
hence thesis by A1,XBOOLE_0:def 4;
end;
definition
let D be Subset of TOP-REAL 2;
attr D is with_the_max_arc means
:Def1:
D meets Vertical_Line((W-bound D+ E-bound D)/2);
end;
registration
cluster with_the_max_arc -> non empty for Subset of TOP-REAL 2;
coherence
proof
let D be Subset of TOP-REAL 2;
assume D meets Vertical_Line((W-bound D+E-bound D)/2);
hence thesis;
end;
end;
registration
cluster -> with_the_max_arc for Simple_closed_curve;
coherence
proof
let C be Simple_closed_curve;
(Upper_Middle_Point C)`1 = (W-bound C+E-bound C)/2 by JORDAN6:65;
then Upper_Middle_Point C in C & Upper_Middle_Point C in Vertical_Line((
W-bound C +E-bound C)/2) by JORDAN6:31,68;
hence C meets Vertical_Line((W-bound C+E-bound C)/2) by XBOOLE_0:3;
end;
end;
registration
cluster non empty for Simple_closed_curve;
existence
proof
set A = the Simple_closed_curve;
take A;
thus thesis;
end;
end;
reserve D for compact with_the_max_arc Subset of TOP-REAL 2;
theorem Th12:
for D being with_the_max_arc Subset of TOP-REAL 2 holds proj2.:(
D /\ Vertical_Line((W-bound D + E-bound D) / 2)) is not empty
proof
let D be with_the_max_arc Subset of TOP-REAL 2;
set w = (W-bound D + E-bound D) / 2;
D meets Vertical_Line w by Def1;
then D /\ Vertical_Line w is non empty;
hence thesis by Lm1,RELAT_1:119;
end;
theorem Th13:
for C being compact Subset of TOP-REAL 2 holds proj2.:(C /\
Vertical_Line((W-bound C + E-bound C) / 2)) is closed bounded_below
bounded_above
proof
let C be compact Subset of TOP-REAL 2;
set w = (W-bound C + E-bound C) / 2;
set X = C /\ Vertical_Line w;
Vertical_Line w is closed by JORDAN6:30;
then
A1: X is closed by TOPS_1:8;
X is bounded by RLTOPSP1:42,XBOOLE_1:17;
hence proj2.:X is closed by A1,JCT_MISC:13;
X c= C by XBOOLE_1:17;
then proj2.:X is real-bounded by JCT_MISC:14,RLTOPSP1:42;
hence thesis by XXREAL_2:def 11;
end;
begin :: Middle Points
theorem Th14:
Lower_Middle_Point C in C
proof
Lower_Middle_Point C in Lower_Arc C & Lower_Arc C c= C by JORDAN6:61,66;
hence thesis;
end;
theorem Th15:
(Lower_Middle_Point C)`2 <> (Upper_Middle_Point C)`2
proof
set l = Lower_Middle_Point C, u = Upper_Middle_Point C, w = (W-bound C+
E-bound C)/2;
A1: l`1 = w by JORDAN6:64;
A2: u`1 = w by JORDAN6:65;
assume l`2 = u`2;
then l = u by A1,A2,TOPREAL3:6;
then l in Lower_Arc C & l in Upper_Arc C by JORDAN6:66,67;
then l in Lower_Arc C /\ Upper_Arc C by XBOOLE_0:def 4;
then l in {W-min(C),E-max(C)} by JORDAN6:def 9;
then l = W-min(C) or l = E-max(C) by TARSKI:def 2;
then W-bound C = w or E-bound C = w by A1,EUCLID:52;
hence thesis by SPRECT_1:31;
end;
theorem
Lower_Middle_Point C <> Upper_Middle_Point C
proof
(Lower_Middle_Point C)`2 <> (Upper_Middle_Point C)`2 by Th15;
hence thesis;
end;
begin :: Upper_Arc and Lower_Arc
theorem Th17:
W-bound C = W-bound Upper_Arc C
proof
A1: W-bound Upper_Arc C <= W-bound C
proof
A2: (W-min C)`1 = W-bound C by EUCLID:52;
assume
A3: W-bound Upper_Arc C > W-bound C;
A4: west_halfline W-min C misses Upper_Arc C
proof
assume west_halfline W-min C meets Upper_Arc C;
then consider p being object such that
A5: p in west_halfline W-min C and
A6: p in Upper_Arc C by XBOOLE_0:3;
reconsider p as Point of TOP-REAL 2 by A5;
p`1 >= W-bound Upper_Arc C by A6,PSCOMP_1:24;
then W-bound C < p`1 by A3,XXREAL_0:2;
hence contradiction by A2,A5,TOPREAL1:def 13;
end;
W-min C in west_halfline W-min C & W-min C in Upper_Arc C by JORDAN7:1
,TOPREAL1:38;
hence contradiction by A4,XBOOLE_0:3;
end;
W-bound C <= W-bound Upper_Arc C by JORDAN6:61,PSCOMP_1:69;
hence thesis by A1,XXREAL_0:1;
end;
theorem Th18:
E-bound C = E-bound Upper_Arc C
proof
A1: E-bound Upper_Arc C >= E-bound C
proof
A2: (E-max C)`1 = E-bound C by EUCLID:52;
assume
A3: E-bound Upper_Arc C < E-bound C;
A4: east_halfline E-max C misses Upper_Arc C
proof
assume east_halfline E-max C meets Upper_Arc C;
then consider p being object such that
A5: p in east_halfline E-max C and
A6: p in Upper_Arc C by XBOOLE_0:3;
reconsider p as Point of TOP-REAL 2 by A5;
p`1 <= E-bound Upper_Arc C by A6,PSCOMP_1:24;
then E-bound C > p`1 by A3,XXREAL_0:2;
hence contradiction by A2,A5,TOPREAL1:def 11;
end;
E-max C in east_halfline E-max C & E-max C in Upper_Arc C by JORDAN7:1
,TOPREAL1:38;
hence contradiction by A4,XBOOLE_0:3;
end;
E-bound C >= E-bound Upper_Arc C by JORDAN6:61,PSCOMP_1:67;
hence thesis by A1,XXREAL_0:1;
end;
theorem Th19:
W-bound C = W-bound Lower_Arc C
proof
A1: W-bound Lower_Arc C <= W-bound C
proof
A2: (W-min C)`1 = W-bound C by EUCLID:52;
assume
A3: W-bound Lower_Arc C > W-bound C;
A4: west_halfline W-min C misses Lower_Arc C
proof
assume west_halfline W-min C meets Lower_Arc C;
then consider p being object such that
A5: p in west_halfline W-min C and
A6: p in Lower_Arc C by XBOOLE_0:3;
reconsider p as Point of TOP-REAL 2 by A5;
p`1 >= W-bound Lower_Arc C by A6,PSCOMP_1:24;
then W-bound C < p`1 by A3,XXREAL_0:2;
hence contradiction by A2,A5,TOPREAL1:def 13;
end;
W-min C in west_halfline W-min C & W-min C in Lower_Arc C by JORDAN7:1
,TOPREAL1:38;
hence contradiction by A4,XBOOLE_0:3;
end;
W-bound C <= W-bound Lower_Arc C by JORDAN6:61,PSCOMP_1:69;
hence thesis by A1,XXREAL_0:1;
end;
theorem Th20:
E-bound C = E-bound Lower_Arc C
proof
A1: E-bound Lower_Arc C >= E-bound C
proof
A2: (E-max C)`1 = E-bound C by EUCLID:52;
assume
A3: E-bound Lower_Arc C < E-bound C;
A4: east_halfline E-max C misses Lower_Arc C
proof
assume east_halfline E-max C meets Lower_Arc C;
then consider p being object such that
A5: p in east_halfline E-max C and
A6: p in Lower_Arc C by XBOOLE_0:3;
reconsider p as Point of TOP-REAL 2 by A5;
p`1 <= E-bound Lower_Arc C by A6,PSCOMP_1:24;
then E-bound C > p`1 by A3,XXREAL_0:2;
hence contradiction by A2,A5,TOPREAL1:def 11;
end;
E-max C in east_halfline E-max C & E-max C in Lower_Arc C by JORDAN7:1
,TOPREAL1:38;
hence contradiction by A4,XBOOLE_0:3;
end;
E-bound C >= E-bound Lower_Arc C by JORDAN6:61,PSCOMP_1:67;
hence thesis by A1,XXREAL_0:1;
end;
theorem Th21:
Upper_Arc C /\ Vertical_Line((W-bound C + E-bound C) / 2) is not
empty & proj2.:(Upper_Arc C /\ Vertical_Line((W-bound C + E-bound C) / 2)) is
not empty
proof
set w = (W-bound C + E-bound C) / 2;
A1: W-bound C < E-bound C by SPRECT_1:31;
(E-max C)`1 = E-bound C by EUCLID:52;
then
A2: w <= (E-max C)`1 by A1,XREAL_1:226;
(W-min C)`1 = W-bound C by EUCLID:52;
then Upper_Arc C is_an_arc_of W-min C,E-max C & (W-min C)`1 <= w by A1,
JORDAN6:def 8,XREAL_1:226;
then Upper_Arc C meets Vertical_Line w by A2,JORDAN6:49;
then Upper_Arc C /\ Vertical_Line w is non empty;
hence thesis by Lm1,RELAT_1:119;
end;
theorem Th22:
Lower_Arc C /\ Vertical_Line((W-bound C + E-bound C) / 2) is not
empty & proj2.:(Lower_Arc C /\ Vertical_Line((W-bound C + E-bound C) / 2)) is
not empty
proof
set w = (W-bound C + E-bound C) / 2;
A1: W-bound C < E-bound C by SPRECT_1:31;
(E-max C)`1 = E-bound C by EUCLID:52;
then
A2: w <= (E-max C)`1 by A1,XREAL_1:226;
Lower_Arc C is_an_arc_of E-max C,W-min C by JORDAN6:def 9;
then
A3: Lower_Arc C is_an_arc_of W-min C,E-max C by JORDAN5B:14;
(W-min C)`1 = W-bound C by EUCLID:52;
then (W-min C)`1 <= w by A1,XREAL_1:226;
then Lower_Arc C meets Vertical_Line w by A3,A2,JORDAN6:49;
then Lower_Arc C /\ Vertical_Line w is non empty;
hence thesis by Lm1,RELAT_1:119;
end;
theorem
for P being compact connected Subset of TOP-REAL 2 st P c= C & W-min C
in P & E-max C in P holds Upper_Arc C c= P or Lower_Arc C c= P
proof
let P be compact connected Subset of TOP-REAL 2 such that
A1: P c= C and
A2: W-min C in P and
A3: E-max C in P;
A4: now
given p being Point of TOP-REAL 2 such that
A5: P = {p};
W-min C = p & E-max C = p by A2,A3,A5,TARSKI:def 1;
hence contradiction by TOPREAL5:19;
end;
per cases by A1,A2,A4,BORSUK_4:56;
suppose
ex p1, p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2;
hence thesis by A1,A2,A3,JORDAN16:22;
end;
suppose
P = C;
hence thesis by JORDAN6:61;
end;
end;
registration
let C;
cluster Lower_Arc C -> with_the_max_arc;
coherence
proof
W-bound C = W-bound Lower_Arc C & E-bound C = E-bound Lower_Arc C by Th19
,Th20;
hence Lower_Arc C meets Vertical_Line((W-bound Lower_Arc C+E-bound
Lower_Arc C)/2) by JORDAN6:62;
end;
cluster Upper_Arc C -> with_the_max_arc;
coherence
proof
W-bound C = W-bound Upper_Arc C & E-bound C = E-bound Upper_Arc C by Th17
,Th18;
hence Upper_Arc C meets Vertical_Line((W-bound Upper_Arc C+E-bound
Upper_Arc C)/2) by JORDAN6:63;
end;
end;
begin :: UMP and LMP
definition
let P be Subset of the carrier of TOP-REAL 2;
func UMP P -> Point of TOP-REAL 2 equals
|[ (E-bound P + W-bound P) / 2 ,
upper_bound (proj2.:(P /\ Vertical_Line ((E-bound P + W-bound P) / 2))) ]|;
correctness;
func LMP P -> Point of TOP-REAL 2 equals
|[ (E-bound P + W-bound P) / 2 ,
lower_bound (proj2.:(P /\ Vertical_Line ((E-bound P + W-bound P) / 2))) ]|;
correctness;
end;
theorem Th24:
for C being non vertical compact Subset of TOP-REAL 2 holds UMP C <> W-min C
proof
let C being non vertical compact Subset of TOP-REAL 2;
A1: (W-min C)`1 = W-bound C & (UMP C)`1 = (W-bound C + E-bound C)/2 by
EUCLID:52;
assume UMP C = W-min C;
hence thesis by A1,SPRECT_1:31;
end;
theorem Th25:
for C being non vertical compact Subset of TOP-REAL 2 holds UMP C <> E-max C
proof
let C being non vertical compact Subset of TOP-REAL 2;
A1: (E-max C)`1 = E-bound C & (UMP C)`1 = (W-bound C + E-bound C)/2 by
EUCLID:52;
assume UMP C = E-max C;
hence thesis by A1,SPRECT_1:31;
end;
theorem Th26:
for C being non vertical compact Subset of TOP-REAL 2 holds LMP C <> W-min C
proof
let C being non vertical compact Subset of TOP-REAL 2;
A1: (W-min C)`1 = W-bound C & (LMP C)`1 = (W-bound C + E-bound C)/2 by
EUCLID:52;
assume LMP C = W-min C;
hence thesis by A1,SPRECT_1:31;
end;
theorem Th27:
for C being non vertical compact Subset of TOP-REAL 2 holds LMP C <> E-max C
proof
let C being non vertical compact Subset of TOP-REAL 2;
A1: (E-max C)`1 = E-bound C & (LMP C)`1 = (W-bound C + E-bound C)/2 by
EUCLID:52;
assume LMP C = E-max C;
hence thesis by A1,SPRECT_1:31;
end;
theorem
for C being compact Subset of TOP-REAL 2 st p in C /\ Vertical_Line ((
W-bound C + E-bound C) / 2) holds p`2 <= (UMP C)`2
proof
let C be compact Subset of TOP-REAL 2 such that
A1: p in C /\ Vertical_Line ((W-bound C + E-bound C) / 2);
p`2 = proj2.p by PSCOMP_1:def 6;
then
A2: p`2 in proj2.:(C /\ Vertical_Line ((E-bound C + W-bound C) / 2)) by A1,
FUNCT_2:35;
(UMP C)`2 =
upper_bound (proj2.:(C /\ Vertical_Line ((E-bound C + W-bound C) / 2
))) & proj2.:(C /\ Vertical_Line ((E-bound C + W-bound C) / 2)) is non empty
bounded_above by A1,Lm1,Th13,EUCLID:52,RELAT_1:119;
hence thesis by A2,SEQ_4:def 1;
end;
theorem
for C being compact Subset of TOP-REAL 2 st p in C /\ Vertical_Line ((
W-bound C + E-bound C) / 2) holds (LMP C)`2 <= p`2
proof
let C be compact Subset of TOP-REAL 2 such that
A1: p in C /\ Vertical_Line ((W-bound C + E-bound C) / 2);
p`2 = proj2.p by PSCOMP_1:def 6;
then
A2: p`2 in proj2.:(C /\ Vertical_Line ((E-bound C + W-bound C) / 2)) by A1,
FUNCT_2:35;
(LMP C)`2 =
lower_bound (proj2.:(C /\ Vertical_Line ((E-bound C + W-bound C) / 2
))) & proj2.:(C /\ Vertical_Line ((E-bound C + W-bound C) / 2)) is non empty
bounded_below by A1,Lm1,Th13,EUCLID:52,RELAT_1:119;
hence thesis by A2,SEQ_4:def 2;
end;
theorem Th30:
UMP D in D
proof
set w = (W-bound D + E-bound D) / 2;
set X = D /\ Vertical_Line w;
D meets Vertical_Line w by Def1;
then
A1: X is non empty;
proj2.:X is closed & proj2.:X is bounded_above by Th13;
then upper_bound (proj2.:X) in proj2.:X by A1,Lm1,RCOMP_1:12,RELAT_1:119;
then consider x being Point of TOP-REAL 2 such that
A2: x in X and
A3: upper_bound (proj2.:X) = proj2.x by Lm2;
x in Vertical_Line w by A2,XBOOLE_0:def 4;
then
A4: x`1 = w by JORDAN6:31
.= (UMP D)`1 by EUCLID:52;
x`2 = upper_bound (proj2.:X) by A3,PSCOMP_1:def 6
.= (UMP D)`2 by EUCLID:52;
then x = UMP D by A4,TOPREAL3:6;
hence thesis by A2,XBOOLE_0:def 4;
end;
theorem Th31:
LMP D in D
proof
set w = (W-bound D + E-bound D) / 2;
set X = D /\ Vertical_Line w;
A1: proj2.:X is bounded_below by Th13;
proj2.:X is non empty & proj2.:X is closed by Th12,Th13;
then consider x being Point of TOP-REAL 2 such that
A2: x in X and
A3: lower_bound (proj2.:X) = proj2.x by A1,Lm2,RCOMP_1:13;
x in Vertical_Line w by A2,XBOOLE_0:def 4;
then
A4: x`1 = w by JORDAN6:31
.= (LMP D)`1 by EUCLID:52;
x`2 = lower_bound (proj2.:X) by A3,PSCOMP_1:def 6
.= (LMP D)`2 by EUCLID:52;
then x = LMP D by A4,TOPREAL3:6;
hence thesis by A2,XBOOLE_0:def 4;
end;
theorem Th32:
LSeg(UMP P, |[ (W-bound P + E-bound P) / 2, N-bound P]|) is vertical
proof
set w = (W-bound P + E-bound P) / 2;
|[w,N-bound P]|`1 = w & (UMP P)`1 = w by EUCLID:52;
hence thesis by SPPOL_1:16;
end;
theorem Th33:
LSeg(LMP P, |[ (W-bound P + E-bound P) / 2, S-bound P]|) is vertical
proof
set w = (W-bound P + E-bound P) / 2;
|[w,S-bound P]|`1 = w & (LMP P)`1 = w by EUCLID:52;
hence thesis by SPPOL_1:16;
end;
theorem Th34:
LSeg(UMP D, |[ (W-bound D + E-bound D) / 2, N-bound D]|) /\ D = { UMP D }
proof
set C = D;
set w = (W-bound C + E-bound C) / 2;
set L = LSeg(UMP C, |[w,N-bound C]|);
set X = C /\ Vertical_Line(w);
A1: UMP C in C by Th30;
A2: UMP C in L by RLTOPSP1:68;
hereby
let x be object;
A3: (UMP C)`1 = w by EUCLID:52;
assume
A4: x in L /\ C;
then
A5: x in L by XBOOLE_0:def 4;
reconsider y = x as Point of TOP-REAL 2 by A4;
UMP C in C by Th30;
then |[w,N-bound C]|`2 = N-bound C & (UMP C)`2 <= N-bound C by EUCLID:52
,PSCOMP_1:24;
then
A6: (UMP C)`2 <= y`2 by A5,TOPREAL1:4;
A7: proj2.:X is bounded_above by Th13;
A8: (UMP C)`2 = upper_bound (proj2.:X) by EUCLID:52;
A9: x in C by A4,XBOOLE_0:def 4;
L is vertical by Th32;
then
A10: y`1 = w by A2,A5,A3,SPPOL_1:def 3;
then y in Vertical_Line (w) by JORDAN6:31;
then y`2 = proj2.y & y in X by A9,PSCOMP_1:def 6,XBOOLE_0:def 4;
then y`2 in proj2.:X by FUNCT_2:35;
then y`2 <= upper_bound (proj2.:X) by A7,SEQ_4:def 1;
then y`2 = upper_bound (proj2.:X) by A8,A6,XXREAL_0:1;
then y = UMP C by A3,A8,A10,TOPREAL3:6;
hence x in {UMP C} by TARSKI:def 1;
end;
let x be object;
assume x in {UMP C};
then x = UMP C by TARSKI:def 1;
hence thesis by A2,A1,XBOOLE_0:def 4;
end;
theorem Th35:
LSeg(LMP D, |[ (W-bound D + E-bound D) / 2, S-bound D]|) /\ D = { LMP D }
proof
set C = D;
set w = (W-bound C + E-bound C) / 2;
set L = LSeg(LMP C, |[w,S-bound C]|);
set X = C /\ Vertical_Line (w);
A1: LMP C in C by Th31;
A2: LMP C in L by RLTOPSP1:68;
hereby
let x be object;
A3: (LMP C)`1 = w by EUCLID:52;
assume
A4: x in L /\ C;
then
A5: x in L by XBOOLE_0:def 4;
reconsider y = x as Point of TOP-REAL 2 by A4;
LMP C in C by Th31;
then |[w,S-bound C]|`2 = S-bound C & (LMP C)`2 >= S-bound C by EUCLID:52
,PSCOMP_1:24;
then
A6: (LMP C)`2 >= y`2 by A5,TOPREAL1:4;
A7: proj2.:X is bounded_below by Th13;
A8: (LMP C)`2 = lower_bound (proj2.:X) by EUCLID:52;
A9: x in C by A4,XBOOLE_0:def 4;
L is vertical by Th33;
then
A10: y`1 = w by A2,A5,A3,SPPOL_1:def 3;
then y in Vertical_Line (w) by JORDAN6:31;
then y`2 = proj2.y & y in X by A9,PSCOMP_1:def 6,XBOOLE_0:def 4;
then y`2 in proj2.:X by FUNCT_2:35;
then y`2 >= lower_bound (proj2.:X) by A7,SEQ_4:def 2;
then y`2 = lower_bound (proj2.:X) by A8,A6,XXREAL_0:1;
then y = LMP C by A3,A8,A10,TOPREAL3:6;
hence x in {LMP C} by TARSKI:def 1;
end;
let x be object;
assume x in {LMP C};
then x = LMP C by TARSKI:def 1;
hence thesis by A2,A1,XBOOLE_0:def 4;
end;
theorem Th36:
(LMP C)`2 < (UMP C)`2
proof
set w = (E-bound C + W-bound C) / 2;
set X = C /\ Vertical_Line (w);
A1: (UMP C)`2 = upper_bound (proj2.:X) & (LMP C)`2 = lower_bound (proj2.:X)
by EUCLID:52;
set u = Upper_Middle_Point C, l = Lower_Middle_Point C;
A2: l`2 = proj2.l by PSCOMP_1:def 6;
l`1 = w by JORDAN6:64;
then
A3: l in Vertical_Line (w) by JORDAN6:31;
l in C by Th14;
then l in X by A3,XBOOLE_0:def 4;
then
A4: l`2 in proj2.:X by A2,FUNCT_2:35;
X is bounded by TOPREAL6:89;
then
A5: proj2.:X is real-bounded by JCT_MISC:14;
u`1 = w by JORDAN6:65;
then u in C & u in Vertical_Line (w) by JORDAN6:31,68;
then
A6: u in X by XBOOLE_0:def 4;
u`2 = proj2.u by PSCOMP_1:def 6;
then
A7: u`2 in proj2.:X by A6,FUNCT_2:35;
u`2 <> l`2 by Th15;
hence thesis by A1,A5,A7,A4,SEQ_4:12;
end;
theorem Th37:
UMP C <> LMP C
proof
assume
A1: UMP C = LMP C;
(LMP C)`2 < (UMP C)`2 by Th36;
hence contradiction by A1;
end;
theorem Th38:
S-bound C < (UMP C)`2
proof
set u = UMP C, l = LMP C;
A1: now
assume
A2: S-bound C = u`2;
l`2 < u`2 & l in C by Th31,Th36;
hence contradiction by A2,PSCOMP_1:24;
end;
u in C by Th30;
then S-bound C <= u`2 by PSCOMP_1:24;
hence thesis by A1,XXREAL_0:1;
end;
theorem Th39:
(UMP C)`2 <= N-bound C
proof
UMP C in C by Th30;
hence thesis by PSCOMP_1:24;
end;
theorem Th40:
S-bound C <= (LMP C)`2
proof
LMP C in C by Th31;
hence thesis by PSCOMP_1:24;
end;
theorem Th41:
(LMP C)`2 < N-bound C
proof
set u = UMP C, l = LMP C;
A1: now
assume
A2: N-bound C = l`2;
l`2 < u`2 & u in C by Th30,Th36;
hence contradiction by A2,PSCOMP_1:24;
end;
l in C by Th31;
then l`2 <= N-bound C by PSCOMP_1:24;
hence thesis by A1,XXREAL_0:1;
end;
theorem Th42:
LSeg(UMP C, |[ (W-bound C + E-bound C) / 2, N-bound C]|) misses
LSeg(LMP C, |[ (W-bound C + E-bound C) / 2, S-bound C]|)
proof
set w = (W-bound C + E-bound C) / 2;
assume LSeg(UMP C, |[w, N-bound C]|) meets LSeg(LMP C, |[w, S-bound C]|);
then consider x being object such that
A1: x in LSeg(UMP C, |[w, N-bound C]|) and
A2: x in LSeg(LMP C, |[w, S-bound C]|) by XBOOLE_0:3;
reconsider x as Point of TOP-REAL 2 by A1;
|[w, N-bound C]|`2 = N-bound C by EUCLID:52;
then (UMP C)`2 <= |[w, N-bound C]|`2 by Th39;
then
A3: x`2 >= (UMP C)`2 by A1,TOPREAL1:4;
|[w, S-bound C]|`2 = S-bound C by EUCLID:52;
then |[w, S-bound C]|`2 <= (LMP C)`2 by Th40;
then x`2 <= (LMP C)`2 by A2,TOPREAL1:4;
hence contradiction by A3,Th36,XXREAL_0:2;
end;
theorem
for A, B being Subset of TOP-REAL 2 st A c= B & W-bound A + E-bound A
= W-bound B + E-bound B & A /\ Vertical_Line ((W-bound A + E-bound A) / 2) is
non empty & proj2.:(B /\ Vertical_Line ((W-bound A + E-bound A) / 2)) is
bounded_above holds (UMP A)`2 <= (UMP B)`2
proof
let A, B be Subset of TOP-REAL 2;
assume that
A1: A c= B and
A2: W-bound A + E-bound A = W-bound B + E-bound B and
A3: A /\ Vertical_Line ((W-bound A + E-bound A) / 2) is non empty and
A4: proj2.:(B /\ Vertical_Line ((W-bound A + E-bound A) / 2)) is bounded_above;
set w = (W-bound A + E-bound A) / 2;
proj2.:(A /\ Vertical_Line w) is non empty & A /\ Vertical_Line w c= B
/\ Vertical_Line w by A1,A3,Lm1,RELAT_1:119,XBOOLE_1:26;
then
upper_bound(proj2.:(A /\ Vertical_Line w)) <=
upper_bound(proj2.:(B /\ Vertical_Line w))
by A4,RELAT_1:123,SEQ_4:48;
then (UMP A)`2 <= upper_bound(proj2.:(B /\ Vertical_Line w)) by EUCLID:52;
hence thesis by A2,EUCLID:52;
end;
theorem
for A, B being Subset of TOP-REAL 2 st A c= B & W-bound A + E-bound A
= W-bound B + E-bound B & A /\ Vertical_Line ((W-bound A + E-bound A) / 2) is
non empty & proj2.:(B /\ Vertical_Line ((W-bound A + E-bound A) / 2)) is
bounded_below holds (LMP B)`2 <= (LMP A)`2
proof
let A, B be Subset of TOP-REAL 2;
assume that
A1: A c= B and
A2: W-bound A + E-bound A = W-bound B + E-bound B and
A3: A /\ Vertical_Line ((W-bound A + E-bound A) / 2) is non empty and
A4: proj2.:(B /\ Vertical_Line ((W-bound A + E-bound A) / 2)) is bounded_below;
set w = (W-bound A + E-bound A) / 2;
proj2.:(A /\ Vertical_Line w) is non empty & A /\ Vertical_Line w c= B
/\ Vertical_Line w by A1,A3,Lm1,RELAT_1:119,XBOOLE_1:26;
then
lower_bound(proj2.:(A /\ Vertical_Line w)) >=
lower_bound(proj2.:(B /\ Vertical_Line w))
by A4,RELAT_1:123,SEQ_4:47;
then (LMP A)`2 >= lower_bound(proj2.:(B /\ Vertical_Line w)) by EUCLID:52;
hence thesis by A2,EUCLID:52;
end;
theorem
for A, B being Subset of TOP-REAL 2 st A c= B & UMP B in A & A /\
Vertical_Line ((W-bound A + E-bound A) / 2) is non empty & proj2.:(B /\
Vertical_Line ((W-bound B + E-bound B) / 2)) is bounded_above & W-bound A +
E-bound A = W-bound B + E-bound B holds UMP A = UMP B
proof
let A, B be Subset of TOP-REAL 2 such that
A1: A c= B and
A2: UMP B in A and
A3: A /\ Vertical_Line ((W-bound A + E-bound A) / 2) is non empty and
A4: proj2.:(B /\ Vertical_Line ((W-bound B + E-bound B) / 2)) is
bounded_above and
A5: W-bound A + E-bound A = W-bound B + E-bound B;
set w = (W-bound A + E-bound A)/2;
A6: (UMP A)`2 = upper_bound (proj2.:(A /\ Vertical_Line w)) & proj2.:(A /\
Vertical_Line w) is non empty by A3,Lm1,EUCLID:52,RELAT_1:119;
A7: (UMP B)`1 = w by A5,EUCLID:52;
A8: for s being Real st 0 < s ex r being Real st r in proj2.:
(A /\ Vertical_Line w) & (UMP B)`2 - s < r
proof
let s be Real;
assume
A9: 0 < s;
take (UMP B)`2;
UMP B in Vertical_Line w by A7,JORDAN6:31;
then proj2.UMP B = (UMP B)`2 & UMP B in A /\ Vertical_Line w by A2,
PSCOMP_1:def 6,XBOOLE_0:def 4;
hence (UMP B)`2 in proj2.:(A /\ Vertical_Line w) by FUNCT_2:35;
(UMP B)`2 - s < (UMP B)`2 - 0 by A9,XREAL_1:15;
hence thesis;
end;
A10: A /\ Vertical_Line w c= B /\ Vertical_Line w by A1,XBOOLE_1:26;
then
A11: proj2.:(A /\ Vertical_Line w) c= proj2.:(B /\ Vertical_Line w) by
RELAT_1:123;
(UMP B)`2 = upper_bound (proj2.:(B /\ Vertical_Line w)) by A5,EUCLID:52;
then
A12: for r being Real st r in proj2.:(A /\ Vertical_Line w) holds (
UMP B)`2 >= r by A4,A5,A11,SEQ_4:def 1;
proj2.:(A /\ Vertical_Line w) is bounded_above by A4,A5,A10,RELAT_1:123
,XXREAL_2:43;
then (UMP A)`1 = w & (UMP A)`2 = (UMP B)`2 by A6,A12,A8,EUCLID:52,SEQ_4:def 1
;
hence thesis by A7,TOPREAL3:6;
end;
theorem
for A, B being Subset of TOP-REAL 2 st A c= B & LMP B in A & A /\
Vertical_Line ((W-bound A + E-bound A) / 2) is non empty & proj2.:(B /\
Vertical_Line ((W-bound B + E-bound B) / 2)) is bounded_below & W-bound A +
E-bound A = W-bound B + E-bound B holds LMP A = LMP B
proof
let A, B be Subset of TOP-REAL 2 such that
A1: A c= B and
A2: LMP B in A and
A3: A /\ Vertical_Line ((W-bound A + E-bound A) / 2) is non empty and
A4: proj2.:(B /\ Vertical_Line ((W-bound B + E-bound B) / 2)) is
bounded_below and
A5: W-bound A + E-bound A = W-bound B + E-bound B;
set w = (W-bound A + E-bound A)/2;
A6: (LMP A)`2 = lower_bound (proj2.:(A /\ Vertical_Line w)) & proj2.:(A /\
Vertical_Line w) is non empty by A3,Lm1,EUCLID:52,RELAT_1:119;
A7: (LMP B)`1 = w by A5,EUCLID:52;
A8: for s being Real st 0 < s ex r being Real st r in proj2.:
(A /\ Vertical_Line w) & r < (LMP B)`2 + s
proof
let s be Real;
assume
A9: 0 < s;
take (LMP B)`2;
LMP B in Vertical_Line w by A7,JORDAN6:31;
then proj2.LMP B = (LMP B)`2 & LMP B in A /\ Vertical_Line w by A2,
PSCOMP_1:def 6,XBOOLE_0:def 4;
hence (LMP B)`2 in proj2.:(A /\ Vertical_Line w) by FUNCT_2:35;
(LMP B)`2 + 0 < (LMP B)`2 + s by A9,XREAL_1:6;
hence thesis;
end;
A10: A /\ Vertical_Line w c= B /\ Vertical_Line w by A1,XBOOLE_1:26;
then
A11: proj2.:(A /\ Vertical_Line w) c= proj2.:(B /\ Vertical_Line w) by
RELAT_1:123;
(LMP B)`2 = lower_bound (proj2.:(B /\ Vertical_Line w)) by A5,EUCLID:52;
then
A12: for r being Real st r in proj2.:(A /\ Vertical_Line w) holds (
LMP B)`2 <= r by A4,A5,A11,SEQ_4:def 2;
proj2.:(A /\ Vertical_Line w) is bounded_below by A4,A5,A10,RELAT_1:123
,XXREAL_2:44;
then (LMP A)`1 = w & (LMP A)`2 = (LMP B)`2 by A6,A12,A8,EUCLID:52,SEQ_4:def 2
;
hence thesis by A7,TOPREAL3:6;
end;
theorem
(UMP Upper_Arc C)`2 <= N-bound C
proof
set w = (E-bound C + W-bound C) / 2;
A1: Upper_Arc C /\ Vertical_Line w c= C /\ Vertical_Line w by JORDAN6:61
,XBOOLE_1:26;
proj2.:(Upper_Arc C /\ Vertical_Line w) is non empty & proj2.:(C /\
Vertical_Line w) is bounded_above by Th13,Th21;
then
A2: upper_bound(proj2.:(Upper_Arc C /\ Vertical_Line w))
<= upper_bound(proj2.:(C /\
Vertical_Line w)) by A1,RELAT_1:123,SEQ_4:48;
W-bound C = W-bound Upper_Arc C & E-bound C = E-bound Upper_Arc C by Th17
,Th18;
then
A3: (UMP Upper_Arc C)`2 = upper_bound(proj2.:(Upper_Arc C /\ Vertical_Line w))
by EUCLID:52;
(UMP C)`2 = upper_bound(proj2.:(C /\ Vertical_Line w)) & (UMP C)`2 <=
N-bound C
by Th39,EUCLID:52;
hence thesis by A2,A3,XXREAL_0:2;
end;
theorem
S-bound C <= (LMP Lower_Arc C)`2
proof
set w = (E-bound C + W-bound C) / 2;
A1: Lower_Arc C /\ Vertical_Line w c= C /\ Vertical_Line w by JORDAN6:61
,XBOOLE_1:26;
proj2.:(Lower_Arc C /\ Vertical_Line w) is non empty & proj2.:(C /\
Vertical_Line w) is bounded_below by Th13,Th22;
then
A2: lower_bound(proj2.:(Lower_Arc C /\ Vertical_Line w)) >=
lower_bound(proj2.:(C /\
Vertical_Line w)) by A1,RELAT_1:123,SEQ_4:47;
W-bound C = W-bound Lower_Arc C & E-bound C = E-bound Lower_Arc C by Th19
,Th20;
then
A3: (LMP Lower_Arc C)`2 = lower_bound(proj2.:(Lower_Arc C /\ Vertical_Line w))
by EUCLID:52;
(LMP C)`2 = lower_bound(proj2.:(C /\ Vertical_Line w)) & S-bound C
<= (LMP C)`2
by Th40,EUCLID:52;
hence thesis by A2,A3,XXREAL_0:2;
end;
theorem
not (LMP C in Lower_Arc C & UMP C in Lower_Arc C)
proof
assume that
A1: LMP C in Lower_Arc C and
A2: UMP C in Lower_Arc C;
A3: Upper_Arc(C) /\ Lower_Arc(C) = {W-min(C),E-max(C)} by JORDAN6:def 9;
set n = |[ (W-bound C + E-bound C) / 2, N-bound C ]|;
set S1 = LSeg(n, UMP C);
A4: Lower_Arc C c= C by JORDAN6:61;
A5: n`2 = N-bound C by EUCLID:52;
set s = |[ (W-bound C + E-bound C) / 2, S-bound C ]|;
set S2 = LSeg(LMP C, s);
A6: Lower_Arc C is_an_arc_of E-max C,W-min C by JORDAN6:def 9;
A7: (W-min C)`1 = W-bound C & (E-max C)`1 = E-bound C by EUCLID:52;
A8: Upper_Arc C c= C by JORDAN6:61;
then
A9: for p being Point of TOP-REAL 2 st p in Upper_Arc C holds (W-min C)`1<=
p`1 & p`1<=(E-max C)`1 by A7,PSCOMP_1:24;
A10: UMP C <> E-max C by Th25;
A11: UMP C <> W-min C by Th24;
A12: now
assume UMP C in Upper_Arc C;
then UMP C in Upper_Arc C /\ Lower_Arc C by A2,XBOOLE_0:def 4;
hence contradiction by A11,A10,A3,TARSKI:def 2;
end;
A13: W-bound C < E-bound C by SPRECT_1:31;
A14: Upper_Arc C misses S1
proof
A15: S1 /\ C = {UMP C} by Th34;
assume Upper_Arc C meets S1;
then consider x being object such that
A16: x in Upper_Arc C and
A17: x in S1 by XBOOLE_0:3;
x in S1 /\ C by A8,A16,A17,XBOOLE_0:def 4;
then
A18: x = UMP C by A15,TARSKI:def 1;
then x in Lower_Arc C /\ Upper_Arc C by A2,A16,XBOOLE_0:def 4;
hence contradiction by A11,A10,A3,A18,TARSKI:def 2;
end;
A19: UMP C in C & LMP C in C by Th30,Th31;
A20: (UMP C)`1 = (W-bound C + E-bound C)/2 by EUCLID:52;
n`1 = (W-bound C + E-bound C)/2 by EUCLID:52;
then
A21: S1 is vertical by A20,SPPOL_1:16;
A22: UMP C in S1 by RLTOPSP1:68;
A23: LMP C <> E-max C by Th27;
A24: LMP C <> W-min C by Th26;
A25: now
assume LMP C in Upper_Arc C;
then LMP C in Upper_Arc C /\ Lower_Arc C by A1,XBOOLE_0:def 4;
hence contradiction by A24,A23,A3,TARSKI:def 2;
end;
A26: LMP C <> UMP C by Th37;
A27: (LMP C)`1 = (W-bound C + E-bound C)/2 by EUCLID:52;
A28: Upper_Arc C misses S2
proof
A29: S2 /\ C = {LMP C} by Th35;
assume Upper_Arc C meets S2;
then consider x being object such that
A30: x in Upper_Arc C and
A31: x in S2 by XBOOLE_0:3;
x in S2 /\ C by A8,A30,A31,XBOOLE_0:def 4;
then
A32: x = LMP C by A29,TARSKI:def 1;
then x in Lower_Arc C /\ Upper_Arc C by A1,A30,XBOOLE_0:def 4;
hence contradiction by A24,A23,A3,A32,TARSKI:def 2;
end;
s`1 = (W-bound C + E-bound C)/2 by EUCLID:52;
then
A33: S2 is vertical by A27,SPPOL_1:16;
A34: LMP C in S2 by RLTOPSP1:68;
A35: S1 misses S2 by Th42;
A36: s`2 = S-bound C by EUCLID:52;
then
A37: Upper_Arc C is_an_arc_of W-min C,E-max C & for p being Point of
TOP-REAL 2 st p in Upper_Arc C holds s`2<=p`2 & p`2<=n`2 by A8,A5,
JORDAN6:def 8,PSCOMP_1:24;
per cases by A19,JORDAN16:7;
suppose
A38: LE LMP C, UMP C, C;
set S = Segment(Lower_Arc C, E-max C, W-min C, LMP C, UMP C);
A39: S c= Lower_Arc C by JORDAN16:2;
then
A40: S c= C by A4;
A41: now
let p be Point of TOP-REAL 2;
assume
A42: p in S1 \/ S \/ S2;
per cases by A42,Lm3;
suppose
p in S1;
then p`1 = (UMP C)`1 by A21,A22,SPPOL_1:def 3;
hence (W-min C)`1<=p`1 & p`1<=(E-max C)`1 by A20,A7,A13,XREAL_1:226;
end;
suppose
p in S;
hence (W-min C)`1<=p`1 & p`1<=(E-max C)`1 by A7,A40,PSCOMP_1:24;
end;
suppose
p in S2;
then p`1 = (LMP C)`1 by A33,A34,SPPOL_1:def 3;
hence (W-min C)`1<=p`1 & p`1<=(E-max C)`1 by A27,A7,A13,XREAL_1:226;
end;
end;
A43: now
let p be Point of TOP-REAL 2;
assume
A44: p in S1 \/ S \/ S2;
per cases by A44,Lm3;
suppose
A45: p in S1;
A46: s`2<=(UMP C)`2 by A36,Th38;
A47: (UMP C)`2<=n`2 by A5,Th39;
then (UMP C)`2<=p`2 by A45,TOPREAL1:4;
hence s`2<=p`2 & p`2<=n`2 by A45,A47,A46,TOPREAL1:4,XXREAL_0:2;
end;
suppose
p in S;
hence s`2<=p`2 & p`2<=n`2 by A36,A5,A40,PSCOMP_1:24;
end;
suppose
A48: p in S2;
A49: s`2<=(LMP C)`2 by A36,Th40;
hence s`2<=p`2 by A48,TOPREAL1:4;
p`2<=(LMP C)`2 by A48,A49,TOPREAL1:4;
hence p`2<=n`2 by A5,Th41,XXREAL_0:2;
end;
end;
A50: S c= Lower_Arc C \ {W-min C,E-max C}
proof
let s be object;
assume
A51: s in S;
now
assume s in {W-min C,E-max C};
then s = W-min C or s = E-max C by TARSKI:def 2;
hence contradiction by A11,A23,A6,A51,Th11;
end;
hence thesis by A39,A51,XBOOLE_0:def 5;
end;
Upper_Arc C misses S
proof
assume Upper_Arc C meets S;
then consider x being object such that
A52: x in Upper_Arc C and
A53: x in S by XBOOLE_0:3;
x in Lower_Arc C by A50,A53,XBOOLE_0:def 5;
then x in Lower_Arc C /\ Upper_Arc C by A52,XBOOLE_0:def 4;
hence contradiction by A3,A50,A53,XBOOLE_0:def 5;
end;
then
A54: Upper_Arc C misses S1 \/ S \/ S2 by A14,A28,Lm4;
A55: LE LMP C, UMP C, Lower_Arc C, E-max C, W-min C by A25,A38,JORDAN6:def 10;
then
A56: UMP C in S by JORDAN16:5;
A57: S1 /\ S = {UMP C}
proof
S1 /\ C = {UMP C} by Th34;
hence S1 /\ S c= {UMP C} by A40,XBOOLE_1:26;
let x be object;
assume x in {UMP C};
then
A58: x = UMP C by TARSKI:def 1;
UMP C in S1 by RLTOPSP1:68;
hence thesis by A56,A58,XBOOLE_0:def 4;
end;
A59: LMP C in S by A55,JORDAN16:5;
A60: S2 /\ S = {LMP C}
proof
S2 /\ C = {LMP C} by Th35;
hence S2 /\ S c= {LMP C} by A40,XBOOLE_1:26;
let x be object;
assume x in {LMP C};
then x = LMP C by TARSKI:def 1;
hence thesis by A34,A59,XBOOLE_0:def 4;
end;
S is_an_arc_of LMP C, UMP C by A26,A6,A55,JORDAN16:21;
then S is_an_arc_of UMP C, LMP C by JORDAN5B:14;
then
A61: S1 \/ S is_an_arc_of n,LMP C by A57,TOPREAL1:11;
(S1 \/ S) /\ S2 = S1 /\ S2 \/ S /\ S2 by XBOOLE_1:23
.= {} \/ S /\ S2 by A35;
then S1 \/ S \/ S2 is_an_arc_of n,s by A60,A61,TOPREAL1:10;
then S1 \/ S \/ S2 is_an_arc_of s,n by JORDAN5B:14;
hence thesis by A37,A9,A54,A43,A41,JGRAPH_1:44;
end;
suppose
A62: LE UMP C, LMP C, C;
set S = Segment(Lower_Arc C, E-max C, W-min C, UMP C, LMP C);
A63: S c= Lower_Arc C by JORDAN16:2;
then
A64: S c= C by A4;
A65: now
let p be Point of TOP-REAL 2;
assume
A66: p in S1 \/ S \/ S2;
per cases by A66,Lm3;
suppose
p in S1;
then p`1 = (UMP C)`1 by A21,A22,SPPOL_1:def 3;
hence (W-min C)`1<=p`1 & p`1<=(E-max C)`1 by A20,A7,A13,XREAL_1:226;
end;
suppose
p in S;
hence (W-min C)`1<=p`1 & p`1<=(E-max C)`1 by A7,A64,PSCOMP_1:24;
end;
suppose
p in S2;
then p`1 = (LMP C)`1 by A33,A34,SPPOL_1:def 3;
hence (W-min C)`1<=p`1 & p`1<=(E-max C)`1 by A27,A7,A13,XREAL_1:226;
end;
end;
A67: now
let p be Point of TOP-REAL 2;
assume
A68: p in S1 \/ S \/ S2;
per cases by A68,Lm3;
suppose
A69: p in S1;
A70: s`2<=(UMP C)`2 by A36,Th38;
A71: (UMP C)`2<=n`2 by A5,Th39;
then (UMP C)`2<=p`2 by A69,TOPREAL1:4;
hence s`2<=p`2 & p`2<=n`2 by A69,A71,A70,TOPREAL1:4,XXREAL_0:2;
end;
suppose
p in S;
hence s`2<=p`2 & p`2<=n`2 by A36,A5,A64,PSCOMP_1:24;
end;
suppose
A72: p in S2;
A73: s`2<=(LMP C)`2 by A36,Th40;
hence s`2<=p`2 by A72,TOPREAL1:4;
p`2<=(LMP C)`2 by A72,A73,TOPREAL1:4;
hence p`2<=n`2 by A5,Th41,XXREAL_0:2;
end;
end;
A74: S c= Lower_Arc C \ {W-min C,E-max C}
proof
let s be object;
assume
A75: s in S;
now
assume s in {W-min C,E-max C};
then s = W-min C or s = E-max C by TARSKI:def 2;
hence contradiction by A10,A24,A6,A75,Th11;
end;
hence thesis by A63,A75,XBOOLE_0:def 5;
end;
Upper_Arc C misses S
proof
assume Upper_Arc C meets S;
then consider x being object such that
A76: x in Upper_Arc C and
A77: x in S by XBOOLE_0:3;
x in Lower_Arc C by A74,A77,XBOOLE_0:def 5;
then x in Lower_Arc C /\ Upper_Arc C by A76,XBOOLE_0:def 4;
hence contradiction by A3,A74,A77,XBOOLE_0:def 5;
end;
then
A78: Upper_Arc C misses S1 \/ S \/ S2 by A14,A28,Lm4;
A79: LE UMP C, LMP C, Lower_Arc C, E-max C, W-min C by A12,A62,JORDAN6:def 10;
then
A80: UMP C in S by JORDAN16:5;
A81: S1 /\ S = {UMP C}
proof
S1 /\ C = {UMP C} by Th34;
hence S1 /\ S c= {UMP C} by A64,XBOOLE_1:26;
let x be object;
assume x in {UMP C};
then
A82: x = UMP C by TARSKI:def 1;
UMP C in S1 by RLTOPSP1:68;
hence thesis by A80,A82,XBOOLE_0:def 4;
end;
A83: LMP C in S by A79,JORDAN16:5;
A84: S2 /\ S = {LMP C}
proof
S2 /\ C = {LMP C} by Th35;
hence S2 /\ S c= {LMP C} by A64,XBOOLE_1:26;
let x be object;
assume x in {LMP C};
then x = LMP C by TARSKI:def 1;
hence thesis by A34,A83,XBOOLE_0:def 4;
end;
S is_an_arc_of UMP C, LMP C by A6,A79,Th37,JORDAN16:21;
then
A85: S1 \/ S is_an_arc_of n,LMP C by A81,TOPREAL1:11;
(S1 \/ S) /\ S2 = S1 /\ S2 \/ S /\ S2 by XBOOLE_1:23
.= {} \/ S /\ S2 by A35;
then S1 \/ S \/ S2 is_an_arc_of n,s by A84,A85,TOPREAL1:10;
then S1 \/ S \/ S2 is_an_arc_of s,n by JORDAN5B:14;
hence thesis by A37,A9,A78,A67,A65,JGRAPH_1:44;
end;
end;
theorem
not (LMP C in Upper_Arc C & UMP C in Upper_Arc C)
proof
assume that
A1: LMP C in Upper_Arc C and
A2: UMP C in Upper_Arc C;
A3: Upper_Arc(C) /\ Lower_Arc(C) = {W-min(C),E-max(C)} by JORDAN6:def 9;
set s = |[ (W-bound C + E-bound C) / 2, S-bound C ]|;
set S2 = LSeg(LMP C, s);
A4: Upper_Arc C is_an_arc_of W-min C,E-max C by JORDAN6:def 8;
Lower_Arc C is_an_arc_of E-max C,W-min C by JORDAN6:def 9;
then
A5: Lower_Arc C is_an_arc_of W-min C,E-max C by JORDAN5B:14;
A6: UMP C in C & LMP C in C by Th30,Th31;
A7: (UMP C)`1 = (W-bound C + E-bound C)/2 by EUCLID:52;
set n = |[ (W-bound C + E-bound C) / 2, N-bound C ]|;
set S1 = LSeg(n, UMP C);
A8: Upper_Arc C c= C by JORDAN6:61;
A9: n`2 = N-bound C by EUCLID:52;
n`1 = (W-bound C + E-bound C)/2 by EUCLID:52;
then
A10: S1 is vertical by A7,SPPOL_1:16;
A11: S1 misses S2 by Th42;
A12: UMP C in S1 by RLTOPSP1:68;
A13: (W-min C)`1 = W-bound C & (E-max C)`1 = E-bound C by EUCLID:52;
A14: Lower_Arc C c= C by JORDAN6:61;
then
A15: for p being Point of TOP-REAL 2 st p in Lower_Arc C holds (W-min C)`1<=
p`1 & p`1<=(E-max C)`1 by A13,PSCOMP_1:24;
A16: UMP C <> E-max C by Th25;
A17: UMP C <> W-min C by Th24;
A18: now
assume UMP C in Lower_Arc C;
then UMP C in Upper_Arc C /\ Lower_Arc C by A2,XBOOLE_0:def 4;
hence contradiction by A17,A16,A3,TARSKI:def 2;
end;
A19: W-bound C < E-bound C by SPRECT_1:31;
A20: Lower_Arc C misses S1
proof
A21: S1 /\ C = {UMP C} by Th34;
assume Lower_Arc C meets S1;
then consider x being object such that
A22: x in Lower_Arc C and
A23: x in S1 by XBOOLE_0:3;
x in S1 /\ C by A14,A22,A23,XBOOLE_0:def 4;
then
A24: x = UMP C by A21,TARSKI:def 1;
then x in Lower_Arc C /\ Upper_Arc C by A2,A22,XBOOLE_0:def 4;
hence contradiction by A17,A16,A3,A24,TARSKI:def 2;
end;
A25: LMP C <> E-max C by Th27;
A26: LMP C <> W-min C by Th26;
A27: now
assume LMP C in Lower_Arc C;
then LMP C in Upper_Arc C /\ Lower_Arc C by A1,XBOOLE_0:def 4;
hence contradiction by A26,A25,A3,TARSKI:def 2;
end;
A28: LMP C <> UMP C by Th37;
A29: (LMP C)`1 = (W-bound C + E-bound C)/2 by EUCLID:52;
A30: Lower_Arc C misses S2
proof
A31: S2 /\ C = {LMP C} by Th35;
assume Lower_Arc C meets S2;
then consider x being object such that
A32: x in Lower_Arc C and
A33: x in S2 by XBOOLE_0:3;
x in S2 /\ C by A14,A32,A33,XBOOLE_0:def 4;
then
A34: x = LMP C by A31,TARSKI:def 1;
then x in Lower_Arc C /\ Upper_Arc C by A1,A32,XBOOLE_0:def 4;
hence contradiction by A26,A25,A3,A34,TARSKI:def 2;
end;
s`1 = (W-bound C + E-bound C)/2 by EUCLID:52;
then
A35: S2 is vertical by A29,SPPOL_1:16;
A36: LMP C in S2 by RLTOPSP1:68;
A37: s`2 = S-bound C by EUCLID:52;
then
A38: for p being Point of TOP-REAL 2 st p in Lower_Arc C holds s`2<=p`2 & p
`2<=n`2 by A14,A9,PSCOMP_1:24;
per cases by A6,JORDAN16:7;
suppose
A39: LE LMP C, UMP C, C;
set S = Segment(Upper_Arc C, W-min C, E-max C, LMP C, UMP C);
A40: S c= Upper_Arc C by JORDAN16:2;
then
A41: S c= C by A8;
A42: now
let p be Point of TOP-REAL 2;
assume
A43: p in S1 \/ S \/ S2;
per cases by A43,Lm3;
suppose
p in S1;
then p`1 = (UMP C)`1 by A10,A12,SPPOL_1:def 3;
hence (W-min C)`1<=p`1 & p`1<=(E-max C)`1 by A7,A13,A19,XREAL_1:226;
end;
suppose
p in S;
hence (W-min C)`1<=p`1 & p`1<=(E-max C)`1 by A13,A41,PSCOMP_1:24;
end;
suppose
p in S2;
then p`1 = (LMP C)`1 by A35,A36,SPPOL_1:def 3;
hence (W-min C)`1<=p`1 & p`1<=(E-max C)`1 by A29,A13,A19,XREAL_1:226;
end;
end;
A44: now
let p be Point of TOP-REAL 2;
assume
A45: p in S1 \/ S \/ S2;
per cases by A45,Lm3;
suppose
A46: p in S1;
A47: s`2<=(UMP C)`2 by A37,Th38;
A48: (UMP C)`2<=n`2 by A9,Th39;
then (UMP C)`2<=p`2 by A46,TOPREAL1:4;
hence s`2<=p`2 & p`2<=n`2 by A46,A48,A47,TOPREAL1:4,XXREAL_0:2;
end;
suppose
p in S;
hence s`2<=p`2 & p`2<=n`2 by A37,A9,A41,PSCOMP_1:24;
end;
suppose
A49: p in S2;
A50: s`2<=(LMP C)`2 by A37,Th40;
hence s`2<=p`2 by A49,TOPREAL1:4;
p`2<=(LMP C)`2 by A49,A50,TOPREAL1:4;
hence p`2<=n`2 by A9,Th41,XXREAL_0:2;
end;
end;
A51: S c= Upper_Arc C \ {W-min C,E-max C}
proof
let s be object;
assume
A52: s in S;
now
assume s in {W-min C,E-max C};
then s = W-min C or s = E-max C by TARSKI:def 2;
hence contradiction by A16,A26,A4,A52,Th11;
end;
hence thesis by A40,A52,XBOOLE_0:def 5;
end;
Lower_Arc C misses S
proof
assume Lower_Arc C meets S;
then consider x being object such that
A53: x in Lower_Arc C and
A54: x in S by XBOOLE_0:3;
x in Upper_Arc C by A51,A54,XBOOLE_0:def 5;
then x in Lower_Arc C /\ Upper_Arc C by A53,XBOOLE_0:def 4;
hence contradiction by A3,A51,A54,XBOOLE_0:def 5;
end;
then
A55: Lower_Arc C misses S1 \/ S \/ S2 by A20,A30,Lm4;
A56: LE LMP C, UMP C, Upper_Arc C, W-min C, E-max C by A18,A39,JORDAN6:def 10;
then
A57: UMP C in S by JORDAN16:5;
A58: S1 /\ S = {UMP C}
proof
S1 /\ C = {UMP C} by Th34;
hence S1 /\ S c= {UMP C} by A41,XBOOLE_1:26;
let x be object;
assume x in {UMP C};
then
A59: x = UMP C by TARSKI:def 1;
UMP C in S1 by RLTOPSP1:68;
hence thesis by A57,A59,XBOOLE_0:def 4;
end;
A60: LMP C in S by A56,JORDAN16:5;
A61: S2 /\ S = {LMP C}
proof
S2 /\ C = {LMP C} by Th35;
hence S2 /\ S c= {LMP C} by A41,XBOOLE_1:26;
let x be object;
assume x in {LMP C};
then x = LMP C by TARSKI:def 1;
hence thesis by A36,A60,XBOOLE_0:def 4;
end;
S is_an_arc_of LMP C, UMP C by A28,A4,A56,JORDAN16:21;
then S is_an_arc_of UMP C, LMP C by JORDAN5B:14;
then
A62: S1 \/ S is_an_arc_of n,LMP C by A58,TOPREAL1:11;
(S1 \/ S) /\ S2 = S1 /\ S2 \/ S /\ S2 by XBOOLE_1:23
.= {} \/ S /\ S2 by A11;
then S1 \/ S \/ S2 is_an_arc_of n,s by A61,A62,TOPREAL1:10;
then S1 \/ S \/ S2 is_an_arc_of s,n by JORDAN5B:14;
hence thesis by A5,A38,A15,A55,A44,A42,JGRAPH_1:44;
end;
suppose
A63: LE UMP C, LMP C, C;
set S = Segment(Upper_Arc C, W-min C, E-max C, UMP C, LMP C);
A64: S c= Upper_Arc C by JORDAN16:2;
then
A65: S c= C by A8;
A66: now
let p be Point of TOP-REAL 2;
assume
A67: p in S1 \/ S \/ S2;
per cases by A67,Lm3;
suppose
p in S1;
then p`1 = (UMP C)`1 by A10,A12,SPPOL_1:def 3;
hence (W-min C)`1<=p`1 & p`1<=(E-max C)`1 by A7,A13,A19,XREAL_1:226;
end;
suppose
p in S;
hence (W-min C)`1<=p`1 & p`1<=(E-max C)`1 by A13,A65,PSCOMP_1:24;
end;
suppose
p in S2;
then p`1 = (LMP C)`1 by A35,A36,SPPOL_1:def 3;
hence (W-min C)`1<=p`1 & p`1<=(E-max C)`1 by A29,A13,A19,XREAL_1:226;
end;
end;
A68: now
let p be Point of TOP-REAL 2;
assume
A69: p in S1 \/ S \/ S2;
per cases by A69,Lm3;
suppose
A70: p in S1;
A71: s`2<=(UMP C)`2 by A37,Th38;
A72: (UMP C)`2<=n`2 by A9,Th39;
then (UMP C)`2<=p`2 by A70,TOPREAL1:4;
hence s`2<=p`2 & p`2<=n`2 by A70,A72,A71,TOPREAL1:4,XXREAL_0:2;
end;
suppose
p in S;
hence s`2<=p`2 & p`2<=n`2 by A37,A9,A65,PSCOMP_1:24;
end;
suppose
A73: p in S2;
A74: s`2<=(LMP C)`2 by A37,Th40;
hence s`2<=p`2 by A73,TOPREAL1:4;
p`2<=(LMP C)`2 by A73,A74,TOPREAL1:4;
hence p`2<=n`2 by A9,Th41,XXREAL_0:2;
end;
end;
A75: S c= Upper_Arc C \ {W-min C,E-max C}
proof
let s be object;
assume
A76: s in S;
now
assume s in {W-min C,E-max C};
then s = W-min C or s = E-max C by TARSKI:def 2;
hence contradiction by A17,A25,A4,A76,Th11;
end;
hence thesis by A64,A76,XBOOLE_0:def 5;
end;
Lower_Arc C misses S
proof
assume Lower_Arc C meets S;
then consider x being object such that
A77: x in Lower_Arc C and
A78: x in S by XBOOLE_0:3;
x in Upper_Arc C by A75,A78,XBOOLE_0:def 5;
then x in Lower_Arc C /\ Upper_Arc C by A77,XBOOLE_0:def 4;
hence contradiction by A3,A75,A78,XBOOLE_0:def 5;
end;
then
A79: Lower_Arc C misses S1 \/ S \/ S2 by A20,A30,Lm4;
A80: LE UMP C, LMP C, Upper_Arc C, W-min C, E-max C by A27,A63,JORDAN6:def 10;
then
A81: UMP C in S by JORDAN16:5;
A82: S1 /\ S = {UMP C}
proof
S1 /\ C = {UMP C} by Th34;
hence S1 /\ S c= {UMP C} by A65,XBOOLE_1:26;
let x be object;
assume x in {UMP C};
then
A83: x = UMP C by TARSKI:def 1;
UMP C in S1 by RLTOPSP1:68;
hence thesis by A81,A83,XBOOLE_0:def 4;
end;
A84: LMP C in S by A80,JORDAN16:5;
A85: S2 /\ S = {LMP C}
proof
S2 /\ C = {LMP C} by Th35;
hence S2 /\ S c= {LMP C} by A65,XBOOLE_1:26;
let x be object;
assume x in {LMP C};
then x = LMP C by TARSKI:def 1;
hence thesis by A36,A84,XBOOLE_0:def 4;
end;
S is_an_arc_of UMP C, LMP C by A4,A80,Th37,JORDAN16:21;
then
A86: S1 \/ S is_an_arc_of n,LMP C by A82,TOPREAL1:11;
(S1 \/ S) /\ S2 = S1 /\ S2 \/ S /\ S2 by XBOOLE_1:23
.= {} \/ S /\ S2 by A11;
then S1 \/ S \/ S2 is_an_arc_of n,s by A85,A86,TOPREAL1:10;
then S1 \/ S \/ S2 is_an_arc_of s,n by JORDAN5B:14;
hence thesis by A5,A38,A15,A79,A68,A66,JGRAPH_1:44;
end;
end;