:: On a Dividing Function of the Simple Closed Curve into Segments
:: by Yatsuka Nakamura
::
:: Received June 16, 1998
:: Copyright (c) 1998-2021 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, PRE_TOPC, EUCLID, ARYTM_1, SUBSET_1, XXREAL_0, ARYTM_3,
RCOMP_1, XBOOLE_0, TOPREAL2, PSCOMP_1, JORDAN6, TOPREAL1, JORDAN3,
TARSKI, FUNCT_1, BORSUK_1, RELAT_1, TOPS_2, ORDINAL2, STRUCT_0, FINSEQ_1,
CARD_1, XXREAL_1, REAL_1, PARTFUN1, MEASURE5, GOBRD10, ORDINAL4, NAT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
REAL_1, NAT_1, RCOMP_1, NAT_D, FINSEQ_1, FUNCT_1, RELSET_1, PARTFUN1,
VALUED_0, TOPREAL1, TOPREAL2, TBSP_1, GOBRD10, PRE_TOPC, TOPS_2,
FINSEQ_6, STRUCT_0, COMPTS_1, EUCLID, PSCOMP_1, JORDAN5C, JORDAN6,
TOPMETR, XXREAL_0;
constructors REAL_1, RCOMP_1, NAT_D, TOPS_2, COMPTS_1, TBSP_1, TOPMETR,
TOPREAL1, PSCOMP_1, GOBRD10, JORDAN5C, JORDAN6, XXREAL_2, FINSEQ_6;
registrations RELSET_1, XXREAL_0, XREAL_0, MEMBERED, STRUCT_0, PRE_TOPC,
EUCLID, TOPREAL1, BORSUK_2, VALUED_0, COMPTS_1, XXREAL_2, FINSEQ_1,
FUNCT_1, ORDINAL1;
requirements REAL, SUBSET, BOOLE, NUMERALS, ARITHM;
definitions TARSKI, XBOOLE_0, FUNCT_1;
equalities XBOOLE_0, STRUCT_0;
expansions TARSKI, XBOOLE_0, FUNCT_1;
theorems TARSKI, JORDAN6, TOPREAL1, TOPREAL5, JORDAN5C, UNIFORM1, PRE_TOPC,
FUNCT_2, TOPS_2, RELAT_1, FUNCT_1, FINSEQ_1, FINSEQ_2, NAT_1, FINSEQ_4,
GOBRD10, SPRECT_1, XBOOLE_0, XBOOLE_1, FINSEQ_3, BORSUK_1, COMPTS_1,
RELSET_1, JORDAN5B, PARTFUN2, XCMPLX_1, XREAL_1, XXREAL_0, PARTFUN1,
XXREAL_1, XXREAL_2, SEQM_3, NAT_D, XREAL_0, FINSEQ_6;
schemes DOMAIN_1, NAT_1;
begin :: Definition of the Segment and its property
reserve p,p1,p2,p3,q for Point of TOP-REAL 2;
Lm1: 2-'1 = 2-1 by XREAL_1:233
.=1;
Lm2: for i, j, k be Nat holds i-'k <= j implies i <= j + k
proof
let i, j, k be Nat;
assume
A1: i-'k <= j;
per cases;
suppose
A2: i >= k;
i-'k +k <= j + k by A1,XREAL_1:6;
hence thesis by A2,XREAL_1:235;
end;
suppose
A3: i <= k;
k <= j + k by NAT_1:11;
hence thesis by A3,XXREAL_0:2;
end;
end;
Lm3: for i, j, k be Nat holds j + k <= i implies k <= i -' j
proof
let i, j, k be Nat;
assume
A1: j + k <= i;
per cases by A1,XXREAL_0:1;
suppose
j + k = i;
hence thesis by NAT_D:34;
end;
suppose
j + k < i;
hence thesis by Lm2;
end;
end;
theorem Th1:
for P being compact non empty Subset of TOP-REAL 2 st P is
being_simple_closed_curve holds W-min(P) in Lower_Arc(P) & E-max(P) in
Lower_Arc(P) & W-min(P) in Upper_Arc(P) & E-max(P) in Upper_Arc(P)
proof
let P be compact non empty Subset of TOP-REAL 2;
assume P is being_simple_closed_curve;
then
Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) & Lower_Arc(P) is_an_arc_of
E-max(P),W-min(P) by JORDAN6:50;
hence thesis by TOPREAL1:1;
end;
theorem Th2:
for P being compact non empty Subset of TOP-REAL 2,q st P is
being_simple_closed_curve & LE q,W-min(P),P holds q=W-min(P)
proof
let P be compact non empty Subset of TOP-REAL 2,q;
assume P is being_simple_closed_curve & LE q,W-min(P),P;
then
LE q,W-min(P),Upper_Arc(P),W-min(P),E-max(P) & Upper_Arc(P) is_an_arc_of
W-min(P),E-max(P) by JORDAN6:def 8,def 10;
hence thesis by JORDAN6:54;
end;
theorem Th3:
for P being compact non empty Subset of TOP-REAL 2,q st P is
being_simple_closed_curve & q in P holds LE W-min(P),q,P
proof
let P be compact non empty Subset of TOP-REAL 2,q;
assume that
A1: P is being_simple_closed_curve and
A2: q in P;
A3: q in Upper_Arc(P) \/ Lower_Arc(P) by A1,A2,JORDAN6:50;
A4: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by A1,JORDAN6:50;
A5: W-min(P) in Upper_Arc(P) by A1,Th1;
per cases by A3,XBOOLE_0:def 3;
suppose
A6: q in Upper_Arc(P);
then LE W-min(P),q,Upper_Arc(P),W-min(P),E-max(P) by A4,JORDAN5C:10;
hence thesis by A5,A6,JORDAN6:def 10;
end;
suppose
A7: q in Lower_Arc(P);
per cases;
suppose
not q=W-min(P);
hence thesis by A5,A7,JORDAN6:def 10;
end;
suppose
A8: q=W-min(P);
then LE W-min(P),q,Upper_Arc(P),W-min(P),E-max(P) by A5,JORDAN5C:9;
hence thesis by A5,A8,JORDAN6:def 10;
end;
end;
end;
definition
let P be compact non empty Subset of TOP-REAL 2, q1,q2 be Point of TOP-REAL
2;
func Segment(q1,q2,P) -> Subset of TOP-REAL 2 equals
:Def1:
{p: LE q1,p,P &
LE p,q2,P} if q2<>W-min(P) otherwise {p1: LE q1,p1,P or q1 in P & p1=W-min(P)};
correctness
proof
ex B being Subset of TOP-REAL 2 st (q2<>W-min(P) implies B={p: LE q1,p
,P & LE p,q2,P})& (not q2<>W-min(P) implies B={p1: LE q1,p1,P or q1 in P & p1=
W-min(P)})
proof
per cases;
suppose
A1: q2<>W-min(P);
defpred P[Point of TOP-REAL 2] means LE q1,$1,P & LE $1,q2,P;
{p: P[p]} is Subset of TOP-REAL 2 from DOMAIN_1:sch 7;
then reconsider
C = {p: LE q1,p,P & LE p,q2,P} as Subset of TOP-REAL 2;
q2<>W-min(P) implies C={p: LE q1,p,P & LE p,q2,P};
hence thesis by A1;
end;
suppose
A2: not q2<>W-min(P);
defpred P[Point of TOP-REAL 2] means LE q1,$1,P or q1 in P & $1=W-min(
P);
{p1: P[p1]} is Subset of TOP-REAL 2 from DOMAIN_1:sch 7;
then reconsider
C = {p1: LE q1,p1,P or q1 in P & p1=W-min(P)} as Subset of
TOP-REAL 2;
not q2<>W-min(P) implies C={p1: LE q1,p1,P or q1 in P & p1=W-min(P )};
hence thesis by A2;
end;
end;
hence thesis;
end;
end;
theorem
for P being compact non empty Subset of TOP-REAL 2 st P is
being_simple_closed_curve holds Segment(W-min(P),E-max(P),P)=Upper_Arc(P) &
Segment(E-max(P),W-min(P),P)=Lower_Arc(P)
proof
let P be compact non empty Subset of TOP-REAL 2;
assume
A1: P is being_simple_closed_curve;
then
A2: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by JORDAN6:def 8;
A3: {p1: LE E-max(P),p1,P or E-max(P) in P & p1=W-min(P)} = Lower_Arc(P)
proof
A4: {p1: LE E-max(P),p1,P or E-max(P) in P & p1=W-min(P)} c= Lower_Arc(P)
proof
let x be object;
assume x in {p1: LE E-max(P),p1,P or E-max(P) in P & p1=W-min(P)};
then consider p1 such that
A5: p1=x and
A6: LE E-max(P),p1,P or E-max(P) in P & p1=W-min(P);
per cases by A6;
suppose
A7: LE E-max(P),p1,P;
per cases by A5,A7,JORDAN6:def 10;
suppose
x in Lower_Arc(P);
hence thesis;
end;
suppose
A8: E-max(P) in Upper_Arc(P) & p1 in Upper_Arc(P) & LE E-max(P)
,p1,Upper_Arc(P),W-min(P),E-max(P);
A9: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by A1,JORDAN6:50;
then LE p1,E-max(P),Upper_Arc(P),W-min(P),E-max(P) by A8,JORDAN5C:10;
then
A10: p1=E-max(P) by A8,A9,JORDAN5C:12;
Lower_Arc(P) is_an_arc_of E-max(P),W-min(P) by A1,JORDAN6:def 9;
hence thesis by A5,A10,TOPREAL1:1;
end;
end;
suppose
E-max(P) in P & p1=W-min(P);
then x in {W-min(P),E-max(P)} by A5,TARSKI:def 2;
then x in Upper_Arc(P) /\ Lower_Arc(P) by A1,JORDAN6:def 9;
hence thesis by XBOOLE_0:def 4;
end;
end;
Lower_Arc(P) c= {p1: LE E-max(P),p1,P or E-max(P) in P & p1=W-min(P) }
proof
let x be object;
assume
A11: x in Lower_Arc(P);
then reconsider p2=x as Point of TOP-REAL 2;
Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by A1,JORDAN6:50;
then
not (E-max P in P & p2=W-min P) implies E-max P in Upper_Arc P & p2
in Lower_Arc P & not p2=W-min P by A11,SPRECT_1:14,TOPREAL1:1;
then LE E-max(P),p2,P or E-max P in P & p2=W-min P by JORDAN6:def 10;
hence thesis;
end;
hence thesis by A4;
end;
A12: E-max(P)<>W-min(P) by A1,TOPREAL5:19;
{p: LE W-min(P),p,P & LE p,E-max(P),P} = Upper_Arc(P)
proof
A13: {p: LE W-min(P),p,P & LE p,E-max(P),P} c= Upper_Arc(P)
proof
let x be object;
assume x in {p: LE W-min(P),p,P & LE p,E-max(P),P};
then consider p such that
A14: p=x and
LE W-min(P),p,P and
A15: LE p,E-max(P),P;
per cases by A15,JORDAN6:def 10;
suppose
p in Upper_Arc(P) & E-max(P) in Lower_Arc(P) & not E-max(P)= W-min(P);
hence thesis by A14;
end;
suppose
p in Upper_Arc(P) & E-max(P) in Upper_Arc(P) & LE p,E-max(P),
Upper_Arc(P),W-min(P),E-max(P);
hence thesis by A14;
end;
suppose
A16: p in Lower_Arc(P) & E-max(P) in Lower_Arc(P) & not E-max(P)=
W-min(P) & LE p,E-max(P),Lower_Arc(P),E-max(P),W-min(P);
Lower_Arc(P) is_an_arc_of E-max(P),W-min(P) by A1,JORDAN6:def 9;
then p=E-max(P) by A16,JORDAN6:54;
hence thesis by A2,A14,TOPREAL1:1;
end;
end;
Upper_Arc(P) c= {p: LE W-min(P),p,P & LE p,E-max(P),P}
proof
let x be object;
assume
A17: x in Upper_Arc(P);
then reconsider p2=x as Point of TOP-REAL 2;
E-max(P) in Lower_Arc(P) by A1,Th1;
then
A18: LE p2,E-max(P),P by A12,A17,JORDAN6:def 10;
A19: W-min(P) in Upper_Arc(P) by A1,Th1;
LE W-min(P),p2,Upper_Arc(P),W-min(P),E-max(P) by A2,A17,JORDAN5C:10;
then LE W-min(P),p2,P by A17,A19,JORDAN6:def 10;
hence thesis by A18;
end;
hence thesis by A13;
end;
hence thesis by A12,A3,Def1;
end;
theorem Th5:
for P being compact non empty Subset of TOP-REAL 2, q1,q2 being
Point of TOP-REAL 2 st P is being_simple_closed_curve & LE q1,q2,P holds q1 in
P & q2 in P
proof
let P be compact non empty Subset of TOP-REAL 2, q1,q2 be Point of TOP-REAL
2;
assume that
A1: P is being_simple_closed_curve and
A2: LE q1,q2,P;
A3: Upper_Arc(P) \/ Lower_Arc(P)=P by A1,JORDAN6:50;
per cases by A2,JORDAN6:def 10;
suppose
q1 in Upper_Arc(P) & q2 in Lower_Arc(P);
hence thesis by A3,XBOOLE_0:def 3;
end;
suppose
q1 in Upper_Arc(P) & q2 in Upper_Arc(P);
hence thesis by A3,XBOOLE_0:def 3;
end;
suppose
q1 in Lower_Arc(P) & q2 in Lower_Arc(P);
hence thesis by A3,XBOOLE_0:def 3;
end;
end;
theorem Th6:
for P being compact non empty Subset of TOP-REAL 2, q1,q2 being
Point of TOP-REAL 2 st P is being_simple_closed_curve & LE q1,q2,P holds q1 in
Segment(q1,q2,P) & q2 in Segment(q1,q2,P)
proof
let P be compact non empty Subset of TOP-REAL 2, q1,q2 be Point of TOP-REAL
2;
assume that
A1: P is being_simple_closed_curve and
A2: LE q1,q2,P;
hereby
per cases;
suppose
A3: q2<>W-min(P);
q1 in P by A1,A2,Th5;
then LE q1,q1,P by A1,JORDAN6:56;
then q1 in {p: LE q1,p,P & LE p,q2,P} by A2;
hence q1 in Segment(q1,q2,P) by A3,Def1;
end;
suppose
A4: q2=W-min(P);
q1 in P by A1,A2,Th5;
then LE q1,q1,P by A1,JORDAN6:56;
then q1 in {p1: LE q1,p1,P or q1 in P & p1=W-min(P)};
hence q1 in Segment(q1,q2,P) by A4,Def1;
end;
end;
per cases;
suppose
A5: q2<>W-min(P);
q2 in P by A1,A2,Th5;
then LE q2,q2,P by A1,JORDAN6:56;
then q2 in {p: LE q1,p,P & LE p,q2,P} by A2;
hence thesis by A5,Def1;
end;
suppose
A6: q2=W-min(P);
q2 in {p1: LE q1,p1,P or q1 in P & p1=W-min(P)} by A2;
hence thesis by A6,Def1;
end;
end;
theorem Th7:
for P being compact non empty Subset of TOP-REAL 2, q1 being
Point of TOP-REAL 2 st q1 in P & P is being_simple_closed_curve holds q1 in
Segment(q1,W-min P,P)
proof
let P be compact non empty Subset of TOP-REAL 2, q1 be Point of TOP-REAL 2
such that
A1: q1 in P;
assume P is being_simple_closed_curve;
then LE q1,q1,P by A1,JORDAN6:56;
then q1 in {p1: LE q1,p1,P or q1 in P & p1=W-min(P)};
hence thesis by Def1;
end;
theorem
for P being compact non empty Subset of TOP-REAL 2, q being Point of
TOP-REAL 2 st P is being_simple_closed_curve & q in P & q<>W-min(P) holds
Segment(q,q,P)={q}
proof
let P be compact non empty Subset of TOP-REAL 2, q be Point of TOP-REAL 2;
assume that
A1: P is being_simple_closed_curve and
A2: q in P and
A3: q <> W-min P;
for x being object holds x in Segment(q,q,P) iff x=q
proof
let x be object;
hereby
assume x in Segment(q,q,P);
then x in {p: LE q,p,P & LE p,q,P} by A3,Def1;
then ex p st p=x & LE q,p,P & LE p,q,P;
hence x=q by A1,JORDAN6:57;
end;
assume
A4: x=q;
LE q,q,P by A1,A2,JORDAN6:56;
then x in {p: LE q,p,P & LE p,q,P} by A4;
hence thesis by A3,Def1;
end;
hence thesis by TARSKI:def 1;
end;
theorem
for P being compact non empty Subset of TOP-REAL 2, q1,q2 being Point
of TOP-REAL 2 st P is being_simple_closed_curve & q1<>W-min(P) & q2<>W-min(P)
holds not W-min(P) in Segment(q1,q2,P)
proof
let P be compact non empty Subset of TOP-REAL 2, q1,q2 be Point of TOP-REAL
2;
assume that
A1: P is being_simple_closed_curve and
A2: q1<>W-min(P) and
A3: q2<>W-min(P);
A4: Segment(q1,q2,P)={p: LE q1,p,P & LE p,q2,P} by A3,Def1;
now
A5: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by A1,JORDAN6:def 8;
assume W-min(P) in Segment(q1,q2,P);
then consider p such that
A6: p=W-min(P) and
A7: LE q1,p,P and
LE p,q2,P by A4;
LE q1,p,Upper_Arc(P),W-min(P),E-max(P) by A6,A7,JORDAN6:def 10;
hence contradiction by A2,A6,A5,JORDAN6:54;
end;
hence thesis;
end;
theorem Th10:
for P being compact non empty Subset of TOP-REAL 2, q1,q2,q3
being Point of TOP-REAL 2 st P is being_simple_closed_curve & LE q1,q2,P & LE
q2,q3,P & not(q1=q2 & q1=W-min(P)) & not(q2=q3 & q2=W-min(P)) holds Segment(q1,
q2,P)/\ Segment(q2,q3,P)={q2}
proof
let P be compact non empty Subset of TOP-REAL 2, q1,q2,q3 be Point of
TOP-REAL 2;
assume that
A1: P is being_simple_closed_curve and
A2: LE q1,q2,P and
A3: LE q2,q3,P and
A4: not(q1=q2 & q1=W-min(P)) and
A5: not(q2=q3 & q2=W-min(P));
A6: Upper_Arc(P) is_an_arc_of W-min(P),E-max(P) by A1,JORDAN6:def 8;
thus Segment(q1,q2,P)/\ Segment(q2,q3,P) c= {q2}
proof
let x be object;
assume
A7: x in Segment(q1,q2,P)/\ Segment(q2,q3,P);
then
A8: x in Segment(q2,q3,P) by XBOOLE_0:def 4;
A9: x in Segment(q1,q2,P) by A7,XBOOLE_0:def 4;
now
per cases;
case
q3<>W-min(P);
then x in {p: LE q2,p,P & LE p,q3,P} by A8,Def1;
then
A10: ex p st p=x & LE q2,p,P & LE p,q3,P;
per cases;
suppose
q2<>W-min(P);
then x in {p2: LE q1,p2,P & LE p2,q2,P} by A9,Def1;
then ex p2 st p2=x & LE q1,p2,P & LE p2,q2,P;
hence x=q2 by A1,A10,JORDAN6:57;
end;
suppose
A11: q2=W-min(P);
then LE q1,q2,Upper_Arc(P),W-min(P),E-max(P) by A2,JORDAN6:def 10;
hence x=q2 by A4,A6,A11,JORDAN6:54;
end;
end;
case
A12: q3=W-min(P);
then x in {p1: LE q2,p1,P or q2 in P & p1=W-min(P)} by A8,Def1;
then consider p1 such that
A13: p1=x and
A14: LE q2,p1,P or q2 in P & p1=W-min(P);
p1 in {p: LE q1,p,P & LE p,q2,P} by A5,A9,A12,A13,Def1;
then ex p st p=p1 & LE q1,p,P & LE p,q2,P;
hence x=q2 by A1,A3,A12,A13,A14,JORDAN6:57;
end;
end;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {q2};
then x=q2 by TARSKI:def 1;
then x in Segment(q1,q2,P) & x in Segment(q2,q3,P) by A1,A2,A3,Th6;
hence thesis by XBOOLE_0:def 4;
end;
theorem Th11:
for P being compact non empty Subset of TOP-REAL 2, q1,q2 being
Point of TOP-REAL 2 st P is being_simple_closed_curve & LE q1,q2,P & q1 <>
W-min P & q2 <> W-min P holds Segment(q1,q2,P)/\ Segment(q2,W-min P,P)={q2}
proof
let P be compact non empty Subset of TOP-REAL 2, q1,q2 be Point of TOP-REAL
2;
set q3 = W-min P;
assume that
A1: P is being_simple_closed_curve and
A2: LE q1,q2,P and
A3: q1<>q3 and
A4: not q2=W-min(P);
thus Segment(q1,q2,P)/\ Segment(q2,W-min P,P) c= {q2}
proof
let x be object;
assume
A5: x in Segment(q1,q2,P)/\ Segment(q2,q3,P);
then x in Segment(q2,q3,P) by XBOOLE_0:def 4;
then x in {p1: LE q2,p1,P or q2 in P & p1=W-min P} by Def1;
then consider p1 such that
A6: p1=x and
A7: LE q2,p1,P or q2 in P & p1=W-min P;
x in Segment(q1,q2,P) by A5,XBOOLE_0:def 4;
then p1 in {p: LE q1,p,P & LE p,q2,P} by A4,A6,Def1;
then
A8: ex p st p=p1 & LE q1,p,P & LE p,q2,P;
per cases by A7;
suppose
LE q2,p1,P;
then x=q2 by A1,A6,A8,JORDAN6:57;
hence thesis by TARSKI:def 1;
end;
suppose
q2 in P & p1=W-min(P);
hence thesis by A1,A3,A8,Th2;
end;
end;
let x be object;
assume x in {q2};
then
A9: x=q2 by TARSKI:def 1;
q2 in P by A1,A2,Th5;
then
A10: x in Segment(q2,q3,P) by A1,A9,Th7;
x in Segment(q1,q2,P) by A1,A2,A9,Th6;
hence thesis by A10,XBOOLE_0:def 4;
end;
theorem Th12:
for P being compact non empty Subset of TOP-REAL 2, q1,q2 being
Point of TOP-REAL 2 st P is being_simple_closed_curve & LE q1,q2,P & q1<>q2 &
q1<>W-min(P) holds Segment(q2,W-min(P),P)/\ Segment(W-min(P),q1,P)={W-min(P)}
proof
let P be compact non empty Subset of TOP-REAL 2, q1,q2 be Point of TOP-REAL
2;
assume that
A1: P is being_simple_closed_curve and
A2: LE q1,q2,P and
A3: q1<>q2 and
A4: q1<>W-min(P);
thus Segment(q2,W-min(P),P)/\ Segment(W-min(P),q1,P) c= {W-min(P)}
proof
let x be object;
assume
A5: x in Segment(q2,W-min(P),P)/\ Segment(W-min(P),q1,P);
then x in Segment(q2,W-min(P),P) by XBOOLE_0:def 4;
then x in {p1: LE q2,p1,P or q2 in P & p1=W-min(P)} by Def1;
then consider p1 such that
A6: p1=x and
A7: LE q2,p1,P or q2 in P & p1=W-min(P);
A8: x in Segment(W-min(P),q1,P) by A5,XBOOLE_0:def 4;
now
per cases by A7;
case
A9: LE q2,p1,P;
x in {p: LE W-min(P),p,P & LE p,q1,P} by A4,A8,Def1;
then ex p2 st p2=x & LE W-min(P),p2,P & LE p2,q1,P;
then LE q2,q1,P by A1,A6,A9,JORDAN6:58;
hence contradiction by A1,A2,A3,JORDAN6:57;
end;
case
q2 in P & p1=W-min(P);
hence x=W-min(P) by A6;
end;
end;
hence thesis by TARSKI:def 1;
end;
let x be object;
assume x in {W-min(P)};
then
A10: x=W-min(P) by TARSKI:def 1;
q2 in P by A1,A2,Th5;
then x in {p1: LE q2,p1,P or q2 in P & p1=W-min(P)} by A10;
then
A11: x in Segment(q2,W-min(P),P) by Def1;
q1 in P by A1,A2,Th5;
then LE W-min(P),q1,P by A1,Th3;
then x in Segment(W-min(P),q1,P) by A1,A10,Th6;
hence thesis by A11,XBOOLE_0:def 4;
end;
theorem Th13:
for P being compact non empty Subset of TOP-REAL 2, q1,q2,q3,q4
being Point of TOP-REAL 2 st P is being_simple_closed_curve & LE q1,q2,P & LE
q2,q3,P & LE q3,q4,P & q1<>q2 & q2<>q3 holds Segment(q1,q2,P) misses Segment(q3
,q4,P)
proof
let P be compact non empty Subset of TOP-REAL 2, q1,q2,q3,q4 be Point of
TOP-REAL 2;
assume that
A1: P is being_simple_closed_curve and
A2: LE q1,q2,P and
A3: LE q2,q3,P and
A4: LE q3,q4,P and
A5: q1<>q2 and
A6: q2<>q3;
set x = the Element of Segment(q1,q2,P)/\ Segment(q3,q4,P);
assume
A7: Segment(q1,q2,P)/\ Segment(q3,q4,P)<>{};
then
A8: x in Segment(q1,q2,P) by XBOOLE_0:def 4;
A9: x in Segment(q3,q4,P) by A7,XBOOLE_0:def 4;
per cases;
suppose
q4=W-min(P);
then q3=W-min(P) by A1,A4,Th2;
hence contradiction by A1,A3,A6,Th2;
end;
suppose
A10: q4<>W-min(P);
q2<>W-min(P) by A1,A2,A5,Th2;
then x in {p2: LE q1,p2,P & LE p2,q2,P} by A8,Def1;
then
A11: ex p2 st p2=x & LE q1,p2,P & LE p2,q2,P;
x in {p1: LE q3,p1,P & LE p1,q4,P} by A9,A10,Def1;
then ex p1 st p1=x & LE q3,p1,P & LE p1,q4,P;
then LE q3,q2,P by A1,A11,JORDAN6:58;
hence contradiction by A1,A3,A6,JORDAN6:57;
end;
end;
theorem Th14:
for P being compact non empty Subset of TOP-REAL 2, q1,q2,q3
being Point of TOP-REAL 2 st P is being_simple_closed_curve & LE q1,q2,P & LE
q2,q3,P & q1<>W-min P & q2<>q3 holds Segment(q1,q2,P) misses Segment(q3,W-min P
,P)
proof
let P be compact non empty Subset of TOP-REAL 2, q1,q2,q3 be Point of
TOP-REAL 2;
assume that
A1: P is being_simple_closed_curve and
A2: LE q1,q2,P and
A3: LE q2,q3,P and
A4: q1<>W-min P and
A5: q2<>q3;
set x = the Element of Segment(q1,q2,P)/\ Segment(q3,W-min P,P);
assume
A6: Segment(q1,q2,P)/\ Segment(q3,W-min P,P)<>{};
then
A7: x in Segment(q1,q2,P) by XBOOLE_0:def 4;
x in Segment(q3,W-min P,P) by A6,XBOOLE_0:def 4;
then x in {p1: LE q3,p1,P or q3 in P & p1=W-min P} by Def1;
then
A8: ex p1 st p1=x &( LE q3,p1,P or q3 in P & p1=W-min P);
q2 <> W-min P by A1,A2,A4,Th2;
then x in {p: LE q1,p,P & LE p,q2,P} by A7,Def1;
then ex p3 st p3 = x & LE q1,p3,P & LE p3,q2,P;
then LE q3,q2,P by A1,A4,A8,Th2,JORDAN6:58;
hence contradiction by A1,A3,A5,JORDAN6:57;
end;
begin :: A function to divide the simple closed curve
reserve n for Nat;
theorem Th15:
for P being non empty Subset of TOP-REAL n, f being Function of
I[01], (TOP-REAL n)|P st f is being_homeomorphism ex g being Function of I[01],
TOP-REAL n st f=g & g is continuous & g is one-to-one
proof
let P be non empty Subset of TOP-REAL n, f be Function of I[01], (TOP-REAL n
)|P;
A1: [#]((TOP-REAL n)|P)= P by PRE_TOPC:def 5;
the carrier of (TOP-REAL n)|P = [#]((TOP-REAL n)|P) .=P by PRE_TOPC:def 5;
then reconsider g1=f as Function of I[01],TOP-REAL n by FUNCT_2:7;
assume
A2: f is being_homeomorphism;
then
A3: f is one-to-one by TOPS_2:def 5;
A4: [#]((TOP-REAL n)|P) <> {} & f is continuous by A2,TOPS_2:def 5;
A5: for P2 being Subset of TOP-REAL n st P2 is open holds g1"P2 is open
proof
let P2 be Subset of TOP-REAL n;
reconsider B1=P2 /\ P as Subset of (TOP-REAL n)|P by A1,XBOOLE_1:17;
f"(rng f) c= f"P by A1,RELAT_1:143;
then
A6: dom f c= f"P by RELAT_1:134;
assume P2 is open;
then B1 is open by A1,TOPS_2:24;
then
A7: f"B1 is open by A4,TOPS_2:43;
f"P c= dom f by RELAT_1:132;
then f"B1 = f"P2 /\ f"P & f"P=dom f by A6,FUNCT_1:68;
hence thesis by A7,RELAT_1:132,XBOOLE_1:28;
end;
[#]TOP-REAL n <> {};
then g1 is continuous by A5,TOPS_2:43;
hence thesis by A3;
end;
theorem Th16:
for P being non empty Subset of TOP-REAL n, g being Function of
I[01], (TOP-REAL n) st g is continuous one-to-one & rng g = P ex f being
Function of I[01],(TOP-REAL n)|P st f=g & f is being_homeomorphism
proof
let P be non empty Subset of TOP-REAL n, g be Function of I[01], TOP-REAL n;
assume that
A1: g is continuous one-to-one and
A2: rng g = P;
the carrier of (TOP-REAL n)|P = [#]((TOP-REAL n)|P);
then
A3: the carrier of (TOP-REAL n)|P = P by PRE_TOPC:def 5;
then reconsider f=g as Function of I[01],(TOP-REAL n)|P by A2,FUNCT_2:6;
take f;
thus f = g;
A4: [#]((TOP-REAL n)|P)= P by PRE_TOPC:def 5;
A5: dom f = the carrier of I[01] by FUNCT_2:def 1
.= [#]I[01];
A6: [#]TOP-REAL n<>{};
for P2 being Subset of (TOP-REAL n)|P st P2 is open holds f"P2 is open
proof
let P2 be Subset of (TOP-REAL n)|P;
assume P2 is open;
then consider C being Subset of TOP-REAL n such that
A7: C is open and
A8: C /\ [#]((TOP-REAL n)|P) = P2 by TOPS_2:24;
g"P = [#]I[01] by A3,A5,RELSET_1:22;
then f"P2 = f"C /\ [#]I[01] by A4,A8,FUNCT_1:68
.= f"C by XBOOLE_1:28;
hence thesis by A1,A6,A7,TOPS_2:43;
end;
then
A9: f is continuous by A4,TOPS_2:43;
rng f = [#]((TOP-REAL n)|P) by A2,PRE_TOPC:def 5;
hence thesis by A1,A9,COMPTS_1:17;
end;
Lm4: now
let h2 be Nat;
h2
0
ex h being FinSequence of the carrier of TOP-REAL 2
st h.1=W-min(P) & h is one-to-one & 8<=len h & rng h c= P &(for i
being Nat st 1<=i & i 0;
A3: Upper_Arc P is_an_arc_of W-min P, E-max P by A1,JORDAN6:def 8;
then consider g1 being Function of I[01], TOP-REAL 2 such that
A4: g1 is continuous one-to-one and
A5: rng g1 = Upper_Arc P and
A6: g1.0 = W-min P and
A7: g1.1 = E-max P by Th17;
consider h1 being FinSequence of REAL such that
A8: h1.1=0 and
A9: h1.len h1=1 and
A10: 5<=len h1 and
A11: rng h1 c= the carrier of I[01] and
A12: h1 is increasing and
A13: for i being Nat,Q being Subset of I[01], W being Subset
of Euclid 2 st 1<=i & i 1+1+1 by A39,A47,A36,A52,A55,A57,XXREAL_0:2;
then
A60: len h0-'1 > 1+1 by Lm2;
then
A61: 1len h1 by NAT_1:13;
then
A66: 1len h1;
A93: 0+2<=ny-'len h11 +2 by XREAL_1:6;
then
A94: 1<=(ny-'len h11 +2-'1) by Lm1,NAT_D:42;
len h1 +1<=ny by A92,NAT_1:13;
then
A95: len h1 +1-len h1<=ny-len h1 by XREAL_1:9;
then 1<=ny-'len h11 by A39,A92,XREAL_1:233;
then 1+1<=ny-'len h11+1+1-1 by XREAL_1:6;
then
A96: 2<=ny-'len h11+2-'1 by A93,Lm1,NAT_D:39,42;
A97: ny-len h11=ny-'len h11 by A39,A92,XREAL_1:233;
ny-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A85,
XREAL_1:9;
then
A98: ny-'len h11+2<=len h2-2+2 by A39,A97,XREAL_1:6;
then (ny-'len h11 +2-'1)<=len h21 by A47,NAT_D:44;
then
A99: (ny-'len h11 +2-'1) in dom h21 by A94,FINSEQ_3:25;
ny-'len h11+2-1<=len h2-1 by A98,XREAL_1:9;
then
A100: ny-'len h11+2-'1<=len h2-1 by A93,Lm1,NAT_D:39,42;
A101: ny<=len h11 + len (mid(h21,2,len h21 -'1)) by A85,FINSEQ_1:22;
then
A102: ny-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by XREAL_1:9
;
len h11+1<=ny by A39,A92,NAT_1:13;
then
A103: h0.ny=(mid(h21,2,len h21 -'1)).(ny -len h11) by A101,FINSEQ_1:23;
then
A104: h0.ny=h21.(ny-'len h11 +2-'1) by A39,A48,A56,A50,A54,A97,A102,A95,
FINSEQ_6:118;
then h0.ny in rng h21 by A99,FUNCT_1:def 3;
then h0.ny in rng g2 by FUNCT_1:14;
then h0.nx in Upper_Arc(P)/\ Lower_Arc(P) by A23,A81,A89,XBOOLE_0:def 4
;
then
A105: h0.nx in {W-min(P),E-max(P)} by A1,JORDAN6:50;
per cases by A105,TARSKI:def 2;
suppose
h0.nx=W-min(P);
then h21.(ny-'len h11 +2-'1)=W-min(P) by A39,A48,A56,A50,A54,A81,A103
,A97,A102,A95,FINSEQ_6:118;
then len h21=(ny-'len h11 +2-'1) by A46,A47,A34,A35,A32,A99;
then len h21+1<=len h21-1+1 by A47,A100,XREAL_1:6;
then len h21+1-len h21<=len h21 -len h21 by XREAL_1:9;
then len h21+1-len h21<=0;
hence thesis;
end;
suppose
h0.nx=E-max(P);
then 1=(ny-'len h11 +2-'1) by A46,A76,A77,A32,A81,A104,A99;
hence thesis by A96;
end;
end;
end;
suppose
A106: nx>len h1;
then len h1 +1<=nx by NAT_1:13;
then
A107: len h1 +1-len h1<=nx-len h1 by XREAL_1:9;
then 1<=nx-'len h11 by A39,A106,XREAL_1:233;
then
A108: 1+1<=nx-'len h11+1+1-1 by XREAL_1:6;
A109: nx<=len h11 + len (mid(h21,2,len h21 -'1)) by A83,FINSEQ_1:22;
then
A110: nx-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by XREAL_1:9;
A111: nx-len h11=nx-'len h11 by A39,A106,XREAL_1:233;
nx-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A83,
XREAL_1:9;
then
A112: nx-'len h11+2<=len h2-2+2 by A39,A111,XREAL_1:6;
then
A113: nx-'len h11+2-1<=len h2-1 by XREAL_1:9;
A114: (nx-'len h11 +2-'1)<=len h21 by A47,A112,NAT_D:44;
A115: 0+2<=nx-'len h11 +2 by XREAL_1:6;
then 1<=(nx-'len h11 +2-'1) by Lm1,NAT_D:42;
then
A116: (nx-'len h11 +2-'1) in dom h21 by A114,FINSEQ_3:25;
len h11+1<=nx by A39,A106,NAT_1:13;
then
A117: h0.nx=(mid(h21,2,len h21 -'1)).(nx -len h11) by A109,FINSEQ_1:23;
then
A118: h0.nx=h21.(nx-'len h11 +2-'1) by A39,A48,A56,A50,A54,A111,A110,A107,
FINSEQ_6:118;
then h0.nx in rng h21 by A116,FUNCT_1:def 3;
then
A119: h0.nx in Lower_Arc(P) by A23,FUNCT_1:14;
per cases;
suppose
ny<=len h1;
then
A120: ny in dom h1 by A84,FINSEQ_3:25;
then
A121: h1.ny in rng h1 by FUNCT_1:def 3;
h0.ny=h11.ny by A38,A120,FINSEQ_1:def 7
.=g1.(h1.ny) by A38,A120,FUNCT_1:12;
then h0.ny in rng g1 by A37,A121,FUNCT_1:def 3;
then h0.ny in Upper_Arc(P)/\ Lower_Arc(P) by A5,A81,A119,XBOOLE_0:def 4
;
then
A122: h0.ny in {W-min(P),E-max(P)} by A1,JORDAN6:50;
A123: nx-'len h11+2-'1<=len h2-1 by A115,A113,Lm1,NAT_D:39,42;
A124: 2<=nx-'len h11+2-'1 by A108,A115,Lm1,NAT_D:39,42;
per cases by A122,TARSKI:def 2;
suppose
h0.ny=W-min(P);
then len h21=(nx-'len h11 +2-'1) by A46,A47,A34,A35,A32,A81,A118,A116
;
then len h21+1<=len h21-1+1 by A47,A123,XREAL_1:6;
then len h21+1-len h21<=len h21 -len h21 by XREAL_1:9;
then len h21+1-len h21<=0;
hence thesis;
end;
suppose
h0.ny=E-max(P);
then h21.(nx-'len h11 +2-'1)=E-max(P) by A39,A48,A56,A50,A54,A81,A117
,A111,A110,A107,FINSEQ_6:118;
then 1=(nx-'len h11 +2-'1) by A46,A76,A77,A32,A116;
hence thesis by A124;
end;
end;
suppose
A125: ny>len h1;
then
A126: ny-len h11=ny-'len h11 by A39,XREAL_1:233;
len h1 +1<=ny by A125,NAT_1:13;
then
A127: h0.ny=(mid(h21,2,len h21 -'1)).(ny -len h11) & len h1 +1-len h1
<=ny-len h1 by A39,A36,A85,FINSEQ_1:23,XREAL_1:9;
0+2<=ny-'len h11 +2 by XREAL_1:6;
then
A128: 1<=(ny-'len h11 +2-'1) by Lm1,NAT_D:42;
ny-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36,A85,
XREAL_1:9;
then
A129: h0.ny=h21.(ny-'len h11 +2-'1) by A39,A48,A56,A50,A54,A126,A127,
FINSEQ_6:118;
ny-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A85,
XREAL_1:9;
then ny-'len h11+2<=len h2-2+2 by A39,A126,XREAL_1:6;
then (ny-'len h11 +2-'1)<=len h21 by A47,NAT_D:44;
then (ny-'len h11 +2-'1) in dom h21 by A128,FINSEQ_3:25;
then nx-'len h1+2-'1=ny-'len h1+2-'1 by A39,A32,A81,A118,A116,A129;
then nx-'len h1+2-1=ny-'len h1+2-'1 by A39,A115,Lm1,NAT_D:39,42;
then nx-'len h1+(2-1)=ny-'len h1+2-1 by A39,A128,NAT_D:39;
then len h1+nx-len h1=len h1+(ny-len h1) by A39,A111,A126,XCMPLX_1:29;
hence thesis;
end;
end;
end;
then
A130: h0/.len h0 <> W-min P by A16,A72,A65,A74,A75,A67;
A131: dom g2 = [.0,1.] by BORSUK_1:40,FUNCT_2:def 1;
thus 8<=len h0 by A38,A47,A36,A52,A55,A57,A58,FINSEQ_3:29;
rng (mid(h21,2,len h21 -'1)) c= rng h21 & rng (g2*h2) c= rng g2 by
FINSEQ_6:119,RELAT_1:26;
then rng (g1*h1) c= rng g1 & rng (mid(h21,2,len h21 -'1)) c= rng g2 by
RELAT_1:26;
then rng h11 \/ rng (mid(h21,2,len h21 -'1)) c= Upper_Arc(P) \/ Lower_Arc(P
) by A5,A23,XBOOLE_1:13;
then rng h0 c=Upper_Arc(P) \/ Lower_Arc(P) by FINSEQ_1:31;
hence rng h0 c= P by A1,JORDAN6:def 9;
A132: dom g1 =[.0,1.] by BORSUK_1:40,FUNCT_2:def 1;
thus for i being Nat st 1<=i & i=len h1;
per cases by A152,XXREAL_0:1;
suppose
A153: i>len h1;
then len h11+1<=i by A39,NAT_1:13;
then
A154: h0.i=(mid(h21,2,len h21 -'1)).(i -len h11) by A36,A134,FINSEQ_1:23;
A155: i+1-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36,A135
,XREAL_1:9;
i+1>len h11 by A39,A153,NAT_1:13;
then
A156: i+1-len h11=i+1-'len h11 by XREAL_1:233;
A157: len h1 +1<=i by A153,NAT_1:13;
then
A158: len h1 +1-len h1<=i-len h1 by XREAL_1:9;
A159: i-len h11=i-'len h11 by A39,A153,XREAL_1:233;
A160: len h1 +1<=i+1 by A157,NAT_1:13;
then
A161: len h1 +1-len h1<=i+1-len h1 by XREAL_1:9;
then
A162: 1 i+1-'len h11 +2-'1 by A28,A47,A196;
then h0/.(i+1) <> W-min P by A46,A47,A34,A35,A32,A197,A196,A190,A194;
hence thesis by A189,A190,A198,JORDAN6:def 10;
end;
end;
end;
A199: ilen h1;
i in dom h0 by A202,A199,FINSEQ_3:25;
then
A214: h0/.i=h0.i by PARTFUN1:def 6;
A215: i-len h11=i-'len h11 by A39,A213,XREAL_1:233;
i-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A199,
XREAL_1:9;
then i-'len h11+2<=len h2-2+2 by A39,A215,XREAL_1:6;
then
A216: (i-'len h11 +2-'1)<=len h21 by A47,NAT_D:44;
i-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A199,
XREAL_1:9;
then
A217: i-'len h11+2<=len h2-2+2 by A39,A215,XREAL_1:6;
set k=i-'len h11+2-'1;
A218: i-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36,A199,
XREAL_1:9;
A219: 0+2<=i-'len h11 +2 by XREAL_1:6;
then
A220: i-'len h11+2-'1=i-'len h11+2-1 by Lm1,NAT_D:39,42;
1<=(i-'len h11 +2-'1) by A219,Lm1,NAT_D:42;
then
A221: k in dom h2 by A46,A216,FINSEQ_3:25;
then h2.k in rng h2 by FUNCT_1:def 3;
then
A222: g2.(h2.k) in rng g2 by A131,A29,BORSUK_1:40,FUNCT_1:def 3;
A223: len h1 +1<=i by A213,NAT_1:13;
then h0.i=(mid(h21,2,len h21 -'1)).(i -len h11) & len h1 +1-len h1<=i-
len h1 by A39,A36,A199,FINSEQ_1:23,XREAL_1:9;
then
A224: h0.i=h21.(i-'len h11 +2-'1) by A39,A48,A56,A50,A54,A215,A218,FINSEQ_6:118
;
then h0.i=g2.(h2.k) by A221,FUNCT_1:13;
then h0.i in Upper_Arc(P) /\ Lower_Arc(P) by A23,A206,A212,A211,A214,A222
,XBOOLE_0:def 4;
then h0.i in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
then
A225: h0.i=W-min(P) or h0.i=E-max(P)by TARSKI:def 2;
len h11+1-len h11<=i-len h11 by A39,A223,XREAL_1:9;
then 1<=i-'len h11 by NAT_D:39;
then 1+2<=i-'len h11+2 by XREAL_1:6;
then 1+2-1<=i-'len h11+2-1 by XREAL_1:9;
then
A226: 1len h1;
1+1 in dom h1 by A14,FINSEQ_3:25;
then
A239: h11.(1+1)=g1.(h1.(1+1)) by FUNCT_1:13;
A240: i-len h11=i-'len h11 by A39,A238,XREAL_1:233;
i+1-1<=len h1+(len h2-2)-1 by A39,A47,A36,A52,A55,A57,A200,XREAL_1:9;
then i-len h11<=len h1+((len h2-2)-1)-len h11 by XREAL_1:9;
then i-'len h11+2<=len h2-2-1+2 by A39,A240,XREAL_1:6;
then
A241: i-'len h11+2-1<=len h2-1-1 by XREAL_1:9;
A242: len h1 +1<=i by A238,NAT_1:13;
then
A243: len h1 +1-len h1<=i-len h1 by XREAL_1:9;
h1.(1+1) in rng h1 by A15,FUNCT_1:def 3;
then
A244: g1.(h1.(1+1)) in rng g1 by A132,A11,BORSUK_1:40,FUNCT_1:def 3;
0+2<=i-'len h11 +2 by XREAL_1:6;
then
A245: 2-'1<=(i-'len h11 +2-'1) by NAT_D:42;
set k=i-'len h11+2-'1;
0+1<=i-'len h11+1+1-1 by XREAL_1:6;
then
A246: i-'len h11+2-'1=i-'len h11+2-1 by NAT_D:39;
A247: i-len h11 <=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36,A199,
XREAL_1:9;
i-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A199,
XREAL_1:9;
then i-'len h11+2<=len h2-2+2 by A39,A240,XREAL_1:6;
then i-'len h11 +2-'1<=len h21 by A47,NAT_D:44;
then
A248: (i-'len h11 +2-'1) in dom h21 by A245,Lm1,FINSEQ_3:25;
A249: h0.i=(mid(h21,2,len h21 -'1)).(i -len h11) by A39,A36,A199,A242,
FINSEQ_1:23;
then h0.(i)=h21.(i-'len h11 +2-'1) by A39,A48,A56,A50,A54,A240,A247,A243,
FINSEQ_6:118;
then
A250: h0.i=g2.(h2.k) by A46,A248,FUNCT_1:13;
h2.k in rng h2 by A46,A248,FUNCT_1:def 3;
then
A251: h0.i in Lower_Arc(P) by A23,A131,A29,A250,BORSUK_1:40,FUNCT_1:def 3;
1<=i-len h11 by A38,A243,FINSEQ_3:29;
then h0.i=h21.k by A48,A56,A50,A54,A240,A247,A249,FINSEQ_6:118;
then h0/.i <> W-min P by A228,A46,A34,A35,A32,A204,A246,A248,A241;
hence LE h0/.(1+1),h0/.i,P by A5,A204,A206,A41,A239,A244,A251,
JORDAN6:def 10;
end;
end;
A252: len h0-len h11=len h0-'len h11 by A39,A65,XREAL_1:233;
then (len h0-'len h11 +2-'1)<=len h21 by A36,A52,A55,A57,NAT_D:44;
then (len h0-'len h11 +2-'1) in dom h21 by A43,Lm1,FINSEQ_3:25;
then
A253: h21.k=g2.(h2.k) & h2.k in rng h2 by A46,FUNCT_1:13,def 3;
h1.len h1 in dom g1 by A9,A69,XXREAL_1:1;
then
A254: len h1 in dom (g1*h1) by A45,FUNCT_1:11;
then
A255: h11.len h1=E-max(P) by A7,A9,FUNCT_1:12;
A256: for i being Nat st 1<=i & i+1<=len h0 holds LE h0/.i,h0/.(i
+1),P & h0/.(i+1)<>W-min(P) & h0/.i<>h0/.(i+1)
proof
let i be Nat such that
A257: 1<=i and
A258: i+1<=len h0;
A259: i 1 & i+1 <> i by A257,NAT_1:13;
A270: i in dom h1 by A257,A264,FINSEQ_3:25;
then
A271: h1.i in rng h1 by FUNCT_1:def 3;
then
A272: 0 <= (h1.i) & (h1.i) <= 1 by A11,BORSUK_1:40,XXREAL_1:1;
A273: h0.(i+1)=h11.(i+1) by A39,A260,A265,FINSEQ_1:64;
then
A274: h0.(i+1)=g1.(h1.(i+1)) by A266,FUNCT_1:13;
then
A275: h0.(i+1) in Upper_Arc(P) by A5,A132,A11,A267,BORSUK_1:40,FUNCT_1:def 3;
A276: h0.i=h11.i by A39,A257,A264,FINSEQ_1:64;
then
A277: g1.(h1.i) = h0/.i by A263,A270,FUNCT_1:13;
g1.(h1.i) in rng g1 by A132,A11,A271,BORSUK_1:40,FUNCT_1:def 3;
then
A278: h0.i in Upper_Arc(P) by A5,A276,A270,FUNCT_1:13;
h1.i=len h1;
per cases by A279,XXREAL_0:1;
suppose
A280: i>len h1;
i-len h11len h11 by A39,A280,NAT_1:13;
then
A282: i+1-len h11=i+1-'len h11 by XREAL_1:233;
set j=i-'len h11+2-'1;
A283: i+1-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36,A258
,XREAL_1:9;
A284: 0+2<=i-'len h11 +2 by XREAL_1:6;
then
A285: j+1=i-'len h11+(1+1)-1+1 by Lm1,NAT_D:39,42
.=i-'len h11+(1+1);
A286: len h1 +1<=i by A280,NAT_1:13;
then
A287: len h1 +1-len h1<=i-len h1 by XREAL_1:9;
i+1 in dom h0 by A258,A260,FINSEQ_3:25;
then
A288: h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
A289: len h1 +1<=i+1 by A286,NAT_1:13;
then
A290: len h1 +1-len h1<=i+1-len h1 by XREAL_1:9;
then 1 W-min P by A46,A34,A35,A32,A295,A292,A281,A285,A297,A288;
A307: h0.(i+1)=g2.(h2.(j+1)) by A292,A305,A297,FUNCT_1:13;
then
A308: h0/.(i+1) in Lower_Arc(P) by A23,A131,A29,A298,A288,BORSUK_1:40
,FUNCT_1:def 3;
A309: h2.j in rng h2 by A300,FUNCT_1:def 3;
then
A310: j < j+1 & h0/.i in Lower_Arc(P) by A23,A131,A29,A304,A302,BORSUK_1:40
,FUNCT_1:def 3,NAT_1:13;
0 <= (h2.j) & (h2.j) <= 1 by A29,A309,BORSUK_1:40,XXREAL_1:1;
then LE h0/.i,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P) by A21,A22,A23
,A24,A25,A304,A307,A301,A302,A288,A299,Th18;
hence thesis by A46,A32,A303,A292,A305,A300,A297,A302,A288,A306,A310
,A308,JORDAN6:def 10;
end;
suppose
A311: i=len h1;
then
A312: i-len h11=i-'len h11 by A39,XREAL_1:233;
i-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A262,
XREAL_1:9;
then
A313: i-'len h11+2<=len h2-2+2 by A39,A312,XREAL_1:6;
then
A314: (i-'len h11 +2-'1)<=len h21 by A47,NAT_D:44;
set j=i-'len h11+2-'1;
A315: j+1 <> j;
A316: 0+2<=i-'len h11 +2 by XREAL_1:6;
then
A317: j+1=i-'len h11+(1+1)-1+1 by Lm1,NAT_D:39,42
.=i-'len h11+2;
2-'1<=(i-'len h11 +2-'1) by A316,NAT_D:42;
then 1 W-min P by A46,A34,A35,A32,A323,A331,A318,A330;
hence thesis by A46,A32,A323,A331,A327,A328,A326,A318,A329,A330,A332
,A325,A315,JORDAN6:def 10;
end;
end;
end;
then
A333: LE h0/.1,h0/.(1+1),P & h0/.1<>h0/.(1+1) by A205;
A334: E-max P in Upper_Arc P by A1,Th1;
thus for i being Nat,W being Subset of Euclid 2 st 1<=i & i W-min P by A38,A17,A71,A20,A340,A358,A353,A351;
assume x in Segment(h0/.i,h0/.(i+1),P);
then x in {p: LE h0/.i,p,P & LE p,h0/.(i+1),P} by A362,Def1;
then consider p being Point of TOP-REAL 2 such that
A363: p=x and
A364: LE h0/.i,p,P and
A365: LE p,h0/.(i+1),P;
A366: h0/.i in Upper_Arc(P) & p in Lower_Arc(P)& not p=W-min(P) or h0
/.i in Upper_Arc(P) & p in Upper_Arc(P) & LE h0/.i,p,Upper_Arc(P),W-min(P),
E-max(P) or h0/.i in Lower_Arc(P) & p in Lower_Arc(P)& not p=W-min(P) & LE h0/.
i,p,Lower_Arc(P),E-max(P),W-min(P) by A364,JORDAN6:def 10;
A367: p in Upper_Arc(P) & h0/.(i+1) in Lower_Arc(P) or p in Upper_Arc(
P) & h0/.(i+1) in Upper_Arc(P) & LE p,h0/.(i+1),Upper_Arc(P),W-min(P),E-max(P)
or p in Lower_Arc(P) & h0/.(i+1) in Lower_Arc(P)& LE p,h0/.(i+1),Lower_Arc(P),
E-max(P),W-min(P) by A365,JORDAN6:def 10;
now
per cases by A352,XXREAL_0:1;
suppose
i+1 E-max P by A38,A45,A255,A20,A358,A353,A351;
A369: now
assume h0/.(i+1) in Lower_Arc(P);
then
h0/.(i+1) in Upper_Arc(P)/\ Lower_Arc(P) by A351,A360,XBOOLE_0:def 4;
then h0/.(i+1) in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
hence contradiction by A362,A368,TARSKI:def 2;
end;
then
A370: LE p,h0/.(i+1),Upper_Arc(P),W-min(P),E-max(P) by A365,
JORDAN6:def 10;
then
A371: p<>E-max(P) by A3,A368,JORDAN6:55;
A372: p in Upper_Arc(P) by A365,A369,JORDAN6:def 10;
per cases by A335,XXREAL_0:1;
suppose
i>1;
then
A373: h0/.i <> W-min P by A38,A17,A71,A20,A342,A347,A348,A350;
A374: h11.i <> E-max(P) by A38,A45,A255,A20,A341,A342;
now
assume h0/.i in Lower_Arc(P);
then h0/.i in Upper_Arc(P)/\ Lower_Arc(P) by A350,A349,
XBOOLE_0:def 4;
then h0/.i in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
hence contradiction by A357,A350,A373,A374,TARSKI:def 2;
end;
then
A375: h0/.i in Upper_Arc(P) & p in Lower_Arc(P) & not p=W-min(P)
or h0/.i in Upper_Arc(P) & p in Upper_Arc(P) & LE h0/.i,p,Upper_Arc(P),W-min(P)
,E-max(P) by A364,JORDAN6:def 10;
then
A376: p <> W-min P by A3,A373,JORDAN6:54;
A377: now
assume p in Lower_Arc(P);
then p in Upper_Arc(P)/\ Lower_Arc(P) by A372,XBOOLE_0:def 4;
then p in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
hence contradiction by A371,A376,TARSKI:def 2;
end;
then consider z being object such that
A378: z in dom g1 and
A379: p=g1.z by A5,A375,FUNCT_1:def 3;
reconsider rz=z as Real by A132,A378;
A380: rz<=1 by A378,BORSUK_1:40,XXREAL_1:1;
h1.(i+1) in rng h1 by A353,FUNCT_1:def 3;
then
A381: 0<=h1/.(i+1) & h1/.(i+1)<=1 by A11,A355,BORSUK_1:40,XXREAL_1:1;
reconsider z as set by TARSKI:1;
take z;
thus z in dom g1 by A378;
A382: g1.(h1/.i)=h0/.i & h1/.i<=1 by A335,A341,A357,A347,A344,A350,
FINSEQ_4:15;
g1.(h1/.(i+1))=h0/.(i+1) by A340,A352,A359,A351,FINSEQ_4:15;
then
A383: rz<=h1/.(i+1) by A4,A5,A6,A7,A370,A379,A381,A380,Th19;
0<=rz by A378,BORSUK_1:40,XXREAL_1:1;
then h1/.i<=rz by A4,A5,A6,A7,A375,A377,A379,A382,A380,Th19;
hence z in [.h1/.i,h1/.(i+1).] by A383,XXREAL_1:1;
thus x = g1.z by A363,A379;
end;
suppose
A384: i=1;
now
per cases;
case
A385: p<>W-min(P);
now
assume p in Lower_Arc(P);
then p in Upper_Arc(P)/\ Lower_Arc(P) by A372,
XBOOLE_0:def 4;
then p in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
hence contradiction by A371,A385,TARSKI:def 2;
end;
then consider z being object such that
A386: z in dom g1 and
A387: p=g1.z by A5,A366,FUNCT_1:def 3;
reconsider rz=z as Real by A132,A386;
A388: h1/.1<=rz by A8,A346,A384,A386,BORSUK_1:40,XXREAL_1:1;
h1.(1+1) in rng h1 by A353,A384,FUNCT_1:def 3;
then
A389: 0<=h1/.(1+1) & h1/.(1+1)<=1 by A11,A355,A384,BORSUK_1:40
,XXREAL_1:1;
A390: g1.(h1/.(1+1))=h0/.(1+1) by A352,A359,A351,A384,FINSEQ_4:15;
take rz;
rz<=1 by A386,BORSUK_1:40,XXREAL_1:1;
then rz<=h1/.(1+1) by A4,A5,A6,A7,A370,A384,A387,A390,A389
,Th19;
hence
rz in dom g1 & rz in [.h1/.1,h1/.(1+1).] & x = g1.rz by A363
,A386,A387,A388,XXREAL_1:1;
end;
case
A391: p=W-min(P);
thus 0 in [.h1/.1,h1/.(1+1).] by A8,A354,A346,A355,A384,
XXREAL_1:1;
thus x = g1.0 by A6,A363,A391;
end;
end;
hence ex y being set
st y in dom g1 & y in [.h1/.i,h1/.(i+1).] &
x = g1.y by A44,A384;
end;
end;
suppose
A392: i+1=len h1;
then
A393: h0/.(i+1)=E-max(P) by A7,A9,A45,A358,A351,FUNCT_1:13;
A394: now
assume that
A395: p in Lower_Arc(P) and
A396: not p in Upper_Arc(P);
LE h0/.(i+1),p,Lower_Arc(P),E-max(P),W-min(P) by A21,A393,A395,
JORDAN5C:10;
hence contradiction by A334,A21,A367,A393,A396,JORDAN5C:12;
end;
p in Upper_Arc(P) or p in Lower_Arc(P) by A364,JORDAN6:def 10;
then
A397: LE p,h0/.(i+1),Upper_Arc(P),W-min(P),E-max(P) by A3,A393,A394,
JORDAN5C:10;
per cases;
suppose
A398: p<>E-max(P);
now
per cases;
case
A399: p<>W-min(P);
A400: now
assume p in Lower_Arc(P);
then p in Upper_Arc(P)/\ Lower_Arc(P) by A394,
XBOOLE_0:def 4;
then p in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
hence contradiction by A398,A399,TARSKI:def 2;
end;
then consider z being object such that
A401: z in dom g1 and
A402: p=g1.z by A5,A366,FUNCT_1:def 3;
reconsider rz=z as Real by A132,A401;
A403: rz<=1 by A401,BORSUK_1:40,XXREAL_1:1;
h1.(i+1) in rng h1 by A353,FUNCT_1:def 3;
then
A404: 0<=h1/.(i+1) & h1/.(i+1)<=1 by A11,A355,BORSUK_1:40
,XXREAL_1:1;
g1.(h1/.(i+1))=h0/.(i+1) by A340,A352,A359,A351,FINSEQ_4:15;
then
A405: rz<=h1/.(i+1) by A4,A5,A6,A7,A397,A402,A404,A403,Th19;
take rz;
0<=rz by A401,BORSUK_1:40,XXREAL_1:1;
then h1/.i<=rz by A4,A5,A6,A7,A357,A347,A344,A350,A346,A366
,A400,A402,A403,Th19;
hence
rz in dom g1 & rz in [.h1/.i,h1/.(i+1).] & x = g1.rz by A363
,A401,A402,A405,XXREAL_1:1;
end;
case
A406: p=W-min(P);
then h11.i=W-min(P) by A3,A357,A350,A366,JORDAN6:54;
then i=1 by A38,A17,A71,A20,A342;
then 0 in [.h1/.i,h1/.(i+1).] by A8,A354,A346,A355,XXREAL_1:1
;
hence ex y being set st y in dom g1 & y in [.h1/.i,h1/.(i+1)
.] & x = g1.y by A6,A44,A363,A406;
end;
end;
hence ex y being set st y in dom g1 & y in [.h1/.i,h1/.(i+1).] &
x = g1.y;
end;
suppose
A407: p=E-max(P);
1 in [.h1/.i,h1/.(i+1).] by A9,A354,A346,A355,A392,XXREAL_1:1;
hence ex y being set
st y in dom g1 & y in [.h1/.i,h1/.(i+1).] &
x = g1.y by A7,A69,A363,A407,Lm6;
end;
end;
end;
hence thesis by FUNCT_1:def 6;
end;
A408: h1.(i+1)<=1 by A11,A356,BORSUK_1:40,XXREAL_1:1;
g1.:([.h1/.i,h1/.(i+1).]) c= Segment(h0/.i,h0/.(i+1),P)
proof
A409: g1.(h1/.i)=h0/.i & 0<=h1/.i by A335,A341,A348,A345,A350,FINSEQ_4:15;
let x be object;
assume x in g1.:([.h1/.i,h1/.(i+1).]);
then consider y being object such that
A410: y in dom g1 and
A411: y in [.h1/.i,h1/.(i+1).] and
A412: x=g1.y by FUNCT_1:def 6;
reconsider sy=y as Real by A411;
A413: sy<=1 by A410,BORSUK_1:40,XXREAL_1:1;
A414: x in Upper_Arc(P) by A5,A410,A412,FUNCT_1:def 3;
then reconsider p1=x as Point of TOP-REAL 2;
A415: h1/.i<=1 by A335,A341,A344,FINSEQ_4:15;
h1/.i<=sy by A411,XXREAL_1:1;
then LE h0/.i,p1,Upper_Arc(P),W-min(P),E-max(P) by A3,A4,A5,A6,A7,A412
,A409,A415,A413,Th18;
then
A416: LE h0/.i,p1,P by A350,A349,A414,JORDAN6:def 10;
sy<=h1/.(i+1) & 0<=sy by A410,A411,BORSUK_1:40,XXREAL_1:1;
then LE p1,h0/.(i+1),Upper_Arc(P),W-min(P),E-max(P) by A3,A4,A5,A6,A7
,A359,A408,A351,A355,A412,A413,Th18;
then LE p1,h0/.(i+1),P by A351,A360,A414,JORDAN6:def 10;
then
A417: x in {p: LE h0/.i,p,P & LE p,h0/.(i+1),P} by A416;
not h0/.(i+1)=W-min P by A38,A17,A71,A20,A340,A358,A353,A351;
hence thesis by A417,Def1;
end;
then W=g1.:Q1 by A337,A361;
hence thesis by A13,A335,A341;
end;
suppose
A418: i>len h1;
i-len h11len h11 by A39,A418,NAT_1:13;
then
A424: i+1-len h11=i+1-'len h11 by XREAL_1:233;
i+1 in dom h0 by A338,A340,FINSEQ_3:25;
then
A425: h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
A426: i<=len h11 + len (mid(h21,2,len h21 -'1)) by A336,FINSEQ_1:22;
len h11+1<=i by A39,A418,NAT_1:13;
then
A427: h0.i=(mid(h21,2,len h21 -'1)).(i -len h11) by A426,FINSEQ_1:23;
A428: i+1-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36,A338,
XREAL_1:9;
i in dom h0 by A335,A336,FINSEQ_3:25;
then
A429: h0/.i=h0.i by PARTFUN1:def 6;
set j=i-'len h11+2-'1;
len h2 W-min(P) by A46,A34,A35,A32,A440,A439,A429;
A458: h2/.j<=1 by A29,A442,A445,BORSUK_1:40,XXREAL_1:1;
let x be object;
assume
A459: x in Segment(h0/.i,h0/.(i+1),P);
h0/.(i+1) <> W-min P by A46,A34,A35,A32,A422,A451,A419,A432,A450,A435
,A425;
then x in {p: LE h0/.i,p,P & LE p,h0/.(i+1),P} by A459,Def1;
then consider p being Point of TOP-REAL 2 such that
A460: p=x and
A461: LE h0/.i,p,P and
A462: LE p,h0/.(i+1),P;
A463: h0/.i in Upper_Arc(P) & p in Lower_Arc(P)& not p=W-min(P) or h0
/.i in Upper_Arc(P) & p in Upper_Arc(P) & LE h0/.i,p,Upper_Arc(P),W-min(P),
E-max(P) or h0/.i in Lower_Arc(P) & p in Lower_Arc(P)& not p=W-min(P) & LE h0/.
i,p,Lower_Arc(P),E-max(P),W-min(P) by A461,JORDAN6:def 10;
A464: h21.j <> E-max P by A46,A76,A77,A32,A453,A439;
A465: now
assume h0/.i in Upper_Arc(P);
then h0/.i in Upper_Arc(P)/\ Lower_Arc(P) by A429,A443,XBOOLE_0:def 4
;
then h0/.i in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
hence contradiction by A440,A429,A457,A464,TARSKI:def 2;
end;
then
A466: LE h0/.i,p,Lower_Arc P, E-max P, W-min P by A461,JORDAN6:def 10;
A467: h0/.i <> E-max(P) by A46,A76,A77,A32,A440,A453,A439,A429;
A468: now
assume p in Upper_Arc(P);
then p in Upper_Arc P /\ Lower_Arc P by A463,A465,XBOOLE_0:def 4;
then p in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
then p=W-min(P) or p=E-max(P) by TARSKI:def 2;
hence contradiction by A21,A463,A465,A467,JORDAN6:54;
end;
A469: h0/.(i+1) <> E-max P & h21.(j+1) <> W-min P by A46,A76,A34,A77,A35,A32
,A422,A451,A419,A432,A450,A434,A435,A425;
now
assume h0/.(i+1) in Upper_Arc(P);
then h0/.(i+1) in Upper_Arc(P)/\ Lower_Arc(P) by A425,A452,
XBOOLE_0:def 4;
then h0/.(i+1) in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
hence contradiction by A451,A450,A425,A469,TARSKI:def 2;
end;
then p in Lower_Arc(P) & h0/.(i+1) in Lower_Arc(P)& not h0/.(i+ 1)=
W-min(P) & LE p,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P) or p in Upper_Arc(P) &
h0/.(i+1) in Lower_Arc(P) & not h0/.(i+1)=W-min(P) by A462,JORDAN6:def 10;
then consider z being object such that
A470: z in dom g2 and
A471: p=g2.z by A23,A468,FUNCT_1:def 3;
reconsider rz=z as Real by A131,A470;
A472: rz<=1 by A470,BORSUK_1:40,XXREAL_1:1;
LE p,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P) by A462,A468,
JORDAN6:def 10;
then
A473: rz<=h2/.(j+1) by A22,A23,A24,A25,A471,A456,A472,A455,Th19;
0<=rz by A470,BORSUK_1:40,XXREAL_1:1;
then h2/.j<=rz by A22,A23,A24,A25,A441,A429,A445,A466,A471,A458,A472
,Th19;
then rz in [.h2/.j,h2/.(j+1).] by A473,XXREAL_1:1;
hence thesis by A460,A470,A471,FUNCT_1:def 6;
end;
A474: g2.(h2.(j+1)) = h0/.(i+1) by A451,A450,A435,A425,FUNCT_1:13;
g2.:([.h2/.j,h2/.(j+1).]) c= Segment(h0/.i,h0/.(i+1),P)
proof
let x be object;
assume x in g2.:([.h2/.j,h2/.(j+1).]);
then consider y being object such that
A475: y in dom g2 and
A476: y in [.h2/.j,h2/.(j+1).] and
A477: x=g2.y by FUNCT_1:def 6;
reconsider sy=y as Real by A476;
A478: sy<=h2/.(j+1) by A476,XXREAL_1:1;
A479: x in Lower_Arc(P) by A23,A475,A477,FUNCT_1:def 3;
then reconsider p1=x as Point of TOP-REAL 2;
A480: h2.(j+1) <> 1 by A27,A30,A34,A422,A419,A432,A435,FUNCT_1:def 4;
A481: now
assume p1=W-min(P);
then 1=sy by A22,A25,A227,A475,A477;
hence contradiction by A437,A438,A478,A480,XXREAL_0:1;
end;
A482: sy<=1 by A475,BORSUK_1:40,XXREAL_1:1;
h2/.j<=sy by A476,XXREAL_1:1;
then LE h0/.i,p1,Lower_Arc(P),E-max(P),W-min(P) by A21,A22,A23,A24,A25
,A441,A429,A446,A445,A477,A482,Th18;
then
A483: LE h0/.i,p1,P by A429,A443,A479,A481,JORDAN6:def 10;
A484: h0/.(i+1) <> W-min P by A46,A34,A35,A32,A422,A451,A419,A432,A450,A435
,A425;
0<=sy by A475,BORSUK_1:40,XXREAL_1:1;
then LE p1,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P) by A21,A22,A23,A24
,A25,A474,A437,A438,A477,A478,A482,Th18;
then LE p1,h0/.(i+1),P by A425,A452,A479,A484,JORDAN6:def 10;
then x in {p: LE h0/.i,p,P & LE p,h0/.(i+1),P} by A483;
hence thesis by A484,Def1;
end;
then W=g2.:(Q1) by A337,A454;
hence thesis by A31,A433,A444;
end;
suppose
A485: i=len h1;
A486: i+1-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36,A338,
XREAL_1:9;
then 1<=i+1-'len h11 by A39,A339,A485,XREAL_1:233;
then 1W-min(P) by A46,A34,A35,A32,A507,A517,A494,A488;
A520: g2.(h2/.(j+1))=h0/.(i+1) by A496,A491,A503,A515,A501,FINSEQ_4:15;
h2.(j+1) in rng h2 by A504,FUNCT_1:def 3;
then
A521: 0<=h2/.(j+1) & h2/.(j+1)<=1 by A29,A510,BORSUK_1:40,XXREAL_1:1;
A522: h0/.(i+1) in Lower_Arc(P) by A23,A131,A29,A515,A505,A501,BORSUK_1:40
,FUNCT_1:def 3;
let x be object;
assume
A523: x in Segment(h0/.i,h0/.(i+1),P);
h0/.(i+1) <> W-min P by A46,A34,A35,A32,A498,A514,A504,A501;
then x in {p: LE h0/.i,p,P & LE p,h0/.(i+1),P} by A523,Def1;
then consider p being Point of TOP-REAL 2 such that
A524: p=x and
A525: LE h0/.i,p,P and
A526: LE p,h0/.(i+1),P;
A527: h0/.i in Upper_Arc(P) & p in Lower_Arc(P)& not p=W-min(P) or h0
/.i in Upper_Arc(P) & p in Upper_Arc(P) & LE h0/.i,p,Upper_Arc(P),W-min(P),
E-max(P) or h0/.i in Lower_Arc(P) & p in Lower_Arc(P)& not p=W-min(P) & LE h0/.
i,p,Lower_Arc(P),E-max(P),W-min(P) by A525,JORDAN6:def 10;
dom (g1*h1) c= dom h0 by FINSEQ_1:26;
then
A528: h0/.i=E-max(P) by A254,A485,A489,PARTFUN1:def 6;
A529: now
assume
A530: not p in Lower_Arc(P);
then p=E-max(P) by A3,A527,A528,JORDAN6:55;
hence contradiction by A1,A530,Th1;
end;
A531: now
assume p in Upper_Arc(P);
then p in Upper_Arc(P)/\ Lower_Arc(P) by A529,XBOOLE_0:def 4;
then
A532: p in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
p <> W-min P by A3,A527,A519,JORDAN6:54;
hence p = E-max P by A532,TARSKI:def 2;
end;
then p in rng g2 by A1,A23,A525,Th1,JORDAN6:def 10;
then consider z being object such that
A533: z in dom g2 and
A534: p=g2.z by FUNCT_1:def 3;
reconsider rz=z as Real by A131,A533;
0<=rz by A533,BORSUK_1:40,XXREAL_1:1;
then
A535: h2/.j<=rz by A26,A485,A511,A492,Lm1,FINSEQ_4:15;
A536: not h0/.(i+1)=E-max(P) by A46,A76,A77,A32,A503,A514,A504,A501;
now
assume h0/.(i+1) in Upper_Arc(P);
then h0/.(i+1) in Upper_Arc(P)/\ Lower_Arc(P) by A522,XBOOLE_0:def 4;
then h0/.(i+1) in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
then h21.(j+1)=W-min(P) by A514,A501,A536,TARSKI:def 2;
hence contradiction by A46,A34,A35,A32,A498,A504;
end;
then p in Lower_Arc(P) & h0/.(i+1) in Lower_Arc(P) & not h0/.(i +1)=
W-min(P) & LE p,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P) or p in Upper_Arc(P) &
h0/.(i+1) in Lower_Arc(P) & not h0/.(i+1)=W-min(P) by A526,JORDAN6:def 10;
then
A537: LE p,h0/.(i+1),Lower_Arc P, E-max P, W-min P by A21,A531,JORDAN5C:10;
rz<=1 by A533,BORSUK_1:40,XXREAL_1:1;
then rz<=h2/.(j+1) by A22,A23,A24,A25,A537,A534,A520,A521,Th19;
then rz in [.h2/.j,h2/.(j+1).] by A535,XXREAL_1:1;
hence thesis by A524,A533,A534,FUNCT_1:def 6;
end;
A538: g2.(h2.(j+1)) = h0/.(i+1) by A514,A504,A501,FUNCT_1:13;
g2.:([.h2/.j,h2/.(j+1).]) c= Segment(h0/.i,h0/.(i+1),P)
proof
let x be object;
assume x in g2.:([.h2/.j,h2/.(j+1).]);
then consider y being object such that
A539: y in dom g2 and
A540: y in [.h2/.j,h2/.(j+1).] and
A541: x=g2.y by FUNCT_1:def 6;
reconsider sy=y as Real by A540;
A542: sy<=h2/.(j+1) by A540,XXREAL_1:1;
A543: x in Lower_Arc(P) by A23,A539,A541,FUNCT_1:def 3;
then reconsider p1=x as Point of TOP-REAL 2;
A544: h2.(j+1) <> 1 by A27,A30,A34,A498,A504,FUNCT_1:def 4;
A545: now
assume p1=W-min(P);
then 1=sy by A22,A25,A227,A539,A541;
hence contradiction by A506,A510,A542,A544,XXREAL_0:1;
end;
A546: 0<=sy & sy<=1 by A539,BORSUK_1:40,XXREAL_1:1;
then LE h0/.i,p1,Lower_Arc(P),E-max(P),W-min(P) by A21,A22,A23,A24,A25
,A489,A488,A541,Th18;
then
A547: LE h0/.i,p1,P by A488,A509,A543,A545,JORDAN6:def 10;
A548: h0/.(i+1) <> W-min(P) by A46,A34,A35,A32,A498,A514,A504,A501;
LE p1,h0/.(i+1),Lower_Arc(P),E-max(P),W-min(P) by A21,A22,A23,A24,A25
,A538,A506,A510,A541,A542,A546,Th18;
then LE p1,h0/.(i+1),P by A501,A516,A543,A548,JORDAN6:def 10;
then x in {p: LE h0/.i,p,P & LE p,h0/.(i+1),P} by A547;
hence thesis by A548,Def1;
end;
then W=g2.:(Q1) by A337,A518;
hence thesis by A31,A502,A512;
end;
end;
A549: len h0=len h1+(len h2-2) by A38,A47,A36,A52,A55,A57,FINSEQ_3:29;
thus for W being Subset of Euclid 2 st W=Segment(h0/.len h0,h0/.1,P) holds
diameter W < e
proof
set i=len h0;
let W be Subset of Euclid 2;
set j=i-'len h11+2-'1;
A550: 0+2<=i-'len h11 +2 by XREAL_1:6;
then
A551: 1<=(i-'len h11 +2-'1) by Lm1,NAT_D:42;
len h11+1-len h11<=i-len h11 by A47,A36,A52,A55,A57,A62,XXREAL_0:2;
then 1<=i-'len h11 by NAT_D:39;
then 1+2<=i-'len h11+2 by XREAL_1:6;
then
A552: 1+2-1<=i-'len h11+2-1 by XREAL_1:9;
len h0<=len h11 + len mid(h21,2,len h21 -'1) by FINSEQ_1:22;
then
A553: h0.i=(mid(h21,2,len h21 -'1)).(i -len h11) by A39,A64,FINSEQ_1:23;
A554: i-len h11=i-'len h11 by A39,A65,XREAL_1:233;
then (i-'len h11 +2-'1)<=len h21 by A36,A52,A55,A57,NAT_D:44;
then
A555: j in dom h2 by A46,A551,FINSEQ_3:25;
then
A556: h2.j in rng h2 by FUNCT_1:def 3;
i-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 & len h1 +
1-len h1 <=i-len h1 by A549,A62,FINSEQ_1:22,XXREAL_0:2;
then
A557: h0.i=h21.(i-'len h11 +2-'1) by A39,A48,A56,A50,A54,A553,A554,FINSEQ_6:118
;
then
A558: h0.i=g2.(h2.j) by A555,FUNCT_1:13;
then
A559: h0.i in Lower_Arc P by A23,A131,A29,A556,BORSUK_1:40,FUNCT_1:def 3;
A560: 2-'1<=(i-'len h11 +2-'1) by A550,NAT_D:42;
then
A561: 1W-min(P) or not h0/.i in P);
then p in Lower_Arc(P) by A567,A565,JORDAN6:def 10;
then consider z being object such that
A578: z in dom g2 and
A579: p=g2.z by A23,FUNCT_1:def 3;
take z;
thus z in dom g2 by A578;
reconsider rz=z as Real by A131,A578;
A580: rz<=1 by A578,BORSUK_1:40,XXREAL_1:1;
then
A581: rz<=h2/.(j+1) by A27,A47,A36,A52,A55,A57,A554,A561,FINSEQ_4:15;
A582: LE h0/.i,p,Lower_Arc(P),E-max(P),W-min(P) by A567,A565,A577,
JORDAN6:def 10;
0<=rz by A578,BORSUK_1:40,XXREAL_1:1;
then h2/.j<=rz by A22,A23,A24,A25,A558,A568,A565,A564,A582,A579,A580
,Th19;
hence z in [.h2/.j,h2/.(j+1).] & x = g2.z by A574,A579,A581,
XXREAL_1:1;
end;
suppose
h0/.i in P & p=W-min(P);
hence ex y being object
st y in dom g2 & y in [.h2/.j,h2/.(j+1).] & x =
g2.y by A25,A227,A574,A573,A576;
end;
end;
hence thesis by FUNCT_1:def 6;
end;
A583: 0 <= h2.j & h2.j <= 1 by A29,A556,BORSUK_1:40,XXREAL_1:1;
A584: g2.:([.h2/.j,h2/.(j+1).]) c= Segment(h0/.i,h0/.1,P)
proof
A585: Upper_Arc(P) \/ Lower_Arc(P)=P by A1,JORDAN6:def 9;
let x be object;
assume x in g2.:([.h2/.j,h2/.(j+1).]);
then consider y being object such that
A586: y in dom g2 and
A587: y in [.h2/.j,h2/.(j+1).] and
A588: x=g2.y by FUNCT_1:def 6;
reconsider sy=y as Real by A587;
A589: x in Lower_Arc(P) by A23,A586,A588,FUNCT_1:def 3;
then reconsider p1=x as Point of TOP-REAL 2;
h2/.j<=sy & sy<=1 by A586,A587,BORSUK_1:40,XXREAL_1:1;
then
A590: LE h0/.i,p1,Lower_Arc(P),E-max(P),W-min(P) by A21,A22,A23,A24,A25,A558
,A565,A583,A564,A588,Th18;
now
per cases;
case
p1=W-min(P);
hence LE h0/.i,p1,P or h0/.i in P & p1=W-min(P) by A559,A565,A585,
XBOOLE_0:def 3;
end;
case
p1<>W-min(P);
hence LE h0/.i,p1,P or h0/.i in P & p1=W-min(P) by A559,A565,A589
,A590,JORDAN6:def 10;
end;
end;
then
A591: x in {p: LE h0/.i,p,P or h0/.i in P & p=W-min(P)};
h0/.1=W-min(P) by A72,A67,PARTFUN1:def 6;
hence thesis by A591,Def1;
end;
assume W=Segment(h0/.len h0,h0/.1,P);
then W=g2.:Q1 by A569,A584;
hence thesis by A31,A47,A36,A52,A55,A57,A554,A560,A563,Lm1;
end;
A592: for i being Nat st 1<=i & i+1=len h1;
per cases by A615,XXREAL_0:1;
suppose
A616: i+1>len h1;
set j=(i+1)-'len h11+2-'1;
A617: (i+1)+1-len h11 <=len h11 + len (mid(h21,2,len h21 -'1))-len h11
by A36,A595,XREAL_1:9;
A618: 0+2<=(i+1)-'len h11 +2 by XREAL_1:6;
then
A619: 1<=((i+1)-'len h11 +2-'1) by Lm1,NAT_D:42;
A620: j+1=(i+1)-'len h11+(1+1)-1+1 by A618,Lm1,NAT_D:39,42
.=(i+1)-'len h11+2;
A621: len h1 +1<=i+1 by A616,NAT_1:13;
then
A622: len h1 +1-len h1<=(i+1)-len h1 by XREAL_1:9;
A623: (i+1)-len h11=(i+1)-'len h11 by A39,A616,XREAL_1:233;
(i+1)+1>len h11 by A39,A616,NAT_1:13;
then
A624: (i+1)+1-len h11=(i+1)+1-'len h11 by XREAL_1:233;
A625: len h1 +1<=(i+1)+1 by A621,NAT_1:13;
then
A626: len h1 +1-len h1<=(i+1)+1-len h1 by XREAL_1:9;
then 1<(i+1)+1-'len h11+(2-1) by A39,A624,NAT_1:13;
then
A627: 0<(i+1)+1-'len h11+2-1;
(i+1)-'len h11+2-'1=(i+1)-'len h11+2-1 by A618,Lm1,NAT_D:39,42;
then
A628: j+1=(i+1)+1-'len h11+2-'1 by A623,A624,A627,XREAL_0:def 2;
(i+1)-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57
,A594,XREAL_1:9;
then
A629: (i+1)-'len h11+2<=len h2-2+2 by A39,A623,XREAL_1:6;
then ((i+1)-'len h11 +2-'1)<=len h21 by A47,NAT_D:44;
then
A630: j in dom h2 by A46,A619,FINSEQ_3:25;
2-'1<=((i+1)-'len h11 +2-'1) by A618,NAT_D:42;
then 1 W-min P by A46,A34,A35,A32,A623,A641,A620,A628,A631,A640
;
i+1 in dom h0 by A594,A597,FINSEQ_3:25;
then
A645: h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
0<=h2.j & h2.j<=1 by A29,A638,BORSUK_1:40,XXREAL_1:1;
then LE h0/.(i+1),h0/.((i+1)+1),Lower_Arc(P),E-max(P),W-min(P) by A21
,A22,A23,A24,A25,A637,A642,A634,A645,A640,A633,Th18;
hence thesis by A645,A640,A639,A643,A644,JORDAN6:def 10;
end;
suppose
A646: i+1=len h1;
then len h1+1 <=len h11 + len (mid(h21,2,len h21 -'1)) by A595,
FINSEQ_1:22;
then
A647: (i+1)+1-len h11 <=len h11 + len (mid(h21,2,len h21 -'1))-len h11
by A646,XREAL_1:9;
then 1<=(i+1)+1-'len h11 by A39,A596,A646,XREAL_1:233;
then 1<(i+1)+1-'len h11+(2-1) by NAT_1:13;
then
A648: 0<(i+1)+1-'len h11+2-1;
A649: (i+1)+1-len h11=(i+1)+1-'len h11 by A39,A596,A646,XREAL_1:233;
len h1 in dom h0 by A594,A597,A646,FINSEQ_3:25;
then
A650: h0/.len h1=h0.len h1 by PARTFUN1:def 6;
set j=(i+1)-'len h11+2-'1;
A651: 0+2<=(i+1)-'len h11 +2 by XREAL_1:6;
then
A652: j+1=(i+1)-'len h11+(1+1)-1+1 by Lm1,NAT_D:39,42
.=(i+1)-'len h11+(1+1);
2-'1<=((i+1)-'len h11 +2-'1) by A651,NAT_D:42;
then
A653: 1 W-min P by A46,A34,A35,A32,A658,A659,A654,A657;
hence thesis by A646,A650,A657,A660,A656,JORDAN6:def 10;
end;
end;
end;
thus for i being Nat st 1<=i & i+1W-min(P) by A256;
h0/.i<>h0/.(i+1) & LE h0/.(i+1),h0/.(i+2),P by A592,A256,A661;
hence thesis by A1,A662,Th10;
end;
A663: 2 in dom h0 by A201,FINSEQ_3:25;
i <> 1 by A59,Lm2;
then
A664: h0/.i <> h0/.1 by A67,A78,A203,PARTFUN2:10;
A665: len h1 in dom h1 by A16,FINSEQ_3:25;
thus Segment(h0/.len h0,h0/.1,P)/\ Segment(h0/.1,h0/.2,P)={h0/.1}
proof
defpred P[Nat] means $1+2<=len h0 implies LE h0/.2,h0/.($1+2),P;
set j=len h0-'len h11+2-'1;
A666: len h0 -len h11 <=len h11 + len mid(h21,2,len h21 -'1) -len h11 by
FINSEQ_1:22;
A667: h0/.2=h0.2 by A663,PARTFUN1:def 6;
A668: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A669: k+2<=len h0 implies LE h0/.2,h0/.(k+2),P;
now
A670: k+1+1=k+2;
A671: k+1+2=k+2+1;
assume
A672: k+1+2<=len h0;
then k+2 W-min(P) by A38,A17,A71,A15,A20;
len h1 +1-len h1<=len h0 -len h1 & h0.len h0=(mid(h21,2,len h21 -'1)
).(len h0 -len h11) by A39,A36,A549,A62,A64,FINSEQ_1:23,XXREAL_0:2;
then h0.len h0=h21.(len h0-'len h11 +2-'1) by A39,A48,A56,A50,A54,A252,A666
,FINSEQ_6:118;
then
A680: h0.len h0=g2.(h2.j) by A675,FUNCT_1:13;
A681: now
h2.j in rng h2 by A675,FUNCT_1:def 3;
then
A682: g2.(h2.j) in rng g2 by A131,A29,BORSUK_1:40,FUNCT_1:def 3;
assume h0/.2=h0/.len h0;
then h0/.2 in Upper_Arc(P)/\ Lower_Arc(P) by A23,A75,A676,A680,A682,
XBOOLE_0:def 4;
then h0/.2 in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
then h11.2=E-max(P) by A40,A679,A667,TARSKI:def 2;
hence contradiction by A38,A665,A255,A14,A15,A20;
end;
h0/.2<>W-min(P) by A663,A40,A679,PARTFUN1:def 6;
hence thesis by A1,A73,A681,A678,A673,Th12;
end;
A683: i+1 = len h0 by A16,A65,XREAL_1:235,XXREAL_0:2;
then LE h0/.i,h0/.(i+1),P & h0/.(i+1)<>W-min(P) by A256,A202;
hence Segment(h0/.i,h0/.len h0,P)/\ Segment(h0/.len h0,h0/.1,P)={h0/.len h0}
by A1,A73,A683,A664,Th11;
LE h0/.i,h0/.(i+1),P by A256,A202,A200;
hence Segment(h0/.i,h0/.len h0,P) misses Segment(h0/.1,h0/.2,P) by A1,A683
,A333,A229,A207,Th13;
thus for i,j being Nat st 1<=i & i < j & j < len h0 &
i,j aren't_adjacent
holds Segment(h0/.i,h0/.(i+1),P) misses Segment(h0/.j,h0/.(j+1),P)
proof
let i,j be Nat;
assume that
A684: 1<=i and
A685: i < j and
A686: j < len h0 and
A687: i,j aren't_adjacent;
A688: 1h0/.(i+1) by A256,A684;
A691: i+1<=j by A685,NAT_1:13;
then
A692: (i+1)len h1;
j in dom h0 by A686,A688,FINSEQ_3:25;
then
A707: h0/.j=h0.j by PARTFUN1:def 6;
A708: j-len h11=j-'len h11 by A39,A706,XREAL_1:233;
j-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A686,
XREAL_1:9;
then j-'len h11+2<=len h2-2+2 by A39,A708,XREAL_1:6;
then
A709: (j-'len h11 +2-'1)<= len h21 by A47,NAT_D:44;
j-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A686,
XREAL_1:9;
then
A710: j-'len h11+2<=len h2-2+2 by A39,A708,XREAL_1:6;
set k=j-'len h11+2-'1;
j<= len h11 + len (mid(h21,2,len h21 -'1)) by A686,FINSEQ_1:22;
then
A711: j-len h11<=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by
XREAL_1:9;
A712: 0+2<=j-'len h11 +2 by XREAL_1:6;
then
A713: j-'len h11+2-'1=j-'len h11+2-1 by Lm1,NAT_D:39,42;
1<=(j-'len h11 +2-'1) by A712,Lm1,NAT_D:42;
then
A714: k in dom h2 by A46,A709,FINSEQ_3:25;
then h2.k in rng h2 by FUNCT_1:def 3;
then
A715: g2.(h2.k) in rng g2 by A131,A29,BORSUK_1:40,FUNCT_1:def 3;
A716: len h1 +1<=j by A706,NAT_1:13;
then h0.j=(mid(h21,2,len h21 -'1)).(j -len h11) & len h1 +1-len h1
<=j-len h1 by A39,A36,A686,FINSEQ_1:23,XREAL_1:9;
then
A717: h0.j=h21.(j-'len h11 +2-'1) by A39,A48,A56,A50,A54,A708,A711,
FINSEQ_6:118;
then h0.j=g2.(h2.k) by A714,FUNCT_1:13;
then h0.j in Upper_Arc(P) /\ Lower_Arc(P) by A23,A696,A701,A703,A707
,A715,XBOOLE_0:def 4;
then
A718: h0.j in {W-min(P),E-max(P)} by A1,JORDAN6:def 9;
len h11+1-len h11<=j-len h11 by A39,A716,XREAL_1:9;
then 1<=j-'len h11 by NAT_D:39;
then 1+2<=j-'len h11+2 by XREAL_1:6;
then 1+2-1<=j-'len h11+2-1 by XREAL_1:9;
then 1 E-max P by A46,A76,A77,A32,A717,A714;
j-'len h11+2-'1 W-min P by A46,A34,A35,A32,A717,A713,A710,A714;
hence contradiction by A718,A719,TARSKI:def 2;
end;
end;
suppose
A720: i+1>len h1;
then
A721: j>len h1 by A691,XXREAL_0:2;
then
A722: len h1 +1<=j by NAT_1:13;
then
A723: len h1 +1-len h1<=j-len h1 by XREAL_1:9;
len h11+1-len h11<=j-len h11 by A39,A722,XREAL_1:9;
then
A724: j-'len h11=j-len h11 by NAT_D:39;
A725: len h1 +1<=i+1 by A720,NAT_1:13;
then len h11+1-len h11<=(i+1)-len h11 by A39,XREAL_1:9;
then (i+1)-'len h11=(i+1)-len h11 by NAT_D:39;
then i+1-'len h11len h1;
set k=j-'len h11+2-'1;
0+2<=j-'len h11 +2 by XREAL_1:6;
then
A765: 2-'1<=j-'len h11 +2-'1 by NAT_D:42;
A766: j-len h11=j-'len h11 by A39,A764,XREAL_1:233;
j-len h11<=len h1+(len h2-2)-len h11 by A39,A47,A36,A52,A55,A57,A686,
XREAL_1:9;
then j-'len h11+2<=len h2-2+2 by A39,A766,XREAL_1:6;
then (j-'len h11 +2-'1)<=len h21 by A47,NAT_D:44;
then
A767: (j-'len h11 +2-'1) in dom h21 by A765,Lm1,FINSEQ_3:25;
j+1-1<=len h1+(len h2-2)-1 by A39,A47,A36,A52,A55,A57,A743,XREAL_1:9;
then j-len h11<=len h1+((len h2-2)-1)-len h11 by XREAL_1:9;
then j-'len h11+2<=len h2-2-1+2 by A39,A766,XREAL_1:6;
then
A768: j-'len h11+2-1<=len h2-1-1 by XREAL_1:9;
A769: h0.(i+1)=h11.(i+1) by A39,A744,A748,FINSEQ_1:64;
i+1 in dom h1 by A744,A748,FINSEQ_3:25;
then h1.(i+1) in rng h1 by FUNCT_1:def 3;
then
A770: g1.(h1.(i+1)) in rng g1 by A132,A11,BORSUK_1:40,FUNCT_1:def 3;
0+1<=j-'len h11+1+1-1 by XREAL_1:6;
then
A771: j-'len h11+2-'1=j-'len h11+2-1 by NAT_D:39;
len h1 +1<=j by A764,NAT_1:13;
then
A772: h0.j=(mid(h21,2,len h21 -'1)).(j -len h11) & len h1 +1-len h1
<=j-len h1 by A39,A36,A686,FINSEQ_1:23,XREAL_1:9;
A773: j-len h11 <=len h11 + len (mid(h21,2,len h21 -'1))-len h11 by A36
,A686,XREAL_1:9;
then h0.j=h21.(j-'len h11 +2-'1) by A39,A48,A56,A50,A54,A766,A772,
FINSEQ_6:118;
then
A774: h0.j=g2.(h2.k) by A46,A767,FUNCT_1:13;
j-len h11=j-'len h11 by A39,A764,XREAL_1:233;
then
A775: h0.j=h21.k by A39,A48,A56,A50,A54,A773,A772,FINSEQ_6:118;
j in dom h0 by A686,A688,FINSEQ_3:25;
then
A776: h0/.j=h0.j by PARTFUN1:def 6;
h2.k in rng h2 by A46,A767,FUNCT_1:def 3;
then
A777: h0.j in Lower_Arc(P) by A23,A131,A29,A774,BORSUK_1:40,FUNCT_1:def 3;
i+1 in Seg len h1 by A745,A748,FINSEQ_1:1;
then i+1 in dom h1 by FINSEQ_1:def 3;
then
A778: h11.(i+1)=g1.(h1.(i+1)) by FUNCT_1:13;
(i+1) in dom h0 by A745,A692,FINSEQ_3:25;
then
A779: h0/.(i+1)=h0.(i+1) by PARTFUN1:def 6;
len h2-1-1 W-min P by A46,A34,A35,A32,A771,A767,A768,A775,A776;
hence thesis by A5,A769,A778,A779,A776,A770,A777,JORDAN6:def 10;
end;
end;
suppose
A780: i+1>len h1;
set j0=(i+1)-'len h11+2-'1;
set k=j-'len h11+2-'1;
A781: 0+2<=(i+1)-'len h11 +2 by XREAL_1:6;
then
A782: 1<=((i+1)-'len h11 +2-'1) by Lm1,NAT_D:42;
A783: j-len h11=j-'len h11 by A39,A691,A780,XREAL_1:233,XXREAL_0:2;
len h1 W-min P by A46,A34,A35,A32,A796,A798,A795,A788,A809;
h21.k=g2.(h2.k) by A46,A798,FUNCT_1:13;
then LE h0/.(i+1),h0/.j,Lower_Arc(P),E-max(P),W-min(P) by A21,A22,A23
,A24,A25,A801,A800,A810,A792,A805,A806,A809,Th18;
hence thesis by A23,A810,A806,A809,A793,A802,A811,JORDAN6:def 10;
end;
end;
LE h0/.j,h0/.(j+1),P by A256,A688,A743;
hence thesis by A1,A690,A747,A695,Th13;
end;
let i be Nat such that
A812: 1 < i and
A813: i+1 < len h0;
A814: 1 E-max P by A46,A76,A77,A32,A829,A827;
len h0-'len h11+2-'1 W-min P by A46,A47,A34,A35,A36,A52,A55,A57,A252,A32
,A829,A827;
hence contradiction by A830,A831,TARSKI:def 2;
end;
suppose
A832: i+1>len h1;
set k=len h0-'len h11+2-'1;
set j0=(i+1)-'len h11+2-'1;
A833: 0+2<=len h0-'len h11 +2 by XREAL_1:6;
then
A834: 2-'1<=(len h0-'len h11 +2-'1) by NAT_D:42;
len h0-'len h11 +2-'1 <= len h21 by A36,A52,A55,A57,A252,NAT_D:44;
then
A835: k in dom h2 by A46,A834,Lm1,FINSEQ_3:25;
i+1 <= len h11 + len mid(h21,2,len h21 -'1) by A813,FINSEQ_1:22;
then
A836: i+1-len h11 <=len h11 + len mid(h21,2,len h21 -'1)-len h11 by XREAL_1:9;
A837: len h1 +1<=i+1 by A832,NAT_1:13;
then len h11+1-len h11<=(i+1)-len h11 by A39,XREAL_1:9;
then
A838: (i+1)-'len h11=(i+1)-len h11 by NAT_D:39;
len h0-'len h11=len h0-len h11 by A36,A57,XREAL_0:def 2;
then i+1-'len h11len h1;
then len h1+1<=i+1 by NAT_1:13;
then
A856: len h1+1-len h1<=i+1-len h1 by XREAL_1:9;
then
A857: i+1-'len h11=i+1-len h11 by A39,NAT_D:39;
A858: i+1-len h11W-min P by A72,A67,A78,A812,A878;
LE h0/.i,h0/.(i+1),P by A256,A812,A813;
hence thesis by A1,A72,A68,A879,A850,A817,Th14;
end;