:: The Ordering of Points on a Curve, Part {IV}
:: by Artur Korni{\l}owicz
::
:: Received September 16, 2002
:: Copyright (c) 2002-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 NUMBERS, SUBSET_1, EUCLID, PRE_TOPC, TOPREAL2, RELAT_1, STRUCT_0,
ARYTM_1, SQUARE_1, XBOOLE_0, FUNCT_1, TOPS_2, RCOMP_1, ORDINAL2,
TOPREAL1, XXREAL_2, MCART_1, XXREAL_0, CARD_1, ARYTM_3, PCOMPS_1,
METRIC_1, TARSKI, COMPLEX1, JORDAN2C, RLTOPSP1, SPPOL_1, ZFMISC_1,
JORDAN6, JORDAN3, JORDAN18, SEQ_4, REAL_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, RELSET_1, ORDINAL1,
NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1, XXREAL_2, SEQ_4,
STRUCT_0, PCOMPS_1, COMPLEX1, PRE_TOPC, TOPS_2, RCOMP_1, COMPTS_1,
METRIC_1, SPPOL_1, RLTOPSP1, EUCLID, TOPREAL1, PSCOMP_1, TOPREAL2,
JORDAN5C, JORDAN2C, TOPREAL6, JORDAN6;
constructors REAL_1, SQUARE_1, COMPLEX1, RCOMP_1, TOPS_2, COMPTS_1, TOPREAL1,
SPPOL_1, PSCOMP_1, JORDAN5C, JORDAN6, JORDAN2C, TOPREAL6, SEQ_4,
RELSET_1, FUNCSDOM, BINOP_2, PCOMPS_1;
registrations RELSET_1, NUMBERS, XXREAL_0, XREAL_0, SQUARE_1, MEMBERED,
COMPTS_1, EUCLID, TOPREAL1, STRUCT_0, TOPS_1, JORDAN2C, ORDINAL1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0, ZFMISC_1, XXREAL_2;
equalities XBOOLE_0, SQUARE_1, SUBSET_1;
expansions TARSKI, XBOOLE_0, XXREAL_2;
theorems JORDAN5B, TARSKI, TOPREAL1, XBOOLE_0, EUCLID, JORDAN6, TOPS_2,
XBOOLE_1, SEQ_4, RELAT_1, PSCOMP_1, FUNCT_2, TOPREAL3, JORDAN1A,
COMPTS_1, ZFMISC_1, JORDAN5C, TOPREAL2, JORDAN2C, SQUARE_1, RCOMP_1,
TOPMETR, METRIC_1, JORDAN16, SPPOL_1, COMPLEX1, XREAL_1, TOPREAL6,
XXREAL_0, JCT_MISC, PRE_TOPC, RLTOPSP1;
begin :: Preliminaries
reserve n for Element of NAT,
V for Subset of TOP-REAL n,
s,s1,s2,t,t1,t2 for Point of TOP-REAL n,
C for Simple_closed_curve,
P for Subset of TOP-REAL 2,
a,p ,p1,p2,q,q1,q2 for Point of TOP-REAL 2;
Lm1: dom proj1 = the carrier of TOP-REAL 2 by FUNCT_2:def 1;
Lm2: dom proj2 = the carrier of TOP-REAL 2 by FUNCT_2:def 1;
theorem
for a,b being Real holds (a-b)^2 = (b-a)^2;
theorem
for S,T being non empty TopStruct, f being Function of S,T, A being
Subset of T st f is being_homeomorphism & A is compact holds f"A is compact
proof
let S,T be non empty TopStruct, f be Function of S,T, A be Subset of T such
that
A1: f is being_homeomorphism and
A2: A is compact;
A3: rng f = [#]T & f is one-to-one by A1,TOPS_2:def 5;
f" is being_homeomorphism by A1,TOPS_2:56;
then
A4: rng (f") = [#]S by TOPS_2:def 5;
f" is continuous by A1,TOPS_2:def 5;
then f".:A is compact by A2,A4,COMPTS_1:15;
hence thesis by A3,TOPS_2:55;
end;
theorem Th3:
proj2.:(north_halfline a) is bounded_below
proof
take a`2;
let r be ExtReal;
assume r in proj2.:(north_halfline a);
then consider x being object such that
A1: x in the carrier of TOP-REAL 2 and
A2: x in north_halfline a and
A3: r = proj2.x by FUNCT_2:64;
reconsider x as Point of TOP-REAL 2 by A1;
r = x`2 by A3,PSCOMP_1:def 6;
hence thesis by A2,TOPREAL1:def 10;
end;
theorem Th4:
proj2.:(south_halfline a) is bounded_above
proof
take a`2;
let r be ExtReal;
assume r in proj2.:(south_halfline a);
then consider x being object such that
A1: x in the carrier of TOP-REAL 2 and
A2: x in south_halfline a and
A3: r = proj2.x by FUNCT_2:64;
reconsider x as Point of TOP-REAL 2 by A1;
r = x`2 by A3,PSCOMP_1:def 6;
hence thesis by A2,TOPREAL1:def 12;
end;
theorem Th5:
proj1.:(west_halfline a) is bounded_above
proof
take a`1;
let r be ExtReal;
assume r in proj1.:(west_halfline a);
then consider x being object such that
A1: x in the carrier of TOP-REAL 2 and
A2: x in west_halfline a and
A3: r = proj1.x by FUNCT_2:64;
reconsider x as Point of TOP-REAL 2 by A1;
r = x`1 by A3,PSCOMP_1:def 5;
hence thesis by A2,TOPREAL1:def 13;
end;
theorem Th6:
proj1.:(east_halfline a) is bounded_below
proof
take a`1;
let r be ExtReal;
assume r in proj1.:(east_halfline a);
then consider x being object such that
A1: x in the carrier of TOP-REAL 2 and
A2: x in east_halfline a and
A3: r = proj1.x by FUNCT_2:64;
reconsider x as Point of TOP-REAL 2 by A1;
r = x`1 by A3,PSCOMP_1:def 5;
hence thesis by A2,TOPREAL1:def 11;
end;
registration
let a;
cluster proj2.:(north_halfline a) -> non empty;
coherence by Lm2,RELAT_1:119;
cluster proj2.:(south_halfline a) -> non empty;
coherence by Lm2,RELAT_1:119;
cluster proj1.:(west_halfline a) -> non empty;
coherence by Lm1,RELAT_1:119;
cluster proj1.:(east_halfline a) -> non empty;
coherence by Lm1,RELAT_1:119;
end;
theorem Th7:
lower_bound(proj2.:(north_halfline a)) = a`2
proof
set X = proj2.:(north_halfline a);
A1: now
let r be Real;
assume r in X;
then consider x being object such that
A2: x in the carrier of TOP-REAL 2 and
A3: x in north_halfline a and
A4: r = proj2.x by FUNCT_2:64;
reconsider x as Point of TOP-REAL 2 by A2;
r = x`2 by A4,PSCOMP_1:def 6;
hence a`2 <= r by A3,TOPREAL1:def 10;
end;
A5: now
reconsider r = a`2 as Real;
let s be Real;
assume 0 < s;
then
A6: r + 0 < a`2 + s by XREAL_1:8;
take r;
a in north_halfline a & r = proj2.a by PSCOMP_1:def 6,TOPREAL1:38;
hence r in X by FUNCT_2:35;
thus r < a`2 + s by A6;
end;
X is bounded_below by Th3;
hence thesis by A1,A5,SEQ_4:def 2;
end;
theorem Th8:
upper_bound(proj2.:(south_halfline a)) = a`2
proof
set X = proj2.:(south_halfline a);
A1: now
let r be Real;
assume r in X;
then consider x being object such that
A2: x in the carrier of TOP-REAL 2 and
A3: x in south_halfline a and
A4: r = proj2.x by FUNCT_2:64;
reconsider x as Point of TOP-REAL 2 by A2;
r = x`2 by A4,PSCOMP_1:def 6;
hence r <= a`2 by A3,TOPREAL1:def 12;
end;
A5: now
reconsider r = a`2 as Real;
let s be Real;
assume 0 < s;
then
A6: a`2 - s < r - 0 by XREAL_1:15;
take r;
a in south_halfline a & r = proj2.a by PSCOMP_1:def 6,TOPREAL1:38;
hence r in X by FUNCT_2:35;
thus a`2 - s < r by A6;
end;
X is bounded_above by Th4;
hence thesis by A1,A5,SEQ_4:def 1;
end;
theorem
upper_bound(proj1.:(west_halfline a)) = a`1
proof
set X = proj1.:(west_halfline a);
A1: now
let r be Real;
assume r in X;
then consider x being object such that
A2: x in the carrier of TOP-REAL 2 and
A3: x in west_halfline a and
A4: r = proj1.x by FUNCT_2:64;
reconsider x as Point of TOP-REAL 2 by A2;
r = x`1 by A4,PSCOMP_1:def 5;
hence r <= a`1 by A3,TOPREAL1:def 13;
end;
A5: now
reconsider r = a`1 as Real;
let s be Real;
assume 0 < s;
then
A6: a`1 - s < r - 0 by XREAL_1:15;
take r;
a in west_halfline a & r = proj1.a by PSCOMP_1:def 5,TOPREAL1:38;
hence r in X by FUNCT_2:35;
thus a`1 - s < r by A6;
end;
X is bounded_above by Th5;
hence thesis by A1,A5,SEQ_4:def 1;
end;
theorem
lower_bound(proj1.:(east_halfline a)) = a`1
proof
set X = proj1.:(east_halfline a);
A1: now
let r be Real;
assume r in X;
then consider x being object such that
A2: x in the carrier of TOP-REAL 2 and
A3: x in east_halfline a and
A4: r = proj1.x by FUNCT_2:64;
reconsider x as Point of TOP-REAL 2 by A2;
r = x`1 by A4,PSCOMP_1:def 5;
hence a`1 <= r by A3,TOPREAL1:def 11;
end;
A5: now
reconsider r = a`1 as Real;
let s be Real;
assume 0 < s;
then
A6: r + 0 < a`1 + s by XREAL_1:8;
take r;
a in east_halfline a & r = proj1.a by PSCOMP_1:def 5,TOPREAL1:38;
hence r in X by FUNCT_2:35;
thus r < a`1 + s by A6;
end;
X is bounded_below by Th6;
hence thesis by A1,A5,SEQ_4:def 2;
end;
Lm3: the TopStruct of TOP-REAL 2 = TopSpaceMetr Euclid 2 by EUCLID:def 8;
registration
let a;
cluster north_halfline a -> closed;
coherence
proof
set X = north_halfline a;
reconsider XX = X` as Subset of TOP-REAL 2;
reconsider OO = XX as Subset of TopSpaceMetr Euclid 2 by Lm3;
for p being Point of Euclid 2 st p in X` ex r being Real st r>0
& Ball(p,r) c= X`
proof
let p be Point of Euclid 2;
reconsider x = p as Point of TOP-REAL 2 by EUCLID:67;
assume p in X`;
then
A1: not p in X by XBOOLE_0:def 5;
per cases by A1,TOPREAL1:def 10;
suppose
A2: x`1 <> a`1;
take r = |.x`1-a`1.|;
x`1 - a`1 <> 0 by A2;
hence r > 0 by COMPLEX1:47;
let b be object;
assume
A3: b in Ball(p,r);
then reconsider bb=b as Point of Euclid 2;
reconsider c = bb as Point of TOP-REAL 2 by EUCLID:67;
dist(p,bb) < r by A3,METRIC_1:11;
then
A4: dist(x,c) < r by TOPREAL6:def 1;
now
assume c`1 = a`1;
then
A5: sqrt ((x`1-c`1)^2 + (x`2-c`2)^2) < |.x`1-c`1.| by A4,TOPREAL6:92;
A6: 0 <= (x`1-c`1)^2 by XREAL_1:63;
A7: 0 <= (x`2-c`2)^2 by XREAL_1:63;
then 0 <= sqrt ((x`1-c`1)^2 + (x`2-c`2)^2) by A6,SQUARE_1:def 2;
then (sqrt ((x`1-c`1)^2 + (x`2-c`2)^2))^2 < |.x`1-c`1.|^2 by A5,
SQUARE_1:16;
then (sqrt ((x`1-c`1)^2 + (x`2-c`2)^2))^2 < (x`1-c`1)^2 by
COMPLEX1:75;
then (x`1-c`1)^2 + (x`2-c`2)^2 < (x`1-c`1)^2 + 0 by A6,SQUARE_1:def 2
;
hence contradiction by A7,XREAL_1:7;
end;
then not c in X by TOPREAL1:def 10;
hence b in X` by XBOOLE_0:def 5;
end;
suppose
A8: x`2 < a`2;
take r = a`2-x`2;
thus r > 0 by A8,XREAL_1:50;
let b be object;
assume
A9: b in Ball(p,r);
then reconsider b as Point of Euclid 2;
reconsider c = b as Point of TOP-REAL 2 by EUCLID:67;
dist(p,b) < r by A9,METRIC_1:11;
then
A10: dist(x,c) < r by TOPREAL6:def 1;
now
assume c`2 >= a`2;
then
A11: a`2-x`2 <= c`2-x`2 by XREAL_1:13;
0 <= a`2-x`2 by A8,XREAL_1:50;
then
A12: (a`2-x`2)^2 <= (c`2-x`2)^2 by A11,SQUARE_1:15;
A13: 0 <= (x`1-c`1)^2 by XREAL_1:63;
A14: sqrt ((x`1-c`1)^2 + (x`2-c`2)^2) < a`2-x`2 by A10,TOPREAL6:92;
A15: 0 <= (x`2-c`2)^2 by XREAL_1:63;
then 0 <= sqrt ((x`1-c`1)^2 + (x`2-c`2)^2) by A13,SQUARE_1:def 2;
then (sqrt ((x`1-c`1)^2 + (x`2-c`2)^2))^2 < (a`2-x`2)^2 by A14,
SQUARE_1:16;
then
A16: (x`1-c`1)^2 + (x`2-c`2)^2 < (a`2-x`2)^2 by A13,A15,SQUARE_1:def 2;
0 + (x`2-c`2)^2 <= (x`1-c`1)^2 + (x`2-c`2)^2 by A13,XREAL_1:7;
hence contradiction by A16,A12,XXREAL_0:2;
end;
then not c in X by TOPREAL1:def 10;
hence thesis by XBOOLE_0:def 5;
end;
end;
then OO is open by TOPMETR:15;
then XX is open by Lm3,PRE_TOPC:30;
then XX` is closed;
hence thesis;
end;
cluster south_halfline a -> closed;
coherence
proof
set X = south_halfline a;
reconsider XX = X` as Subset of TOP-REAL 2;
reconsider OO = XX as Subset of TopSpaceMetr Euclid 2 by Lm3;
for p being Point of Euclid 2 st p in X` ex r being Real st r>
0 & Ball(p,r) c= X`
proof
let p be Point of Euclid 2;
reconsider x = p as Point of TOP-REAL 2 by EUCLID:67;
assume p in X`;
then
A17: not p in X by XBOOLE_0:def 5;
per cases by A17,TOPREAL1:def 12;
suppose
A18: x`1 <> a`1;
take r = |.x`1-a`1.|;
x`1 - a`1 <> 0 by A18;
hence r > 0 by COMPLEX1:47;
let b be object;
assume
A19: b in Ball(p,r);
then reconsider b as Point of Euclid 2;
reconsider c = b as Point of TOP-REAL 2 by EUCLID:67;
dist(p,b) < r by A19,METRIC_1:11;
then
A20: dist(x,c) < r by TOPREAL6:def 1;
now
assume c`1 = a`1;
then
A21: sqrt ((x`1-c`1)^2 + (x`2-c`2)^2) < |.x`1-c`1.| by A20,TOPREAL6:92;
A22: 0 <= (x`1-c`1)^2 by XREAL_1:63;
A23: 0 <= (x`2-c`2)^2 by XREAL_1:63;
then 0 <= sqrt ((x`1-c`1)^2 + (x`2-c`2)^2) by A22,SQUARE_1:def 2;
then (sqrt ((x`1-c`1)^2 + (x`2-c`2)^2))^2 < |.x`1-c`1.|^2 by A21,
SQUARE_1:16;
then (sqrt ((x`1-c`1)^2 + (x`2-c`2)^2))^2 < (x`1-c`1)^2 by
COMPLEX1:75;
then (x`1-c`1)^2 + (x`2-c`2)^2 < (x`1-c`1)^2 + 0 by A22,
SQUARE_1:def 2;
hence contradiction by A23,XREAL_1:7;
end;
then not c in X by TOPREAL1:def 12;
hence thesis by XBOOLE_0:def 5;
end;
suppose
A24: x`2 > a`2;
take r = x`2-a`2;
thus r > 0 by A24,XREAL_1:50;
let b be object;
assume
A25: b in Ball(p,r);
then reconsider b as Point of Euclid 2;
reconsider c = b as Point of TOP-REAL 2 by EUCLID:67;
dist(p,b) < r by A25,METRIC_1:11;
then
A26: dist(x,c) < r by TOPREAL6:def 1;
now
assume c`2 <= a`2;
then
A27: x`2-c`2 >= x`2-a`2 by XREAL_1:13;
0 <= x`2-a`2 by A24,XREAL_1:50;
then
A28: (x`2-a`2)^2 <= (x`2-c`2)^2 by A27,SQUARE_1:15;
A29: 0 <= (x`1-c`1)^2 by XREAL_1:63;
A30: sqrt ((x`1-c`1)^2 + (x`2-c`2)^2) < x`2-a`2 by A26,TOPREAL6:92;
A31: 0 <= (x`2-c`2)^2 by XREAL_1:63;
then 0 <= sqrt ((x`1-c`1)^2 + (x`2-c`2)^2) by A29,SQUARE_1:def 2;
then (sqrt ((x`1-c`1)^2 + (x`2-c`2)^2))^2 < (x`2-a`2)^2 by A30,
SQUARE_1:16;
then
A32: (x`1-c`1)^2 + (x`2-c`2)^2 < (x`2-a`2)^2 by A29,A31,SQUARE_1:def 2;
0 + (x`2-c`2)^2 <= (x`1-c`1)^2 + (x`2-c`2)^2 by A29,XREAL_1:7;
hence contradiction by A32,A28,XXREAL_0:2;
end;
then not c in X by TOPREAL1:def 12;
hence thesis by XBOOLE_0:def 5;
end;
end;
then OO is open by TOPMETR:15;
then XX is open by Lm3,PRE_TOPC:30;
then XX` is closed;
hence thesis;
end;
cluster east_halfline a -> closed;
coherence
proof
set X = east_halfline a;
reconsider XX = X` as Subset of TOP-REAL 2;
reconsider OO = XX as Subset of TopSpaceMetr Euclid 2 by Lm3;
for p being Point of Euclid 2 st p in X` ex r being Real st r>
0 & Ball(p,r) c= X`
proof
let p be Point of Euclid 2;
reconsider x = p as Point of TOP-REAL 2 by EUCLID:67;
assume p in X`;
then
A33: not p in X by XBOOLE_0:def 5;
per cases by A33,TOPREAL1:def 11;
suppose
A34: x`2 <> a`2;
take r = |.x`2-a`2.|;
x`2 - a`2 <> 0 by A34;
hence r > 0 by COMPLEX1:47;
let b be object;
assume
A35: b in Ball(p,r);
then reconsider b as Point of Euclid 2;
reconsider c = b as Point of TOP-REAL 2 by EUCLID:67;
dist(p,b) < r by A35,METRIC_1:11;
then
A36: dist(x,c) < r by TOPREAL6:def 1;
now
assume c`2 = a`2;
then
A37: sqrt ((x`1-c`1)^2 + (x`2-c`2)^2) < |.x`2-c`2.| by A36,TOPREAL6:92;
A38: 0 <= (x`2-c`2)^2 by XREAL_1:63;
A39: 0 <= (x`1-c`1)^2 by XREAL_1:63;
then 0 <= sqrt ((x`1-c`1)^2 + (x`2-c`2)^2) by A38,SQUARE_1:def 2;
then (sqrt ((x`1-c`1)^2 + (x`2-c`2)^2))^2 < (|.x`2-c`2.|)^2 by A37,
SQUARE_1:16;
then (sqrt ((x`1-c`1)^2 + (x`2-c`2)^2))^2 < (x`2-c`2)^2 by
COMPLEX1:75;
then (x`1-c`1)^2 + (x`2-c`2)^2 < (x`2-c`2)^2 + 0 by A38,
SQUARE_1:def 2;
hence contradiction by A39,XREAL_1:7;
end;
then not c in X by TOPREAL1:def 11;
hence thesis by XBOOLE_0:def 5;
end;
suppose
A40: x`1 < a`1;
take r = a`1-x`1;
thus r > 0 by A40,XREAL_1:50;
let b be object;
assume
A41: b in Ball(p,r);
then reconsider b as Point of Euclid 2;
reconsider c = b as Point of TOP-REAL 2 by EUCLID:67;
dist(p,b) < r by A41,METRIC_1:11;
then
A42: dist(x,c) < r by TOPREAL6:def 1;
now
assume c`1 >= a`1;
then
A43: a`1-x`1 <= c`1-x`1 by XREAL_1:13;
0 <= a`1-x`1 by A40,XREAL_1:50;
then
A44: (a`1-x`1)^2 <= (c`1-x`1)^2 by A43,SQUARE_1:15;
A45: 0 <= (x`2-c`2)^2 by XREAL_1:63;
A46: sqrt ((x`1-c`1)^2 + (x`2-c`2)^2) < a`1-x`1 by A42,TOPREAL6:92;
A47: 0 <= (x`1-c`1)^2 by XREAL_1:63;
then 0 <= sqrt ((x`1-c`1)^2 + (x`2-c`2)^2) by A45,SQUARE_1:def 2;
then (sqrt ((x`1-c`1)^2 + (x`2-c`2)^2))^2 < (a`1-x`1)^2 by A46,
SQUARE_1:16;
then
A48: (x`1-c`1)^2 + (x`2-c`2)^2 < (a`1-x`1)^2 by A45,A47,SQUARE_1:def 2;
(x`1-c`1)^2 + 0 <= (x`1-c`1)^2 + (x`2-c`2)^2 by A45,XREAL_1:7;
hence contradiction by A48,A44,XXREAL_0:2;
end;
then not c in X by TOPREAL1:def 11;
hence thesis by XBOOLE_0:def 5;
end;
end;
then OO is open by TOPMETR:15;
then XX is open by Lm3,PRE_TOPC:30;
then XX` is closed;
hence thesis;
end;
cluster west_halfline a -> closed;
coherence
proof
set X = west_halfline a;
reconsider XX = X` as Subset of TOP-REAL 2;
reconsider OO = XX as Subset of TopSpaceMetr Euclid 2 by Lm3;
for p being Point of Euclid 2 st p in X` ex r being Real st r
>0 & Ball(p,r) c= X`
proof
let p be Point of Euclid 2;
reconsider x = p as Point of TOP-REAL 2 by EUCLID:67;
assume p in X`;
then
A49: not p in X by XBOOLE_0:def 5;
per cases by A49,TOPREAL1:def 13;
suppose
A50: x`2 <> a`2;
take r = |.x`2-a`2.|;
x`2 - a`2 <> 0 by A50;
hence r > 0 by COMPLEX1:47;
let b be object;
assume
A51: b in Ball(p,r);
then reconsider b as Point of Euclid 2;
reconsider c = b as Point of TOP-REAL 2 by EUCLID:67;
dist(p,b) < r by A51,METRIC_1:11;
then
A52: dist(x,c) < r by TOPREAL6:def 1;
now
assume c`2 = a`2;
then
A53: sqrt ((x`1-c`1)^2 + (x`2-c`2)^2) < |.x`2-c`2.| by A52,TOPREAL6:92;
A54: 0 <= (x`2-c`2)^2 by XREAL_1:63;
A55: 0 <= (x`1-c`1)^2 by XREAL_1:63;
then 0 <= sqrt ((x`1-c`1)^2 + (x`2-c`2)^2) by A54,SQUARE_1:def 2;
then (sqrt ((x`1-c`1)^2 + (x`2-c`2)^2))^2 < (|.x`2-c`2.|)^2 by A53,
SQUARE_1:16;
then (sqrt ((x`1-c`1)^2 + (x`2-c`2)^2))^2 < (x`2-c`2)^2 by
COMPLEX1:75;
then (x`1-c`1)^2 + (x`2-c`2)^2 < (x`2-c`2)^2 + 0 by A54,
SQUARE_1:def 2;
hence contradiction by A55,XREAL_1:7;
end;
then not c in X by TOPREAL1:def 13;
hence thesis by XBOOLE_0:def 5;
end;
suppose
A56: x`1 > a`1;
take r = x`1-a`1;
thus r > 0 by A56,XREAL_1:50;
let b be object;
assume
A57: b in Ball(p,r);
then reconsider b as Point of Euclid 2;
reconsider c = b as Point of TOP-REAL 2 by EUCLID:67;
dist(p,b) < r by A57,METRIC_1:11;
then
A58: dist(x,c) < r by TOPREAL6:def 1;
now
assume c`1 <= a`1;
then
A59: x`1-c`1 >= x`1-a`1 by XREAL_1:13;
0 <= x`1-a`1 by A56,XREAL_1:50;
then
A60: (x`1-a`1)^2 <= (x`1-c`1)^2 by A59,SQUARE_1:15;
A61: 0 <= (x`2-c`2)^2 by XREAL_1:63;
A62: sqrt ((x`1-c`1)^2 + (x`2-c`2)^2) < x`1-a`1 by A58,TOPREAL6:92;
A63: 0 <= (x`1-c`1)^2 by XREAL_1:63;
then 0 <= sqrt ((x`1-c`1)^2 + (x`2-c`2)^2) by A61,SQUARE_1:def 2;
then (sqrt ((x`1-c`1)^2 + (x`2-c`2)^2))^2 < (x`1-a`1)^2 by A62,
SQUARE_1:16;
then
A64: (x`1-c`1)^2 + (x`2-c`2)^2 < (x`1-a`1)^2 by A61,A63,SQUARE_1:def 2;
0 + (x`1-c`1)^2 <= (x`1-c`1)^2 + (x`2-c`2)^2 by A61,XREAL_1:7;
hence contradiction by A64,A60,XXREAL_0:2;
end;
then not c in X by TOPREAL1:def 13;
hence thesis by XBOOLE_0:def 5;
end;
end;
then OO is open by TOPMETR:15;
then XX is open by Lm3,PRE_TOPC:30;
then XX` is closed;
hence thesis;
end;
end;
theorem Th11:
a in BDD P implies not north_halfline a c= UBD P
proof
A1: BDD P misses UBD P & a in north_halfline a by JORDAN2C:24,TOPREAL1:38;
assume a in BDD P;
hence thesis by A1,XBOOLE_0:3;
end;
theorem Th12:
a in BDD P implies not south_halfline a c= UBD P
proof
A1: BDD P misses UBD P & a in south_halfline a by JORDAN2C:24,TOPREAL1:38;
assume a in BDD P;
hence thesis by A1,XBOOLE_0:3;
end;
theorem
a in BDD P implies not east_halfline a c= UBD P
proof
A1: BDD P misses UBD P & a in east_halfline a by JORDAN2C:24,TOPREAL1:38;
assume a in BDD P;
hence thesis by A1,XBOOLE_0:3;
end;
theorem
a in BDD P implies not west_halfline a c= UBD P
proof
A1: BDD P misses UBD P & a in west_halfline a by JORDAN2C:24,TOPREAL1:38;
assume a in BDD P;
hence thesis by A1,XBOOLE_0:3;
end;
theorem Th15:
for C being Simple_closed_curve, P being Subset of TOP-REAL 2,
p1,p2 being Point of TOP-REAL 2 st P is_an_arc_of p1,p2 & P c= C ex R being non
empty Subset of TOP-REAL 2 st R is_an_arc_of p1,p2 & P \/ R = C & P /\ R = {p1,
p2}
proof
let C be Simple_closed_curve, P be Subset of TOP-REAL 2, p1,p2 be Point of
TOP-REAL 2 such that
A1: P is_an_arc_of p1,p2 and
A2: P c= C;
A3: p1 <> p2 by A1,JORDAN6:37;
p1 in P & p2 in P by A1,TOPREAL1:1;
then consider P1,P2 being non empty Subset of TOP-REAL 2 such that
A4: P1 is_an_arc_of p1,p2 and
A5: P2 is_an_arc_of p1,p2 and
A6: C = P1 \/ P2 and
A7: P1 /\ P2 = {p1,p2} by A2,A3,TOPREAL2:5;
reconsider P1,P2 as non empty Subset of TOP-REAL 2;
A8: P1 c= C & P2 c= C by A6,XBOOLE_1:7;
A9: now
assume
A10: P1 = P2;
ex p3 being Point of TOP-REAL 2 st p3 in P1 & p3 <> p1 & p3 <> p2 by A4,
JORDAN6:42;
hence contradiction by A7,A10,TARSKI:def 2;
end;
per cases by A1,A2,A4,A5,A8,A9,JORDAN16:14;
suppose
A11: P = P1;
take P2;
thus thesis by A5,A6,A7,A11;
end;
suppose
A12: P = P2;
take P1;
thus thesis by A4,A6,A7,A12;
end;
end;
begin :: Two Special Points on a Simple Closed Curve
definition
let p,P;
func North-Bound(p,P) -> Point of TOP-REAL 2 equals
|[p`1,lower_bound(proj2.:(P /\
north_halfline p))]|;
correctness;
func South-Bound(p,P) -> Point of TOP-REAL 2 equals
|[p`1,upper_bound(proj2.:(P /\
south_halfline p))]|;
correctness;
end;
theorem
North-Bound(p,P)`1 = p`1 & South-Bound(p,P)`1 = p`1 by EUCLID:52;
theorem Th17:
for C being compact Subset of TOP-REAL 2 holds p in BDD C
implies North-Bound(p,C) in C & North-Bound(p,C) in north_halfline p &
South-Bound(p,C) in C & South-Bound(p,C) in south_halfline p
proof
let C be compact Subset of TOP-REAL 2;
set X = C /\ north_halfline p;
X c= C by XBOOLE_1:17;
then proj2.:X is real-bounded by JCT_MISC:14,RLTOPSP1:42;
then
A1: proj2.:X is bounded_below;
assume
A2: p in BDD C;
then not north_halfline p c= UBD C by Th11;
then north_halfline p meets C by JORDAN2C:129;
then
A3: X is non empty;
X is bounded by RLTOPSP1:42,XBOOLE_1:17;
then proj2.:X is closed by JCT_MISC:13;
then lower_bound (proj2.:X) in proj2.:X by A3,A1,Lm2,RCOMP_1:13,RELAT_1:119;
then consider x being object such that
A4: x in the carrier of TOP-REAL 2 and
A5: x in X and
A6: lower_bound (proj2.:X) = proj2.x by FUNCT_2:64;
reconsider x as Point of TOP-REAL 2 by A4;
A7: x`2 = lower_bound (proj2.:X) by A6,PSCOMP_1:def 6
.= North-Bound(p,C)`2 by EUCLID:52;
x in north_halfline p by A5,XBOOLE_0:def 4;
then x`1 = p`1 by TOPREAL1:def 10
.= North-Bound(p,C)`1 by EUCLID:52;
then x = North-Bound(p,C) by A7,TOPREAL3:6;
hence North-Bound(p,C) in C & North-Bound(p,C) in north_halfline p by A5,
XBOOLE_0:def 4;
set X = C /\ south_halfline p;
X c= C by XBOOLE_1:17;
then proj2.:X is real-bounded by JCT_MISC:14,RLTOPSP1:42;
then
A8: proj2.:X is bounded_above;
not south_halfline p c= UBD C by A2,Th12;
then south_halfline p meets C by JORDAN2C:128;
then
A9: X is non empty;
X is bounded by RLTOPSP1:42,XBOOLE_1:17;
then proj2.:X is closed by JCT_MISC:13;
then upper_bound (proj2.:X) in proj2.:X by A9,A8,Lm2,RCOMP_1:12,RELAT_1:119;
then consider x being object such that
A10: x in the carrier of TOP-REAL 2 and
A11: x in X and
A12: upper_bound (proj2.:X) = proj2.x by FUNCT_2:64;
reconsider x as Point of TOP-REAL 2 by A10;
x in south_halfline p by A11,XBOOLE_0:def 4;
then
A13: x`1 = p`1 by TOPREAL1:def 12
.= South-Bound(p,C)`1 by EUCLID:52;
x`2 = upper_bound (proj2.:X) by A12,PSCOMP_1:def 6
.= South-Bound(p,C)`2 by EUCLID:52;
then x = South-Bound(p,C) by A13,TOPREAL3:6;
hence thesis by A11,XBOOLE_0:def 4;
end;
theorem Th18:
for C being compact Subset of TOP-REAL 2 holds p in BDD C
implies South-Bound(p,C)`2 < p`2 & p`2 < North-Bound(p,C)`2
proof
let C be compact Subset of TOP-REAL 2;
assume
A1: p in BDD C;
then South-Bound(p,C) in C & South-Bound(p,C) in south_halfline p by Th17;
then South-Bound(p,C) in C /\ south_halfline p by XBOOLE_0:def 4;
then
A2: proj2.:(C /\ south_halfline p) is non empty by Lm2,RELAT_1:119;
A3: BDD C misses C by JORDAN1A:7;
A4: now
A5: South-Bound(p,C)`1 = p`1 by EUCLID:52;
assume South-Bound(p,C)`2 = p`2;
then South-Bound(p,C) = p by A5,TOPREAL3:6;
then p in C by A1,Th17;
hence contradiction by A1,A3,XBOOLE_0:3;
end;
North-Bound(p,C) in C & North-Bound(p,C) in north_halfline p by A1,Th17;
then C /\ north_halfline p is non empty by XBOOLE_0:def 4;
then
A6: proj2.:(C /\ north_halfline p) is non empty by Lm2,RELAT_1:119;
proj2.:(south_halfline p) is bounded_above & C /\ south_halfline p c=
south_halfline p by Th4,XBOOLE_1:17;
then
A7: upper_bound(proj2.:(C /\ south_halfline p)) <=
upper_bound(proj2.:(south_halfline p) )
by A2,RELAT_1:123,SEQ_4:48;
A8: now
A9: North-Bound(p,C)`1 = p`1 by EUCLID:52;
assume North-Bound(p,C)`2 = p`2;
then North-Bound(p,C) = p by A9,TOPREAL3:6;
then p in C by A1,Th17;
hence contradiction by A1,A3,XBOOLE_0:3;
end;
South-Bound(p,C)`2 = upper_bound(proj2.:(C /\ south_halfline p))
& upper_bound(proj2.:(
south_halfline p)) = p`2 by Th8,EUCLID:52;
hence South-Bound(p,C)`2 < p`2 by A7,A4,XXREAL_0:1;
proj2.:(north_halfline p) is bounded_below & C /\ north_halfline p c=
north_halfline p by Th3,XBOOLE_1:17;
then
A10: lower_bound(proj2.:(C /\ north_halfline p)) >=
lower_bound(proj2.:(north_halfline p ))
by A6,RELAT_1:123,SEQ_4:47;
lower_bound(proj2.:(north_halfline p)) = p`2 &
North-Bound(p,C)`2 = lower_bound(proj2.:
(C /\ north_halfline p)) by Th7,EUCLID:52;
hence thesis by A10,A8,XXREAL_0:1;
end;
theorem Th19:
for C being compact Subset of TOP-REAL 2 holds p in BDD C
implies lower_bound(proj2.:(C /\ north_halfline p)) >
upper_bound(proj2.:(C /\ south_halfline p
))
proof
let C be compact Subset of TOP-REAL 2;
assume p in BDD C;
then
A1: South-Bound(p,C)`2 < p`2 & p`2 < North-Bound(p,C)`2 by Th18;
North-Bound(p,C)`2 = lower_bound(proj2.:(C /\ north_halfline p))
& South-Bound(p
,C) `2 = upper_bound(proj2.:(C /\ south_halfline p)) by EUCLID:52;
hence thesis by A1,XXREAL_0:2;
end;
theorem
for C being compact Subset of TOP-REAL 2 holds p in BDD C implies
South-Bound(p,C) <> North-Bound(p,C)
proof
let C be compact Subset of TOP-REAL 2;
assume
A1: p in BDD C;
A2: North-Bound(p,C)`2 = lower_bound(proj2.:(C /\ north_halfline p))
& South-Bound(p
,C) `2 = upper_bound(proj2.:(C /\ south_halfline p)) by EUCLID:52;
assume not thesis;
hence thesis by A1,A2,Th19;
end;
theorem Th21:
for C being Subset of TOP-REAL 2 holds LSeg(North-Bound(p,C),
South-Bound(p,C)) is vertical
proof
let C be Subset of TOP-REAL 2;
North-Bound(p,C)`1 = p`1 & South-Bound(p,C)`1 = p`1 by EUCLID:52;
hence thesis by SPPOL_1:16;
end;
theorem
for C being compact Subset of TOP-REAL 2 holds p in BDD C implies LSeg
(North-Bound(p,C),South-Bound(p,C)) /\ C = { North-Bound(p,C), South-Bound(p,C)
}
proof
let C be compact Subset of TOP-REAL 2;
set L = LSeg(North-Bound(p,C),South-Bound(p,C));
assume
A1: p in BDD C;
then
A2: North-Bound(p,C) in C & South-Bound(p,C) in C by Th17;
hereby
A3: North-Bound(p,C)`2 = lower_bound(proj2.:(C /\ north_halfline p))
by EUCLID:52;
A4: South-Bound(p,C)`2 = upper_bound(proj2.:(C /\ south_halfline p))
by EUCLID:52;
let x be object;
A5: South-Bound(p,C)`1 = p`1 by EUCLID:52;
assume
A6: x in L /\ C;
then reconsider y = x as Point of TOP-REAL 2;
A7: x in L by A6,XBOOLE_0:def 4;
L is vertical & South-Bound(p,C) in L by Th21,RLTOPSP1:68;
then
A8: y`1 = p`1 by A5,A7,SPPOL_1:def 3;
A9: x in C by A6,XBOOLE_0:def 4;
A10: North-Bound(p,C)`1 = p`1 by EUCLID:52;
now
C /\ north_halfline p is bounded by TOPREAL6:89;
then proj2.:(C /\ north_halfline p) is real-bounded by JCT_MISC:14;
then
A11: proj2.:(C /\ north_halfline p) is bounded_below;
South-Bound(p,C)`2 < p`2 & p`2 < North-Bound(p,C)`2 by A1,Th18;
then
A12: South-Bound(p,C)`2 < North-Bound(p,C)`2 by XXREAL_0:2;
then
A13: South-Bound(p,C)`2 <= y`2 by A7,TOPREAL1:4;
assume y <> North-Bound(p,C);
then
A14: y`2 <> North-Bound(p,C)`2 by A10,A8,TOPREAL3:6;
A15: y`2 = proj2.y by PSCOMP_1:def 6;
y`2 <= North-Bound(p,C)`2 by A7,A12,TOPREAL1:4;
then
A16: y`2 < North-Bound(p,C)`2 by A14,XXREAL_0:1;
now
assume y`2 > p`2;
then y in north_halfline p by A8,TOPREAL1:def 10;
then y in C /\ north_halfline p by A9,XBOOLE_0:def 4;
then y`2 in proj2.:(C /\ north_halfline p) by A15,FUNCT_2:35;
hence contradiction by A3,A16,A11,SEQ_4:def 2;
end;
then y in south_halfline p by A8,TOPREAL1:def 12;
then y in C /\ south_halfline p by A9,XBOOLE_0:def 4;
then
A17: y`2 in proj2.:(C /\ south_halfline p) by A15,FUNCT_2:35;
C /\ south_halfline p is bounded by TOPREAL6:89;
then proj2.:(C /\ south_halfline p) is real-bounded by JCT_MISC:14;
then proj2.:(C /\ south_halfline p) is bounded_above;
then y`2 <= South-Bound(p,C)`2 by A4,A17,SEQ_4:def 1;
then y`2 = South-Bound(p,C)`2 by A13,XXREAL_0:1;
hence y = South-Bound(p,C) by A5,A8,TOPREAL3:6;
end;
hence x in {North-Bound(p,C),South-Bound(p,C)} by TARSKI:def 2;
end;
let x be object;
assume x in {North-Bound(p,C),South-Bound(p,C)};
then
A18: x = North-Bound(p,C) or x = South-Bound(p,C) by TARSKI:def 2;
then x in L by RLTOPSP1:68;
hence thesis by A18,A2,XBOOLE_0:def 4;
end;
theorem
for C being compact Subset of TOP-REAL 2 holds p in BDD C & q in BDD C
& p`1 <> q`1 implies North-Bound(p,C), South-Bound(q,C), North-Bound(q,C),
South-Bound(p,C) are_mutually_distinct
proof
let C be compact Subset of TOP-REAL 2;
set np = North-Bound(p,C), sq = South-Bound(q,C), nq = North-Bound(q,C), sp
= South-Bound(p,C);
A1: np`1 = p`1 & sp`1 = p`1 by EUCLID:52;
A2: North-Bound(q,C)`2 = lower_bound(proj2.:(C /\ north_halfline q)) &
South-Bound(q
,C) `2 = upper_bound(proj2.:(C /\ south_halfline q)) by EUCLID:52;
A3: North-Bound(p,C)`2 = lower_bound(proj2.:(C /\ north_halfline p)) &
South-Bound(p
,C) `2 = upper_bound(proj2.:(C /\ south_halfline p)) by EUCLID:52;
assume p in BDD C & q in BDD C & p`1 <> q`1;
hence np <> sq & np <> nq & np <> sp & sq <> nq & sq <> sp & nq <> sp by A1
,A2,A3,Th19,EUCLID:52;
end;
begin :: An Order of Points on a Simple Closed Curve
definition
let n,V,s1,s2,t1,t2;
pred s1,s2, V-separate t1,t2 means
for A being Subset of TOP-REAL n
st A is_an_arc_of s1,s2 & A c= V holds A meets {t1,t2};
end;
notation
let n,V,s1,s2,t1,t2;
antonym s1,s2 are_neighbours_wrt t1,t2, V for s1,s2, V-separate t1,t2;
end;
theorem
t,t, V-separate s1,s2
by JORDAN6:37;
theorem
s1,s2, V-separate t1,t2 implies s2,s1, V-separate t1,t2
by JORDAN5B:14;
theorem
s1,s2, V-separate t1,t2 implies s1,s2, V-separate t2,t1;
theorem Th27:
s,t1, V-separate s,t2
proof
let A be Subset of TOP-REAL n such that
A1: A is_an_arc_of s,t1 and
A c= V;
A2: s in {s,t2} by TARSKI:def 2;
s in A by A1,TOPREAL1:1;
hence thesis by A2,XBOOLE_0:3;
end;
theorem Th28:
t1,s, V-separate t2,s
proof
let A be Subset of TOP-REAL n such that
A1: A is_an_arc_of t1,s and
A c= V;
A2: s in {s,t2} by TARSKI:def 2;
s in A by A1,TOPREAL1:1;
hence thesis by A2,XBOOLE_0:3;
end;
theorem Th29:
t1,s, V-separate s,t2
proof
let A be Subset of TOP-REAL n such that
A1: A is_an_arc_of t1,s and
A c= V;
A2: s in {s,t2} by TARSKI:def 2;
s in A by A1,TOPREAL1:1;
hence thesis by A2,XBOOLE_0:3;
end;
theorem Th30:
s,t1, V-separate t2,s
proof
let A be Subset of TOP-REAL n such that
A1: A is_an_arc_of s,t1 and
A c= V;
A2: s in {s,t2} by TARSKI:def 2;
s in A by A1,TOPREAL1:1;
hence thesis by A2,XBOOLE_0:3;
end;
theorem
for p1,p2,q being Point of TOP-REAL 2 st q in C & p1 in C & p2 in C &
p1 <> p2 & p1 <> q & p2 <> q holds p1,p2 are_neighbours_wrt q,q, C
proof
let p1,p2,q be Point of TOP-REAL 2 such that
A1: q in C and
A2: p1 in C & p2 in C & p1 <> p2 and
A3: p1 <> q & p2 <> q;
consider P1,P2 being non empty Subset of TOP-REAL 2 such that
A4: P1 is_an_arc_of p1,p2 and
A5: P2 is_an_arc_of p1,p2 and
A6: C = P1 \/ P2 and
A7: P1 /\ P2 = {p1,p2} by A2,TOPREAL2:5;
per cases by A1,A6,XBOOLE_0:def 3;
suppose
A8: q in P1 & not q in P2;
take P2;
thus P2 is_an_arc_of p1,p2 by A5;
thus P2 c= C by A6,XBOOLE_1:7;
thus P2 misses {q,q} by A8,ZFMISC_1:51;
end;
suppose
A9: q in P2 & not q in P1;
take P1;
thus P1 is_an_arc_of p1,p2 by A4;
thus P1 c= C by A6,XBOOLE_1:7;
thus P1 misses {q,q} by A9,ZFMISC_1:51;
end;
suppose
q in P1 & q in P2;
then q in P1 /\ P2 by XBOOLE_0:def 4;
hence thesis by A3,A7,TARSKI:def 2;
end;
end;
theorem
p1 <> p2 & p1 in C & p2 in C implies (p1,p2, C-separate q1,q2 implies
q1,q2, C-separate p1,p2)
proof
assume that
A1: p1 <> p2 and
A2: p1 in C and
A3: p2 in C and
A4: p1,p2, C-separate q1,q2;
per cases;
suppose
q1 = p1;
hence thesis by Th27;
end;
suppose
q2 = p2;
hence thesis by Th28;
end;
suppose
q1 = p2;
hence thesis by Th30;
end;
suppose
p1 = q2;
hence thesis by Th29;
end;
suppose that
A5: q1 <> p1 & q2 <> p2 & q1 <> p2 & q2 <> p1;
let A be Subset of TOP-REAL 2;
assume A is_an_arc_of q1,q2 & A c= C;
then consider B being non empty Subset of TOP-REAL 2 such that
A6: B is_an_arc_of q1,q2 and
A7: A \/ B = C and
A /\ B = {q1,q2} by Th15;
assume
A8: A misses {p1,p2};
then not p2 in A by ZFMISC_1:49;
then
A9: p2 in B by A3,A7,XBOOLE_0:def 3;
not p1 in A by A8,ZFMISC_1:49;
then p1 in B by A2,A7,XBOOLE_0:def 3;
then consider P being non empty Subset of TOP-REAL 2 such that
A10: P is_an_arc_of p1,p2 and
A11: P c= B and
A12: P misses {q1,q2} by A1,A5,A6,A9,JORDAN16:23;
B c= C by A7,XBOOLE_1:7;
then P c= C by A11;
hence thesis by A4,A10,A12;
end;
end;
theorem
p1 in C & p2 in C & q1 in C & p1 <> p2 & q1 <> p1 & q1 <> p2 & q2 <>
p1 & q2 <> p2 implies p1,p2 are_neighbours_wrt q1,q2, C or p1,q1
are_neighbours_wrt p2,q2, C
proof
assume that
A1: p1 in C & p2 in C and
A2: q1 in C and
A3: p1 <> p2 and
A4: q1 <> p1 and
A5: q1 <> p2 and
A6: q2 <> p1 & q2 <> p2;
consider P,P1 being non empty Subset of TOP-REAL 2 such that
A7: P is_an_arc_of p1,p2 and
A8: P1 is_an_arc_of p1,p2 and
A9: C = P \/ P1 and
A10: P /\ P1 = {p1,p2} by A1,A3,TOPREAL2:5;
A11: P c= C by A9,XBOOLE_1:7;
assume
A12: for A being Subset of TOP-REAL 2 st A is_an_arc_of p1,p2 & A c= C
holds A meets {q1,q2};
then
A13: P meets {q1,q2} by A7,A9,XBOOLE_1:7;
A14: P1 c= C by A9,XBOOLE_1:7;
per cases by A13,ZFMISC_1:51;
suppose that
A15: q1 in P and
A16: not q2 in P;
now
take A = Segment(P,p1,p2,p1,q1);
A17: now
A18: A = {q where q is Point of TOP-REAL 2: LE p1,q,P,p1,p2 & LE q,q1,
P,p1,p2} by JORDAN6:26;
assume p2 in A;
then
ex q being Point of TOP-REAL 2 st p2 = q & LE p1,q,P,p1,p2 & LE q
,q1,P,p1,p2 by A18;
hence contradiction by A5,A7,JORDAN6:55;
end;
LE p1, q1, P, p1, p2 by A7,A15,JORDAN5C:10;
hence A is_an_arc_of p1,q1 by A4,A7,JORDAN16:21;
A19: A c= P by JORDAN16:2;
hence A c= C by A11;
not q2 in A by A16,A19;
hence A misses {p2,q2} by A17,ZFMISC_1:51;
end;
hence thesis;
end;
suppose that
A20: q2 in P and
A21: not q1 in P;
now
take A = Segment(P1,p1,p2,p1,q1);
A22: now
A23: A = {q where q is Point of TOP-REAL 2: LE p1,q,P1,p1,p2 & LE q,q1
,P1,p1,p2} by JORDAN6:26;
assume p2 in A;
then ex q being Point of TOP-REAL 2 st p2 = q & LE p1,q,P1,p1,p2 & LE
q,q1,P1,p1,p2 by A23;
hence contradiction by A5,A8,JORDAN6:55;
end;
q1 in P1 by A2,A9,A21,XBOOLE_0:def 3;
then LE p1, q1, P1, p1, p2 by A8,JORDAN5C:10;
hence A is_an_arc_of p1,q1 by A4,A8,JORDAN16:21;
A24: A c= P1 by JORDAN16:2;
hence A c= C by A14;
now
assume q2 in A;
then q2 in {p1,p2} by A10,A20,A24,XBOOLE_0:def 4;
hence contradiction by A6,TARSKI:def 2;
end;
hence A misses {p2,q2} by A22,ZFMISC_1:51;
end;
hence thesis;
end;
suppose that
A25: q1 in P & q2 in P;
P1 meets {q1,q2} by A12,A8,A9,XBOOLE_1:7;
then q1 in P1 or q2 in P1 by ZFMISC_1:51;
then q1 in {p1,p2} or q2 in {p1,p2} by A10,A25,XBOOLE_0:def 4;
hence thesis by A4,A5,A6,TARSKI:def 2;
end;
end;