### The Mizar article:

### On the Order on a Special Polygon

**by****Andrzej Trybulec, and****Yatsuka Nakamura**

- Received November 30, 1997
Copyright (c) 1997 Association of Mizar Users

- MML identifier: SPRECT_2
- [ MML identifier index ]

environ vocabulary BOOLE, TARSKI, FINSEQ_1, RELAT_1, JORDAN3, ARYTM_1, FINSEQ_4, FUNCT_1, COMPTS_1, EUCLID, PRE_TOPC, MCART_1, PSCOMP_1, TOPREAL1, GOBOARD1, REALSET1, GOBOARD4, FINSEQ_6, SEQM_3, GOBOARD5, FUNCT_5, SUBSET_1, ORDINAL2, SPPOL_1, SPRECT_1, SPPOL_2, FINSEQ_5, TOPREAL2, SPRECT_2, ARYTM; notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XREAL_0, REAL_1, FUNCT_1, FUNCT_2, FINSEQ_1, STRUCT_0, FINSEQ_4, FINSEQ_5, REALSET1, FINSEQ_6, NAT_1, BINARITH, PRE_TOPC, COMPTS_1, EUCLID, TOPREAL1, TOPREAL2, GOBOARD1, GOBOARD4, SPPOL_1, SPPOL_2, GOBOARD5, JORDAN3, PSCOMP_1, SPRECT_1; constructors PSCOMP_1, GOBOARD5, JORDAN3, GOBOARD4, BINARITH, REALSET1, SPPOL_1, FINSEQ_5, REAL_1, SEQM_3, TOPREAL4, SPRECT_1, TOPREAL2, COMPTS_1, FINSEQ_4, GOBOARD1; clusters STRUCT_0, EUCLID, RELSET_1, GOBOARD5, SPPOL_2, GOBOARD2, GOBOARD4, PSCOMP_1, SPRECT_1, XREAL_0, FINSEQ_1, ARYTM_3, MEMBERED; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; definitions TARSKI, GOBOARD4, TOPREAL1, XBOOLE_0; theorems FINSEQ_6, FINSEQ_4, FINSEQ_5, REAL_1, GOBOARD4, GOBOARD1, PSCOMP_1, FINSEQ_3, JORDAN3, AXIOMS, REAL_2, NAT_1, SPPOL_1, CQC_THE1, TOPREAL4, FINSEQ_1, GROUP_5, JORDAN4, ZFMISC_1, SPPOL_2, TOPREAL3, TARSKI, FUNCT_1, TOPREAL1, GOBOARD2, AMI_5, BINARITH, GOBOARD7, PARTFUN2, GOBOARD5, EUCLID, TOPREAL2, FUNCT_2, PRE_TOPC, RELAT_1, SPRECT_1, TOPREAL5, SCMFSA_7, XBOOLE_0, XBOOLE_1, SQUARE_1, XCMPLX_1; begin :: Preliminaries theorem Th1: for A,B,C,p being set st A /\ B c= {p} & p in C & C misses B holds A \/ C misses B proof let A,B,C,p be set such that A1: A /\ B c= {p} and A2: p in C and A3: C misses B; {p} c= C by A2,ZFMISC_1:37; then A /\ B c= C by A1,XBOOLE_1:1; then A /\ B /\ B c= C /\ B by XBOOLE_1:27; then A4: A /\ (B /\ B) c= C /\ B by XBOOLE_1:16; (A \/ C) /\ B = A /\ B \/ C /\ B by XBOOLE_1:23 .= C /\ B by A4,XBOOLE_1:12 .= {} by A3,XBOOLE_0:def 7; hence A \/ C misses B by XBOOLE_0:def 7; end; theorem Th2: for A,B,C,p being set st A /\ C = {p} & p in B & B c= C holds A /\ B = {p} proof let A,B,C,p be set such that A1: A /\ C = {p} and A2: p in B and A3: B c= C; A4: {p} c= B by A2,ZFMISC_1:37; thus A /\ B = A /\ (C /\ B) by A3,XBOOLE_1:28 .= {p} /\ B by A1,XBOOLE_1:16 .= {p} by A4,XBOOLE_1:28; end; canceled; theorem Th4: for A,B being set st for x,y being set st x in A & y in B holds x misses y holds union A misses union B proof let A,B be set such that A1: for x,y being set st x in A & y in B holds x misses y; for y being set st y in B holds union A misses y proof let y be set; assume y in B; then for x being set st x in A holds x misses y by A1; hence union A misses y by ZFMISC_1:98; end; hence union A misses union B by ZFMISC_1:98; end; begin :: Finite sequences reserve i,j,k,l,m,n for Nat, D for non empty set, f for FinSequence of D; theorem Th5: i <= j & i in dom f & j in dom f & k in dom mid(f,i,j) implies k+i-'1 in dom f proof assume that A1: i <= j and A2: i in dom f and A3: j in dom f; A4: 1+0 <= i & i <= len f by A2,FINSEQ_3:27; A5: 1 <= j & j <= len f by A3,FINSEQ_3:27; then A6: len mid(f,i,j) = j -' i +1 by A1,A4,JORDAN3:27; k+i >= i by NAT_1:29; then A7: k+i >= 1 by A4,AXIOMS:22; assume A8: k in dom mid(f,i,j); then k <= len mid(f,i,j) by FINSEQ_3:27; then k <= j - i +1 by A1,A6,SCMFSA_7:3; then k <= j +1 - i by XCMPLX_1:29; then k+i <= j +1 by REAL_1:84; then k+i - 1 <= j by REAL_1:86; then k+i -' 1 <= j by A7,SCMFSA_7:3; then A9: k+i-'1 <= len f by A5,AXIOMS:22; A10: 1 <= k by A8,FINSEQ_3:27; i-1 >= 0 by A4,REAL_1:84; then k+0 <= k+(i-1) by AXIOMS:24; then 1 <= k+(i-1) by A10,AXIOMS:22; then 1 <= k+i-1 by XCMPLX_1:29; then 1 <= k+i-'1 by JORDAN3:1; hence k+i-'1 in dom f by A9,FINSEQ_3:27; end; theorem Th6: i > j & i in dom f & j in dom f & k in dom mid(f,i,j) implies i -' k + 1 in dom f proof assume that A1: i > j and A2: i in dom f and A3: j in dom f; A4: 1+0 <= i & i <= len f by A2,FINSEQ_3:27; A5: 1+0 <= j & j <= len f by A3,FINSEQ_3:27; then A6: len mid(f,i,j) = i -' j +1 by A1,A4,JORDAN3:27; 1 - j <= 0 by A5,REAL_2:106; then A7: i +(1 - j) <= i + 0 by AXIOMS:24; assume A8: k in dom mid(f,i,j); then k <= len mid(f,i,j) by FINSEQ_3:27; then k <= i - j +1 by A1,A6,SCMFSA_7:3; then k <= i +1 - j by XCMPLX_1:29; then k <= i +(1 - j) by XCMPLX_1:29; then A9: k <= i by A7,AXIOMS:22; k >= 1 by A8,FINSEQ_3:27; then 1 - k <= 0 by REAL_2:106; then i + (1 - k) <= i+0 by AXIOMS:24; then i + 1 - k <= i by XCMPLX_1:29; then i - k + 1 <= i by XCMPLX_1:29; then i -' k + 1 <= i by A9,SCMFSA_7:3; then A10: i -' k + 1 <= len f by A4,AXIOMS:22; 1 <= i -' k + 1 by NAT_1:29; hence i -' k + 1 in dom f by A10,FINSEQ_3:27; end; theorem Th7: i <= j & i in dom f & j in dom f & k in dom mid(f,i,j) implies (mid(f,i,j))/.k = f/.(k+i-'1) proof assume that A1: i <= j and A2: i in dom f and A3: j in dom f and A4: k in dom mid(f,i,j); A5: k+i-'1 in dom f by A1,A2,A3,A4,Th5; A6: 1 <= i & i <= len f by A2,FINSEQ_3:27; A7: 1 <= j & j <= len f by A3,FINSEQ_3:27; A8: 1 <= k & k <= len mid(f,i,j) by A4,FINSEQ_3:27; thus (mid(f,i,j))/.k = mid(f,i,j).k by A4,FINSEQ_4:def 4 .= f.(k+i-'1) by A1,A6,A7,A8,JORDAN3:27 .= f/.(k+i-'1) by A5,FINSEQ_4:def 4; end; theorem Th8: i > j & i in dom f & j in dom f & k in dom mid(f,i,j) implies (mid(f,i,j))/.k = f/.(i-' k +1) proof assume that A1: i > j and A2: i in dom f and A3: j in dom f and A4: k in dom mid(f,i,j); A5: i -' k +1 in dom f by A1,A2,A3,A4,Th6; A6: 1 <= i & i <= len f by A2,FINSEQ_3:27; A7: 1 <= j & j <= len f by A3,FINSEQ_3:27; A8: 1 <= k & k <= len mid(f,i,j) by A4,FINSEQ_3:27; thus (mid(f,i,j))/.k = mid(f,i,j).k by A4,FINSEQ_4:def 4 .= f.(i -' k +1) by A1,A6,A7,A8,JORDAN3:27 .= f/.(i-' k +1) by A5,FINSEQ_4:def 4; end; theorem Th9: i in dom f & j in dom f implies len mid(f,i,j) >= 1 proof assume i in dom f; then A1: 1 <= i & i <= len f by FINSEQ_3:27; assume j in dom f; then A2: 1 <= j & j <= len f by FINSEQ_3:27; i <= j or j < i; then len mid(f,i,j)=i-'j+1 or len mid(f,i,j)=j-'i+1 by A1,A2,JORDAN3:27; hence thesis by NAT_1:29; end; theorem Th10: i in dom f & j in dom f & len mid(f,i,j) = 1 implies i = j proof assume i in dom f; then A1: 1 <= i & i <= len f by FINSEQ_3:27; assume j in dom f; then A2: 1 <= j & j <= len f by FINSEQ_3:27; assume A3: len mid(f,i,j) = 1; per cases; suppose A4: i <= j; then 0 + 1 = j -' i + 1 by A1,A2,A3,JORDAN4:20; then 0 = j -' i by XCMPLX_1:2; then 0 = j - i by A4,SCMFSA_7:3; hence thesis by XCMPLX_1:15; suppose A5: i >= j; then 0 + 1 = i -' j + 1 by A1,A2,A3,JORDAN4:21; then 0 = i -' j by XCMPLX_1:2; then 0 = i - j by A5,SCMFSA_7:3; hence thesis by XCMPLX_1:15; end; theorem Th11: i in dom f & j in dom f implies mid(f,i,j) is non empty proof assume i in dom f & j in dom f; then len mid(f,i,j) >= 1 by Th9; hence mid(f,i,j) is non empty by FINSEQ_3:27,RELAT_1:60; end; theorem Th12: i in dom f & j in dom f implies (mid(f,i,j))/.1 = f/.i proof assume A1: i in dom f; then A2: 1 <= i & i <= len f by FINSEQ_3:27; assume A3:j in dom f; then A4: 1 <= j & j <= len f by FINSEQ_3:27; mid(f,i,j) is non empty by A1,A3,Th11; then 1 in dom mid(f,i,j) by FINSEQ_5:6; hence (mid(f,i,j))/.1 = mid(f,i,j).1 by FINSEQ_4:def 4 .= f.i by A2,A4,JORDAN3:27 .= f/.i by A1,FINSEQ_4:def 4; end; theorem Th13: i in dom f & j in dom f implies (mid(f,i,j))/.len mid(f,i,j) = f/.j proof assume A1: i in dom f; then A2: 1 <= i & i <= len f by FINSEQ_3:27; assume A3:j in dom f; then A4: 1 <= j & j <= len f by FINSEQ_3:27; mid(f,i,j) is non empty by A1,A3,Th11; then len mid(f,i,j) in dom mid(f,i,j) by FINSEQ_5:6; hence (mid(f,i,j))/.len mid(f,i,j) = mid(f,i,j).len mid(f,i,j) by FINSEQ_4:def 4 .= f.j by A2,A4,JORDAN4:23 .= f/.j by A3,FINSEQ_4:def 4; end; begin :: Compact sets on the plane reserve X for compact Subset of TOP-REAL 2; theorem Th14: for p being Point of TOP-REAL 2 st p in X & p`2 = N-bound X holds p in N-most X proof let p be Point of TOP-REAL 2 such that A1: p in X and A2: p`2 = N-bound X; A3: N-most X = LSeg(NW-corner X, NE-corner X)/\X by PSCOMP_1:def 39; A4: (NW-corner X)`2 = N-bound X &(NE-corner X)`2 = N-bound X by PSCOMP_1:75,77; A5: (NW-corner X)`1 = W-bound X &(NE-corner X)`1 = E-bound X by PSCOMP_1:74,76; W-bound X <= p`1 & p`1 <= E-bound X by A1,PSCOMP_1:71; then p in LSeg(NW-corner X, NE-corner X) by A2,A4,A5,GOBOARD7:9; hence p in N-most X by A1,A3,XBOOLE_0:def 3; end; theorem Th15: for p being Point of TOP-REAL 2 st p in X & p`2 = S-bound X holds p in S-most X proof let p be Point of TOP-REAL 2 such that A1: p in X and A2: p`2 = S-bound X; A3: S-most X = LSeg(SW-corner X, SE-corner X)/\X by PSCOMP_1:def 41; A4: (SW-corner X)`2 = S-bound X &(SE-corner X)`2 = S-bound X by PSCOMP_1:73,79; A5: (SW-corner X)`1 = W-bound X &(SE-corner X)`1 = E-bound X by PSCOMP_1:72,78; W-bound X <= p`1 & p`1 <= E-bound X by A1,PSCOMP_1:71; then p in LSeg(SW-corner X, SE-corner X) by A2,A4,A5,GOBOARD7:9; hence p in S-most X by A1,A3,XBOOLE_0:def 3; end; theorem Th16: for p being Point of TOP-REAL 2 st p in X & p`1 = W-bound X holds p in W-most X proof let p be Point of TOP-REAL 2 such that A1: p in X and A2: p`1 = W-bound X; A3: W-most X = LSeg(SW-corner X, NW-corner X)/\X by PSCOMP_1:def 38; A4: (SW-corner X)`1 = W-bound X &(NW-corner X)`1 = W-bound X by PSCOMP_1:72,74; A5: (SW-corner X)`2 = S-bound X &(NW-corner X)`2 = N-bound X by PSCOMP_1:73,75; S-bound X <= p`2 & p`2 <= N-bound X by A1,PSCOMP_1:71; then p in LSeg(SW-corner X, NW-corner X) by A2,A4,A5,GOBOARD7:8; hence p in W-most X by A1,A3,XBOOLE_0:def 3; end; theorem Th17: for p being Point of TOP-REAL 2 st p in X & p`1 = E-bound X holds p in E-most X proof let p be Point of TOP-REAL 2 such that A1: p in X and A2: p`1 = E-bound X; A3: E-most X = LSeg(SE-corner X, NE-corner X)/\X by PSCOMP_1:def 40; A4: (SE-corner X)`1 = E-bound X &(NE-corner X)`1 = E-bound X by PSCOMP_1:76,78; A5: (SE-corner X)`2 = S-bound X &(NE-corner X)`2 = N-bound X by PSCOMP_1:77,79; S-bound X <= p`2 & p`2 <= N-bound X by A1,PSCOMP_1:71; then p in LSeg(SE-corner X, NE-corner X) by A2,A4,A5,GOBOARD7:8; hence p in E-most X by A1,A3,XBOOLE_0:def 3; end; begin :: Finite sequences on the plane theorem Th18: for f being FinSequence of TOP-REAL 2 st 1 <= i & i <= j & j <= len f holds L~mid(f,i,j) = union{ LSeg(f,k): i <= k & k < j} proof let f be FinSequence of TOP-REAL 2; assume that A1: 1 <= i and A2: i <= j and A3: j <= len f; set A = { LSeg(mid(f,i,j),m) : 1 <= m & m+1 <= len mid(f,i,j) }, B = { LSeg(f,l): i <= l & l < j}; per cases by A2,REAL_1:def 5; suppose A4: i = j; then A5: mid(f,i,j) = <*f/.i*> by A1,A3,JORDAN4:27; B = {} proof assume B <> {}; then consider z being set such that A6: z in B by XBOOLE_0:def 1; ex l st z = LSeg(f,l) & i <= l & l < j by A6; hence contradiction by A4; end; hence thesis by A5,SPPOL_2:12,ZFMISC_1:2; suppose A7: i < j; A = B proof hereby let x be set; assume x in A; then consider m such that A8: x = LSeg(mid(f,i,j),m) and A9: 0+1 <= m and A10: m+1 <= len mid(f,i,j); m+i >= m by NAT_1:29; then A11: m+i >= 1 by A9,AXIOMS:22; len mid(f,i,j) = j -' i + 1 by A1,A3,A7,JORDAN4:20; then A12: m < j -' i + 1 by A10,NAT_1:38; then m <= j -' i by NAT_1:38; then m <= j - i by A7,SCMFSA_7:3; then m+i <= j by REAL_1:84; then m+i-'1+1 <= j by A11,AMI_5:4; then A13: m+i-'1 < j by NAT_1:38; m > 0 by A9,NAT_1:38; then i < m+i by REAL_1:69; then A14: i <= m+i-'1 by JORDAN3:12; x = LSeg(f,m+i-'1) by A1,A3,A7,A8,A9,A12,JORDAN4:31; hence x in B by A13,A14; end; let x be set; assume x in B; then consider l such that A15: x = LSeg(f,l) and A16: i <= l and A17: l < j; set m = l -' i + 1; A18: 1 <= m by NAT_1:29; A19: len mid(f,i,j) = j -' i + 1 by A1,A3,A7,JORDAN4:20; j > i by A16,A17,AXIOMS:22; then A20: l -' i = l - i & j -' i = j - i by A16,SCMFSA_7:3; l - i < j - i by A17,REAL_1:54; then A21: m < j-'i+1 by A20,REAL_1:53; then A22: m+1 <= len mid(f,i,j) by A19,NAT_1:38; m+i-'1 = l -' i + i + 1 -' 1 by XCMPLX_1:1 .= l + 1 -' 1 by A16,AMI_5:4 .= l by BINARITH:39; then x = LSeg(mid(f,i,j),m) by A1,A3,A7,A15,A18,A21,JORDAN4:31; hence x in A by A18,A22; end; hence L~mid(f,i,j) = union B by TOPREAL1:def 6; end; theorem Th19: for f being FinSequence of TOP-REAL 2 holds dom X_axis f = dom f proof let f be FinSequence of TOP-REAL 2; len X_axis f = len f by GOBOARD1:def 3; hence dom X_axis f = dom f by FINSEQ_3:31; end; theorem Th20: for f being FinSequence of TOP-REAL 2 holds dom Y_axis f = dom f proof let f be FinSequence of TOP-REAL 2; len Y_axis f = len f by GOBOARD1:def 4; hence dom Y_axis f = dom f by FINSEQ_3:31; end; reserve p,q,r for Real; theorem Th21: for a,b,c being Point of TOP-REAL 2 st b in LSeg(a,c) & a`1 <= b`1 & c`1 <= b`1 holds a = b or b = c or a`1 = b`1 & c`1 = b`1 proof let a,b,c be Point of TOP-REAL 2 such that A1: b in LSeg(a,c) and A2: a`1 <= b`1 & c`1 <= b`1; LSeg(a,c) = { (1-r)*a + r*c : 0 <= r & r <= 1 } by TOPREAL1:def 4; then consider r such that A3: b = (1-r)*a + r*c and 0 <= r & r <= 1 by A1; per cases by A2,REAL_1:def 5; suppose that A4: a`1 = b`1 and A5: c`1 < b`1; b`1 + 0 = ((1-r)*a)`1 + (r*c)`1 by A3,TOPREAL3:7 .= ((1-r)*a)`1 + r*c`1 by TOPREAL3:9 .= (1-r)*b`1 + r*c`1 by A4,TOPREAL3:9 .= 1*b`1-r*b`1 + r*c`1 by XCMPLX_1:40 .= b`1 + r*c`1-r*b`1 by XCMPLX_1:29 .= b`1 + (r*c`1-r*b`1) by XCMPLX_1:29; then A6: 0 = r*c`1-r*b`1 by XCMPLX_1:2 .= r*(c`1-b`1) by XCMPLX_1:40; c`1-b`1 < 0 by A5,REAL_2:105; then r = 0 by A6,XCMPLX_1:6; then b = 1*a + 0.REAL 2 by A3,EUCLID:33 .= 1*a by EUCLID:31 .= a by EUCLID:33; hence thesis; suppose that A7: a`1 < b`1 and A8: c`1 = b`1; b`1 = ((1-r)*a)`1 + (r*c)`1 by A3,TOPREAL3:7 .= ((1-r)*a)`1 + r*c`1 by TOPREAL3:9 .= (1-r)*a`1 + r*b`1 by A8,TOPREAL3:9; then A9: 0 = (1-r)*a`1 + r*b`1 - b`1 by XCMPLX_1:14 .= (1-r)*a`1 - b`1 + r*b`1 by XCMPLX_1:29 .= (1-r)*a`1 - (1*b`1 - r*b`1) by XCMPLX_1:37 .= (1-r)*a`1-(1-r)*b`1 by XCMPLX_1:40 .= (1-r)*(a`1-b`1) by XCMPLX_1:40; a`1-b`1 < 0 by A7,REAL_2:105; then 1 - r = 0 by A9,XCMPLX_1:6; then b = 0 * a + 1*c by A3,XCMPLX_1:15 .= 0.REAL 2 + 1*c by EUCLID:33 .= 1*c by EUCLID:31 .= c by EUCLID:33; hence thesis; suppose that A10: a`1 < b`1 & c`1 < b`1; a`1 <= c`1 or c`1 <= a`1; hence thesis by A1,A10,TOPREAL1:9; suppose a`1 = b`1 & c`1 = b`1; hence thesis; end; theorem Th22: for a,b,c being Point of TOP-REAL 2 st b in LSeg(a,c) & a`2 <= b`2 & c`2 <= b`2 holds a = b or b = c or a`2 = b`2 & c`2 = b`2 proof let a,b,c be Point of TOP-REAL 2 such that A1: b in LSeg(a,c) and A2: a`2 <= b`2 & c`2 <= b`2; LSeg(a,c) = { (1-r)*a + r*c : 0 <= r & r <= 1 } by TOPREAL1:def 4; then consider r such that A3: b = (1-r)*a + r*c and 0 <= r & r <= 1 by A1; per cases by A2,REAL_1:def 5; suppose that A4: a`2 = b`2 and A5: c`2 < b`2; b`2 + 0 = ((1-r)*a)`2 + (r*c)`2 by A3,TOPREAL3:7 .= ((1-r)*a)`2 + r*c`2 by TOPREAL3:9 .= (1-r)*b`2 + r*c`2 by A4,TOPREAL3:9 .= 1*b`2-r*b`2 + r*c`2 by XCMPLX_1:40 .= b`2 + r*c`2-r*b`2 by XCMPLX_1:29 .= b`2 + (r*c`2-r*b`2) by XCMPLX_1:29; then A6: 0 = r*c`2-r*b`2 by XCMPLX_1:2 .= r*(c`2-b`2) by XCMPLX_1:40; c`2-b`2 < 0 by A5,REAL_2:105; then r = 0 by A6,XCMPLX_1:6; then b = 1*a + 0.REAL 2 by A3,EUCLID:33 .= 1*a by EUCLID:31 .= a by EUCLID:33; hence thesis; suppose that A7: a`2 < b`2 and A8: c`2 = b`2; b`2 = ((1-r)*a)`2 + (r*c)`2 by A3,TOPREAL3:7 .= ((1-r)*a)`2 + r*c`2 by TOPREAL3:9 .= (1-r)*a`2 + r*b`2 by A8,TOPREAL3:9; then A9: 0 = (1-r)*a`2 + r*b`2 - b`2 by XCMPLX_1:14 .= (1-r)*a`2 - b`2 + r*b`2 by XCMPLX_1:29 .= (1-r)*a`2 - (1*b`2 - r*b`2) by XCMPLX_1:37 .= (1-r)*a`2-(1-r)*b`2 by XCMPLX_1:40 .= (1-r)*(a`2-b`2) by XCMPLX_1:40; a`2-b`2 < 0 by A7,REAL_2:105; then 1 - r = 0 by A9,XCMPLX_1:6; then b = 0 * a + 1*c by A3,XCMPLX_1:15 .= 0.REAL 2 + 1*c by EUCLID:33 .= 1*c by EUCLID:31 .= c by EUCLID:33; hence thesis; suppose that A10: a`2 < b`2 & c`2 < b`2; a`2 <= c`2 or c`2 <= a`2; hence thesis by A1,A10,TOPREAL1:10; suppose a`2 = b`2 & c`2 = b`2; hence thesis; end; theorem Th23: for a,b,c being Point of TOP-REAL 2 st b in LSeg(a,c) & a`1 >= b`1 & c`1 >= b`1 holds a = b or b = c or a`1 = b`1 & c`1 = b`1 proof let a,b,c be Point of TOP-REAL 2 such that A1: b in LSeg(a,c) and A2: a`1 >= b`1 & c`1 >= b`1; LSeg(a,c) = { (1-r)*a + r*c : 0 <= r & r <= 1 } by TOPREAL1:def 4; then consider r such that A3: b = (1-r)*a + r*c and 0 <= r & r <= 1 by A1; per cases by A2,REAL_1:def 5; suppose that A4: a`1 = b`1 and A5: c`1 > b`1; b`1 + 0 = ((1-r)*a)`1 + (r*c)`1 by A3,TOPREAL3:7 .= ((1-r)*a)`1 + r*c`1 by TOPREAL3:9 .= (1-r)*b`1 + r*c`1 by A4,TOPREAL3:9 .= 1*b`1-r*b`1 + r*c`1 by XCMPLX_1:40 .= b`1 + r*c`1-r*b`1 by XCMPLX_1:29 .= b`1 + (r*c`1-r*b`1) by XCMPLX_1:29; then A6: 0 = r*c`1-r*b`1 by XCMPLX_1:2 .= r*(c`1-b`1) by XCMPLX_1:40; c`1-b`1 > 0 by A5,SQUARE_1:11; then r = 0 by A6,XCMPLX_1:6; then b = 1*a + 0.REAL 2 by A3,EUCLID:33 .= 1*a by EUCLID:31 .= a by EUCLID:33; hence thesis; suppose that A7: a`1 > b`1 and A8: c`1 = b`1; b`1 = ((1-r)*a)`1 + (r*c)`1 by A3,TOPREAL3:7 .= ((1-r)*a)`1 + r*c`1 by TOPREAL3:9 .= (1-r)*a`1 + r*b`1 by A8,TOPREAL3:9; then A9: 0 = (1-r)*a`1 + r*b`1 - b`1 by XCMPLX_1:14 .= (1-r)*a`1 - b`1 + r*b`1 by XCMPLX_1:29 .= (1-r)*a`1 - (1*b`1 - r*b`1) by XCMPLX_1:37 .= (1-r)*a`1-(1-r)*b`1 by XCMPLX_1:40 .= (1-r)*(a`1-b`1) by XCMPLX_1:40; a`1-b`1 > 0 by A7,SQUARE_1:11; then 1 - r = 0 by A9,XCMPLX_1:6; then b = 0 * a + 1*c by A3,XCMPLX_1:15 .= 0.REAL 2 + 1*c by EUCLID:33 .= 1*c by EUCLID:31 .= c by EUCLID:33; hence thesis; suppose that A10: a`1 > b`1 & c`1 > b`1; a`1 >= c`1 or c`1 >= a`1; hence thesis by A1,A10,TOPREAL1:9; suppose a`1 = b`1 & c`1 = b`1; hence thesis; end; theorem Th24: for a,b,c being Point of TOP-REAL 2 st b in LSeg(a,c) & a`2 >= b`2 & c`2 >= b`2 holds a = b or b = c or a`2 = b`2 & c`2 = b`2 proof let a,b,c be Point of TOP-REAL 2 such that A1: b in LSeg(a,c) and A2: a`2 >= b`2 & c`2 >= b`2; LSeg(a,c) = { (1-r)*a + r*c : 0 <= r & r <= 1 } by TOPREAL1:def 4; then consider r such that A3: b = (1-r)*a + r*c and 0 <= r & r <= 1 by A1; per cases by A2,REAL_1:def 5; suppose that A4: a`2 = b`2 and A5: c`2 > b`2; b`2 + 0 = ((1-r)*a)`2 + (r*c)`2 by A3,TOPREAL3:7 .= ((1-r)*a)`2 + r*c`2 by TOPREAL3:9 .= (1-r)*b`2 + r*c`2 by A4,TOPREAL3:9 .= 1*b`2-r*b`2 + r*c`2 by XCMPLX_1:40 .= b`2 + r*c`2-r*b`2 by XCMPLX_1:29 .= b`2 + (r*c`2-r*b`2) by XCMPLX_1:29; then A6: 0 = r*c`2-r*b`2 by XCMPLX_1:2 .= r*(c`2-b`2) by XCMPLX_1:40; c`2-b`2 > 0 by A5,SQUARE_1:11; then r = 0 by A6,XCMPLX_1:6; then b = 1*a + 0.REAL 2 by A3,EUCLID:33 .= 1*a by EUCLID:31 .= a by EUCLID:33; hence thesis; suppose that A7: a`2 > b`2 and A8: c`2 = b`2; b`2 = ((1-r)*a)`2 + (r*c)`2 by A3,TOPREAL3:7 .= ((1-r)*a)`2 + r*c`2 by TOPREAL3:9 .= (1-r)*a`2 + r*b`2 by A8,TOPREAL3:9; then A9: 0 = (1-r)*a`2 + r*b`2 - b`2 by XCMPLX_1:14 .= (1-r)*a`2 - b`2 + r*b`2 by XCMPLX_1:29 .= (1-r)*a`2 - (1*b`2 - r*b`2) by XCMPLX_1:37 .= (1-r)*a`2-(1-r)*b`2 by XCMPLX_1:40 .= (1-r)*(a`2-b`2) by XCMPLX_1:40; a`2-b`2 > 0 by A7,SQUARE_1:11; then 1 - r = 0 by A9,XCMPLX_1:6; then b = 0 * a + 1*c by A3,XCMPLX_1:15 .= 0.REAL 2 + 1*c by EUCLID:33 .= 1*c by EUCLID:31 .= c by EUCLID:33; hence thesis; suppose that A10: a`2 > b`2 & c`2 > b`2; a`2 >= c`2 or c`2 >= a`2; hence thesis by A1,A10,TOPREAL1:10; suppose a`2 = b`2 & c`2 = b`2; hence thesis; end; begin :: The area of a sequence definition let f, g be FinSequence of TOP-REAL 2; pred g is_in_the_area_of f means :Def1: for n st n in dom g holds W-bound L~f <= (g/.n)`1 & (g/.n)`1 <= E-bound L~f & S-bound L~f <= (g/.n)`2 & (g/.n)`2 <= N-bound L~f; end; theorem Th25: for f being non trivial FinSequence of TOP-REAL 2 holds f is_in_the_area_of f proof let f be non trivial FinSequence of TOP-REAL 2; let n; A1: len f >= 2 by SPPOL_1:2; assume n in dom f; then f/.n in L~f by A1,GOBOARD1:16; hence W-bound L~f <= (f/.n)`1 & (f/.n)`1 <= E-bound L~f & S-bound L~f <= (f/.n)`2 & (f/.n)`2 <= N-bound L~f by PSCOMP_1:71; end; theorem Th26: for f, g being FinSequence of TOP-REAL 2 st g is_in_the_area_of f for i,j st i in dom g & j in dom g holds mid(g,i,j) is_in_the_area_of f proof let f, g be FinSequence of TOP-REAL 2 such that A1: for n st n in dom g holds W-bound L~f <= (g/.n)`1 & (g/.n)`1 <= E-bound L~f & S-bound L~f <= (g/.n)`2 & (g/.n)`2 <= N-bound L~f; let i,j such that A2: i in dom g and A3: j in dom g; set h = mid(g,i,j); per cases; suppose A4: i <= j; let n; assume A5: n in dom h; then A6: n+i-'1 in dom g by A2,A3,A4,Th5; h/.n = g/.(n+i-'1) by A2,A3,A4,A5,Th7; hence W-bound L~f <= (h/.n)`1 & (h/.n)`1 <= E-bound L~f & S-bound L~f <= (h/.n)`2 & (h/.n)`2 <= N-bound L~f by A1,A6; suppose A7: i > j; let n; assume A8: n in dom h; then A9: i -' n + 1 in dom g by A2,A3,A7,Th6; h/.n = g/.(i -' n + 1) by A2,A3,A7,A8,Th8; hence W-bound L~f <= (h/.n)`1 & (h/.n)`1 <= E-bound L~f & S-bound L~f <= (h/.n)`2 & (h/.n)`2 <= N-bound L~f by A1,A9; end; theorem Th27: for f being non trivial FinSequence of TOP-REAL 2 for i,j st i in dom f & j in dom f holds mid(f,i,j) is_in_the_area_of f proof let f be non trivial FinSequence of TOP-REAL 2, i,j; f is_in_the_area_of f by Th25; hence thesis by Th26; end; theorem Th28: for f,g,h being FinSequence of TOP-REAL 2 st g is_in_the_area_of f & h is_in_the_area_of f holds g^h is_in_the_area_of f proof let f,g,h be FinSequence of TOP-REAL 2 such that A1: g is_in_the_area_of f and A2: h is_in_the_area_of f; let n; assume A3: n in dom(g^h); per cases by A3,FINSEQ_1:38; suppose A4: n in dom g; then (g^h)/.n = g/.n by GROUP_5:95; hence W-bound L~f <= ((g^h)/.n)`1 & ((g^h)/.n)`1 <= E-bound L~f & S-bound L~f <= ((g^h)/.n)`2 & ((g^h)/.n)`2 <= N-bound L~f by A1,A4,Def1; suppose ex i st i in dom h & n = len g + i; then consider i such that A5: i in dom h and A6: n = len g + i; (g^h)/.n = h/.i by A5,A6,GROUP_5:96; hence W-bound L~f <= ((g^h)/.n)`1 & ((g^h)/.n)`1 <= E-bound L~f & S-bound L~f <= ((g^h)/.n)`2 & ((g^h)/.n)`2 <= N-bound L~f by A2,A5,Def1; end; theorem Th29: for f being non trivial FinSequence of TOP-REAL 2 holds <*NE-corner L~f*> is_in_the_area_of f proof let f be non trivial FinSequence of TOP-REAL 2; set g = <*NE-corner L~f*>; let n; A1: dom g = {1} by FINSEQ_1:4,55; assume n in dom g; then n = 1 by A1,TARSKI:def 1; then g/.n = NE-corner L~f by FINSEQ_4:25 .= |[E-bound L~f, N-bound L~f]| by PSCOMP_1:def 36; then (g/.n)`1 = E-bound L~f & (g/.n)`2 = N-bound L~f by EUCLID:56; hence W-bound L~f <= (g/.n)`1 & (g/.n)`1 <= E-bound L~f & S-bound L~f <= (g/.n)`2 & (g/.n)`2 <= N-bound L~f by SPRECT_1:23,24; end; theorem Th30: for f being non trivial FinSequence of TOP-REAL 2 holds <*NW-corner L~f*> is_in_the_area_of f proof let f be non trivial FinSequence of TOP-REAL 2; set g = <*NW-corner L~f*>; let n; A1: dom g = {1} by FINSEQ_1:4,55; assume n in dom g; then n = 1 by A1,TARSKI:def 1; then g/.n = NW-corner L~f by FINSEQ_4:25 .= |[W-bound L~f, N-bound L~f]| by PSCOMP_1:def 35; then (g/.n)`1 = W-bound L~f & (g/.n)`2 = N-bound L~f by EUCLID:56; hence W-bound L~f <= (g/.n)`1 & (g/.n)`1 <= E-bound L~f & S-bound L~f <= (g/.n)`2 & (g/.n)`2 <= N-bound L~f by SPRECT_1:23,24; end; theorem Th31: for f being non trivial FinSequence of TOP-REAL 2 holds <*SE-corner L~f*> is_in_the_area_of f proof let f be non trivial FinSequence of TOP-REAL 2; set g = <*SE-corner L~f*>; let n; A1: dom g = {1} by FINSEQ_1:4,55; assume n in dom g; then n = 1 by A1,TARSKI:def 1; then g/.n = SE-corner L~f by FINSEQ_4:25 .= |[E-bound L~f, S-bound L~f]| by PSCOMP_1:def 37; then (g/.n)`1 = E-bound L~f & (g/.n)`2 = S-bound L~f by EUCLID:56; hence W-bound L~f <= (g/.n)`1 & (g/.n)`1 <= E-bound L~f & S-bound L~f <= (g/.n)`2 & (g/.n)`2 <= N-bound L~f by SPRECT_1:23,24; end; theorem Th32: for f being non trivial FinSequence of TOP-REAL 2 holds <*SW-corner L~f*> is_in_the_area_of f proof let f be non trivial FinSequence of TOP-REAL 2; set g = <*SW-corner L~f*>; let n; A1: dom g = {1} by FINSEQ_1:4,55; assume n in dom g; then n = 1 by A1,TARSKI:def 1; then g/.n = SW-corner L~f by FINSEQ_4:25 .= |[W-bound L~f, S-bound L~f]| by PSCOMP_1:def 34; then (g/.n)`1 = W-bound L~f & (g/.n)`2 = S-bound L~f by EUCLID:56; hence W-bound L~f <= (g/.n)`1 & (g/.n)`1 <= E-bound L~f & S-bound L~f <= (g/.n)`2 & (g/.n)`2 <= N-bound L~f by SPRECT_1:23,24; end; begin :: Horizontal and vertical connections definition let f, g be FinSequence of TOP-REAL 2; pred g is_a_h.c._for f means :Def2: g is_in_the_area_of f & (g/.1)`1 = W-bound L~f & (g/.len g)`1 = E-bound L~f; pred g is_a_v.c._for f means :Def3: g is_in_the_area_of f & (g/.1)`2 = S-bound L~f & (g/.len g)`2 = N-bound L~f; end; theorem Th33: for f being FinSequence of TOP-REAL 2, g,h being one-to-one special FinSequence of TOP-REAL 2 st 2 <= len g & 2 <= len h & g is_a_h.c._for f & h is_a_v.c._for f holds L~g meets L~h proof let f be FinSequence of TOP-REAL 2, g,h being one-to-one special FinSequence of TOP-REAL 2 such that A1: 2 <= len g & 2 <= len h and A2: for n st n in dom g holds W-bound L~f <= (g/.n)`1 & (g/.n)`1 <= E-bound L~f & S-bound L~f <= (g/.n)`2 & (g/.n)`2 <= N-bound L~f and A3: (g/.1)`1 = W-bound L~f and A4: (g/.len g)`1 = E-bound L~f and A5: for n st n in dom h holds W-bound L~f <= (h/.n)`1 & (h/.n)`1 <= E-bound L~f & S-bound L~f <= (h/.n)`2 & (h/.n)`2 <= N-bound L~f and A6: (h/.1)`2 = S-bound L~f and A7: (h/.len h)`2 = N-bound L~f; len g <> 0 & len h <> 0 by A1; then reconsider g,h as non empty one-to-one special FinSequence of TOP-REAL 2 by FINSEQ_1:25; A8: X_axis(g) lies_between (X_axis(g)).1, (X_axis(g)).(len g) proof set F = X_axis(g), r = (X_axis(g)).1, s = (X_axis(g)).(len g); let n; assume A9: n in dom F; then A10: n in dom g by Th19; A11: F.n = (g/.n)`1 by A9,GOBOARD1:def 3; 1 in dom F by FINSEQ_5:6; then r = W-bound L~f by A3,GOBOARD1:def 3; hence r <= F.n by A2,A10,A11; A12: len F = len g by GOBOARD1:def 3; len F in dom F by FINSEQ_5:6; then s = E-bound L~f by A4,A12,GOBOARD1:def 3; hence F.n <= s by A2,A10,A11; end; A13: X_axis(h) lies_between (X_axis(g)).1, (X_axis(g)).(len g) proof set F = X_axis(g), r = (X_axis(g)).1, s = (X_axis(g)).(len g), H = X_axis h; let n; assume A14: n in dom H; then A15: n in dom h by Th19; A16: H.n = (h/.n)`1 by A14,GOBOARD1:def 3; 1 in dom F by FINSEQ_5:6; then r = W-bound L~f by A3,GOBOARD1:def 3; hence r <= H.n by A5,A15,A16; A17: len F = len g by GOBOARD1:def 3; len F in dom F by FINSEQ_5:6; then s = E-bound L~f by A4,A17,GOBOARD1:def 3; hence H.n <= s by A5,A15,A16; end; A18: Y_axis(g) lies_between (Y_axis(h)).1, (Y_axis(h)).(len h) proof set F = Y_axis(h), r = (Y_axis(h)).1, s = (Y_axis(h)).(len h), G = Y_axis g; let n; assume A19: n in dom G; then A20: n in dom g by Th20; A21: G.n = (g/.n)`2 by A19,GOBOARD1:def 4; 1 in dom F by FINSEQ_5:6; then r = S-bound L~f by A6,GOBOARD1:def 4; hence r <= G.n by A2,A20,A21; A22: len F = len h by GOBOARD1:def 4; len F in dom F by FINSEQ_5:6; then s = N-bound L~f by A7,A22,GOBOARD1:def 4; hence G.n <= s by A2,A20,A21; end; Y_axis(h) lies_between (Y_axis(h)).1, (Y_axis(h)).(len h) proof set F = Y_axis h, r = (Y_axis h).1, s = (Y_axis h).(len h); let n; assume A23: n in dom F; then A24: n in dom h by Th20; A25: F.n = (h/.n)`2 by A23,GOBOARD1:def 4; 1 in dom F by FINSEQ_5:6; then r = S-bound L~f by A6,GOBOARD1:def 4; hence r <= F.n by A5,A24,A25; A26: len F = len h by GOBOARD1:def 4; len F in dom F by FINSEQ_5:6; then s = N-bound L~f by A7,A26,GOBOARD1:def 4; hence F.n <= s by A5,A24,A25; end; hence thesis by A1,A8,A13,A18,GOBOARD4:5; end; begin :: Orientation definition let f be FinSequence of TOP-REAL 2; attr f is clockwise_oriented means :Def4: (Rotate(f,N-min L~f))/.2 in N-most L~f; end; theorem Th34: for f being non constant standard special_circular_sequence st f/.1 = N-min L~f holds f is clockwise_oriented iff f/.2 in N-most L~f proof let f be non constant standard special_circular_sequence; assume f/.1 = N-min L~f; then Rotate(f,N-min L~f) = f by FINSEQ_6:95; hence f is clockwise_oriented iff f/.2 in N-most L~f by Def4; end; definition cluster R^2-unit_square -> compact; coherence by TOPREAL2:2; end; theorem Th35: N-bound R^2-unit_square = 1 proof set X = R^2-unit_square; reconsider Z = (proj2||X).:the carrier of ((TOP-REAL 2)|X) as Subset of REAL; A1: X = [#]((TOP-REAL 2)|X) by PRE_TOPC:def 10 .= the carrier of ((TOP-REAL 2)|X) by PRE_TOPC:12; A2:for p be real number st p in Z holds p <= 1 proof let p be real number; assume p in Z; then consider p0 being set such that A3: p0 in the carrier of (TOP-REAL 2)|X and p0 in the carrier of (TOP-REAL 2)|X and A4: p = (proj2||X).p0 by FUNCT_2:115; reconsider p0 as Point of TOP-REAL 2 by A1,A3; ex q being Point of TOP-REAL 2 st p0 = q & (q`1 = 0 & q`2 <= 1 & q`2 >= 0 or q`1 <= 1 & q`1 >= 0 & q`2 = 1 or q`1 <= 1 & q`1 >= 0 & q`2 = 0 or q`1 = 1 & q`2 <= 1 & q`2 >= 0) by A1,A3,TOPREAL1:def 3; hence p <= 1 by A1,A3,A4,PSCOMP_1:70; end; A5: for q being real number st for p being real number st p in Z holds p <= q holds 1 <= q proof let q be real number such that A6: for p being real number st p in Z holds p <= q; |[1,1]| in LSeg(|[ 1,0 ]|, |[ 1,1 ]|) by TOPREAL1:6; then |[1,1]| in LSeg(|[ 0,0 ]|, |[ 1,0 ]|) \/ LSeg(|[ 1,0 ]|, |[ 1,1 ]|) by XBOOLE_0:def 2; then A7: |[1,1]| in X by TOPREAL1:20,XBOOLE_0:def 2; then (proj2||X). |[1,1]| = |[1,1]|`2 by PSCOMP_1:70 .= 1 by EUCLID:56; then 1 in Z by A1,A7,FUNCT_2:43; hence thesis by A6; end; thus N-bound X = sup (proj2||X) by PSCOMP_1:def 31 .= sup Z by PSCOMP_1:def 21 .= 1 by A2,A5,PSCOMP_1:11; end; theorem Th36: W-bound R^2-unit_square = 0 proof set X = R^2-unit_square; reconsider Z = (proj1||X).:the carrier of ((TOP-REAL 2)|X) as Subset of REAL; A1: X = [#]((TOP-REAL 2)|X) by PRE_TOPC:def 10 .= the carrier of ((TOP-REAL 2)|X) by PRE_TOPC:12; A2: for p be real number st p in Z holds p >= 0 proof let p be real number; assume p in Z; then consider p0 being set such that A3: p0 in the carrier of (TOP-REAL 2)|X and p0 in the carrier of (TOP-REAL 2)|X and A4: p = (proj1||X).p0 by FUNCT_2:115; reconsider p0 as Point of TOP-REAL 2 by A1,A3; ex q being Point of TOP-REAL 2 st p0 = q & (q`1 = 0 & q`2 <= 1 & q`2 >= 0 or q`1 <= 1 & q`1 >= 0 & q`2 = 1 or q`1 <= 1 & q`1 >= 0 & q`2 = 0 or q`1 = 1 & q`2 <= 1 & q`2 >= 0) by A1,A3,TOPREAL1:def 3; hence p >= 0 by A1,A3,A4,PSCOMP_1:69; end; A5: for q be real number st for p be real number st p in Z holds p >= q holds 0 >= q proof let q be real number such that A6: for p be real number st p in Z holds p >= q; |[0,0]| in LSeg(|[ 0,0 ]|, |[ 1,0 ]|) by TOPREAL1:6; then |[0,0]| in LSeg(|[ 0,0 ]|, |[ 1,0 ]|) \/ LSeg(|[ 1,0 ]|, |[ 1,1 ]|) by XBOOLE_0:def 2; then A7: |[0,0]| in X by TOPREAL1:20,XBOOLE_0:def 2; then (proj1||X). |[0,0]| = |[0,0]|`1 by PSCOMP_1:69 .= 0 by EUCLID:56; then 0 in Z by A1,A7,FUNCT_2:43; hence thesis by A6; end; thus W-bound X = inf (proj1||X) by PSCOMP_1:def 30 .= inf Z by PSCOMP_1:def 20 .= 0 by A2,A5,PSCOMP_1:9; end; theorem Th37: E-bound R^2-unit_square = 1 proof set X = R^2-unit_square; reconsider Z = (proj1||X).:the carrier of ((TOP-REAL 2)|X) as Subset of REAL; A1: X = [#]((TOP-REAL 2)|X) by PRE_TOPC:def 10 .= the carrier of ((TOP-REAL 2)|X) by PRE_TOPC:12; A2:for p be real number st p in Z holds p <= 1 proof let p be real number; assume p in Z; then consider p0 being set such that A3: p0 in the carrier of (TOP-REAL 2)|X and p0 in the carrier of (TOP-REAL 2)|X and A4: p = (proj1||X).p0 by FUNCT_2:115; reconsider p0 as Point of TOP-REAL 2 by A1,A3; ex q being Point of TOP-REAL 2 st p0 = q & (q`1 = 0 & q`2 <= 1 & q`2 >= 0 or q`1 <= 1 & q`1 >= 0 & q`2 = 1 or q`1 <= 1 & q`1 >= 0 & q`2 = 0 or q`1 = 1 & q`2 <= 1 & q`2 >= 0) by A1,A3,TOPREAL1:def 3; hence p <= 1 by A1,A3,A4,PSCOMP_1:69; end; A5: for q being real number st for p being real number st p in Z holds p <= q holds 1 <= q proof let q be real number such that A6: for p be real number st p in Z holds p <= q; |[1,1]| in LSeg(|[ 1,0 ]|, |[ 1,1 ]|) by TOPREAL1:6; then |[1,1]| in LSeg(|[ 0,0 ]|, |[ 1,0 ]|) \/ LSeg(|[ 1,0 ]|, |[ 1,1 ]|) by XBOOLE_0:def 2; then A7: |[1,1]| in X by TOPREAL1:20,XBOOLE_0:def 2; then (proj1||X). |[1,1]| = |[1,1]|`1 by PSCOMP_1:69 .= 1 by EUCLID:56; then 1 in Z by A1,A7,FUNCT_2:43; hence thesis by A6; end; thus E-bound X = sup (proj1||X) by PSCOMP_1:def 32 .= sup Z by PSCOMP_1:def 21 .= 1 by A2,A5,PSCOMP_1:11; end; theorem S-bound R^2-unit_square = 0 proof set X = R^2-unit_square; reconsider Z = (proj2||X).:the carrier of ((TOP-REAL 2)|X) as Subset of REAL; A1: X = [#]((TOP-REAL 2)|X) by PRE_TOPC:def 10 .= the carrier of ((TOP-REAL 2)|X) by PRE_TOPC:12; A2:for p be real number st p in Z holds p >= 0 proof let p be real number; assume p in Z; then consider p0 being set such that A3: p0 in the carrier of (TOP-REAL 2)|X and p0 in the carrier of (TOP-REAL 2)|X and A4: p = (proj2||X).p0 by FUNCT_2:115; reconsider p0 as Point of TOP-REAL 2 by A1,A3; ex q being Point of TOP-REAL 2 st p0 = q & (q`1 = 0 & q`2 <= 1 & q`2 >= 0 or q`1 <= 1 & q`1 >= 0 & q`2 = 1 or q`1 <= 1 & q`1 >= 0 & q`2 = 0 or q`1 = 1 & q`2 <= 1 & q`2 >= 0) by A1,A3,TOPREAL1:def 3; hence p >= 0 by A1,A3,A4,PSCOMP_1:70; end; A5: for q be real number st for p be real number st p in Z holds p >= q holds 0 >= q proof let q be real number such that A6: for p be real number st p in Z holds p >= q; |[1,0]| in LSeg(|[ 1,0 ]|, |[ 1,1 ]|) by TOPREAL1:6; then |[1,0]| in LSeg(|[ 0,0 ]|, |[ 1,0 ]|) \/ LSeg(|[ 1,0 ]|, |[ 1,1 ]|) by XBOOLE_0:def 2; then A7: |[1,0]| in X by TOPREAL1:20,XBOOLE_0:def 2; then (proj2||X). |[1,0]| = |[1,0]|`2 by PSCOMP_1:70 .= 0 by EUCLID:56; then 0 in Z by A1,A7,FUNCT_2:43; hence thesis by A6; end; thus S-bound X = inf (proj2||X) by PSCOMP_1:def 33 .= inf Z by PSCOMP_1:def 20 .= 0 by A2,A5,PSCOMP_1:9; end; Lm1: NW-corner R^2-unit_square = |[0,1]| by Th35,Th36,PSCOMP_1:def 35; Lm2: NE-corner R^2-unit_square = |[1,1]| by Th35,Th37,PSCOMP_1:def 36; theorem Th39: N-most R^2-unit_square = LSeg(|[0,1]|,|[1,1]|) proof set X = R^2-unit_square; A1: LSeg(|[ 0,0 ]|, |[ 0,1 ]|) \/ LSeg(|[ 0,1 ]|, |[ 1,1 ]|) c= X by TOPREAL1:20,XBOOLE_1:7; LSeg(|[0,1]|,|[1,1]|) c= LSeg(|[ 0,0 ]|, |[ 0,1 ]|) \/ LSeg(|[ 0,1 ]|, |[ 1,1 ]|) by XBOOLE_1:7; then A2: LSeg(|[0,1]|,|[1,1]|) c= X by A1,XBOOLE_1:1; thus N-most X = LSeg(NW-corner X, NE-corner X)/\X by PSCOMP_1:def 39 .= LSeg(|[0,1]|,|[1,1]|) by A2,Lm1,Lm2,XBOOLE_1:28; end; theorem N-min R^2-unit_square = |[0,1]| proof inf (proj1||LSeg(|[0,1]|,|[1,1]|)) = 0 proof set X = LSeg(|[0,1]|,|[1,1]|); reconsider Z = (proj1||X).:the carrier of ((TOP-REAL 2)|X) as Subset of REAL; A1: X = [#]((TOP-REAL 2)|X) by PRE_TOPC:def 10 .= the carrier of ((TOP-REAL 2)|X) by PRE_TOPC:12; A2: for p be real number st p in Z holds p >= 0 proof let p be real number; assume p in Z; then consider p0 being set such that A3: p0 in the carrier of (TOP-REAL 2)|X and p0 in the carrier of (TOP-REAL 2)|X and A4: p = (proj1||X).p0 by FUNCT_2:115; reconsider p0 as Point of TOP-REAL 2 by A1,A3; |[0,1]|`1 = 0 & |[1,1]|`1 = 1 by EUCLID:56; then p0`1 >= 0 by A1,A3,TOPREAL1:9; hence p >= 0 by A1,A3,A4,PSCOMP_1:69; end; A5: for q be real number st for p be real number st p in Z holds p >= q holds 0 >= q proof let q be real number such that A6: for p be real number st p in Z holds p >= q; A7: |[0,1]| in X by TOPREAL1:6; then (proj1||X). |[0,1]| = |[0,1]|`1 by PSCOMP_1:69 .= 0 by EUCLID:56; then 0 in Z by A1,A7,FUNCT_2:43; hence thesis by A6; end; thus inf (proj1||X) = inf Z by PSCOMP_1:def 20 .= 0 by A2,A5,PSCOMP_1:9; end; hence N-min R^2-unit_square = |[0,1]| by Th35,Th39,PSCOMP_1:def 44; end; definition let X be non vertical non horizontal non empty compact Subset of TOP-REAL 2; cluster SpStSeq X -> clockwise_oriented; coherence proof set f = SpStSeq X; A1: f/.1 = N-min L~f by SPRECT_1:91; f/.2 = N-max L~f by SPRECT_1:92; then f/.2 in N-most L~f by PSCOMP_1:101; hence thesis by A1,Th34; end; end; definition cluster clockwise_oriented (non constant standard special_circular_sequence); existence proof consider X being non vertical non horizontal non empty compact Subset of TOP-REAL 2; take SpStSeq X; thus thesis; end; end; theorem Th41: for f being non constant standard special_circular_sequence, i,j st i > j & (1 < j & i <= len f or 1 <= j & i < len f) holds mid(f,i,j) is S-Sequence_in_R2 proof let f be non constant standard special_circular_sequence, i,j such that A1: i > j and A2: 1 < j & i <= len f or 1 <= j & i < len f; A3: Rev mid(f,j,i) = mid(f,i,j) by JORDAN4:30; per cases by A2; suppose 1 < j & i <= len f; then mid(f,j,i) is S-Sequence_in_R2 by A1,JORDAN4:52; hence mid(f,i,j) is S-Sequence_in_R2 by A3,SPPOL_2:47; suppose A4: 1 <= j & i < len f; then i+1 <= len f by NAT_1:38; then mid(f,j,i) is S-Sequence_in_R2 by A1,A4,JORDAN4:51; hence mid(f,i,j) is S-Sequence_in_R2 by A3,SPPOL_2:47; end; theorem Th42: for f being non constant standard special_circular_sequence, i,j st i < j & (1 < i & j <= len f or 1 <= i & j < len f) holds mid(f,i,j) is S-Sequence_in_R2 proof let f be non constant standard special_circular_sequence,i,j such that A1: i < j and A2:1 < i & j <= len f or 1 <= i & j < len f; A3: Rev Rev mid(f,i,j) = mid(f,i,j) by FINSEQ_6:29; mid(f,j,i) is S-Sequence_in_R2 by A1,A2,Th41; then Rev mid(f,i,j) is S-Sequence_in_R2 by JORDAN4:30; hence mid(f,i,j) is S-Sequence_in_R2 by A3,SPPOL_2:47; end; reserve f for non trivial FinSequence of TOP-REAL 2; theorem Th43: N-min L~f in rng f proof set p = N-min L~f; A1: len f >= 2 by SPPOL_1:2; p in L~f by SPRECT_1:13; then consider i be Nat such that A2: 1 <= i & i+1 <= len f and A3: p in LSeg(f/.i,f/.(i+1)) by SPPOL_2:14; i <= i+1 by NAT_1:29; then i+1 >= 1 & i <= len f by A2,AXIOMS:22; then A4: i in dom f & i+1 in dom f by A2,FINSEQ_3:27; then A5: f/.i in L~f & f/.(i+1) in L~f by A1,GOBOARD1:16; then A6: (f/.i)`2 <= N-bound L~f & (f/.(i+1))`2 <= N-bound L~f by PSCOMP_1:71; A7: p`2 = N-bound L~f by PSCOMP_1:94; now per cases by A3,A6,A7,Th22; suppose p = f/.i; hence thesis by A4,PARTFUN2:4; suppose p = f/.(i+1); hence thesis by A4,PARTFUN2:4; suppose A8: p`2 = (f/.i)`2 & p`2 = (f/.(i+1))`2; then f/.i in N-most L~f & f/.(i+1) in N-most L~f by A5,A7,Th14; then A9: (f/.i)`1 >= p`1 & (f/.(i+1))`1 >= p`1 by PSCOMP_1:98; (f/.i)`1 <= (f/.(i+1))`1 or (f/.(i+1))`1 <= (f/.i)`1; then (f/.i)`1 <= p`1 or (f/.(i+1))`1 <= p`1 by A3,TOPREAL1:9; then p`1 = (f/.i)`1 or p`1 = (f/.(i+1))`1 by A9,AXIOMS:21; then p = (f/.i) or p = (f/.(i+1)) by A8,TOPREAL3:11; hence thesis by A4,PARTFUN2:4; end; hence thesis; end; theorem Th44: N-max L~f in rng f proof set p = N-max L~f; A1: len f >= 2 by SPPOL_1:2; p in L~f by SPRECT_1:13; then consider i be Nat such that A2: 1 <= i & i+1 <= len f and A3: p in LSeg(f/.i,f/.(i+1)) by SPPOL_2:14; i <= i+1 by NAT_1:29; then i+1 >= 1 & i <= len f by A2,AXIOMS:22; then A4: i in dom f & i+1 in dom f by A2,FINSEQ_3:27; then A5: f/.i in L~f & f/.(i+1) in L~f by A1,GOBOARD1:16; then A6: (f/.i)`2 <= N-bound L~f & (f/.(i+1))`2 <= N-bound L~f by PSCOMP_1:71; A7: p`2 = N-bound L~f by PSCOMP_1:94; now per cases by A3,A6,A7,Th22; suppose p = f/.i; hence thesis by A4,PARTFUN2:4; suppose p = f/.(i+1); hence thesis by A4,PARTFUN2:4; suppose A8: p`2 = (f/.i)`2 & p`2 = (f/.(i+1))`2; then f/.i in N-most L~f & f/.(i+1) in N-most L~f by A5,A7,Th14; then A9: (f/.i)`1 <= p`1 & (f/.(i+1))`1 <= p`1 by PSCOMP_1:98; (f/.i)`1 >= (f/.(i+1))`1 or (f/.(i+1))`1 >= (f/.i)`1; then (f/.i)`1 >= p`1 or (f/.(i+1))`1 >= p`1 by A3,TOPREAL1:9; then p`1 = (f/.i)`1 or p`1 = (f/.(i+1))`1 by A9,AXIOMS:21; then p = (f/.i) or p = (f/.(i+1)) by A8,TOPREAL3:11; hence thesis by A4,PARTFUN2:4; end; hence thesis; end; theorem Th45: S-min L~f in rng f proof set p = S-min L~f; A1: len f >= 2 by SPPOL_1:2; p in L~f by SPRECT_1:14; then consider i be Nat such that A2: 1 <= i & i+1 <= len f and A3: p in LSeg(f/.i,f/.(i+1)) by SPPOL_2:14; i <= i+1 by NAT_1:29; then i+1 >= 1 & i <= len f by A2,AXIOMS:22; then A4: i in dom f & i+1 in dom f by A2,FINSEQ_3:27; then A5: f/.i in L~f & f/.(i+1) in L~f by A1,GOBOARD1:16; then A6: (f/.i)`2 >= S-bound L~f & (f/.(i+1))`2 >= S-bound L~f by PSCOMP_1:71; A7: p`2 = S-bound L~f by PSCOMP_1:114; now per cases by A3,A6,A7,Th24; suppose p = f/.i; hence thesis by A4,PARTFUN2:4; suppose p = f/.(i+1); hence thesis by A4,PARTFUN2:4; suppose A8: p`2 = (f/.i)`2 & p`2 = (f/.(i+1))`2; then f/.i in S-most L~f & f/.(i+1) in S-most L~f by A5,A7,Th15; then A9: (f/.i)`1 >= p`1 & (f/.(i+1))`1 >= p`1 by PSCOMP_1:118; (f/.i)`1 <= (f/.(i+1))`1 or (f/.(i+1))`1 <= (f/.i)`1; then (f/.i)`1 <= p`1 or (f/.(i+1))`1 <= p`1 by A3,TOPREAL1:9; then p`1 = (f/.i)`1 or p`1 = (f/.(i+1))`1 by A9,AXIOMS:21; then p = (f/.i) or p = (f/.(i+1)) by A8,TOPREAL3:11; hence thesis by A4,PARTFUN2:4; end; hence thesis; end; theorem Th46: S-max L~f in rng f proof set p = S-max L~f; A1: len f >= 2 by SPPOL_1:2; p in L~f by SPRECT_1:14; then consider i be Nat such that A2: 1 <= i & i+1 <= len f and A3: p in LSeg(f/.i,f/.(i+1)) by SPPOL_2:14; i <= i+1 by NAT_1:29; then i+1 >= 1 & i <= len f by A2,AXIOMS:22; then A4: i in dom f & i+1 in dom f by A2,FINSEQ_3:27; then A5: f/.i in L~f & f/.(i+1) in L~f by A1,GOBOARD1:16; then A6: (f/.i)`2 >= S-bound L~f & (f/.(i+1))`2 >= S-bound L~f by PSCOMP_1:71; A7: p`2 = S-bound L~f by PSCOMP_1:114; now per cases by A3,A6,A7,Th24; suppose p = f/.i; hence thesis by A4,PARTFUN2:4; suppose p = f/.(i+1); hence thesis by A4,PARTFUN2:4; suppose A8: p`2 = (f/.i)`2 & p`2 = (f/.(i+1))`2; then f/.i in S-most L~f & f/.(i+1) in S-most L~f by A5,A7,Th15; then A9: (f/.i)`1 <= p`1 & (f/.(i+1))`1 <= p`1 by PSCOMP_1:118; (f/.i)`1 >= (f/.(i+1))`1 or (f/.(i+1))`1 >= (f/.i)`1; then (f/.i)`1 >= p`1 or (f/.(i+1))`1 >= p`1 by A3,TOPREAL1:9; then p`1 = (f/.i)`1 or p`1 = (f/.(i+1))`1 by A9,AXIOMS:21; then p = (f/.i) or p = (f/.(i+1)) by A8,TOPREAL3:11; hence thesis by A4,PARTFUN2:4; end; hence thesis; end; theorem Th47: W-min L~f in rng f proof set p = W-min L~f; A1: len f >= 2 by SPPOL_1:2; p in L~f by SPRECT_1:15; then consider i be Nat such that A2: 1 <= i & i+1 <= len f and A3: p in LSeg(f/.i,f/.(i+1)) by SPPOL_2:14; i <= i+1 by NAT_1:29; then i+1 >= 1 & i <= len f by A2,AXIOMS:22; then A4: i in dom f & i+1 in dom f by A2,FINSEQ_3:27; then A5: f/.i in L~f & f/.(i+1) in L~f by A1,GOBOARD1:16; then A6: (f/.i)`1 >= W-bound L~f & (f/.(i+1))`1 >= W-bound L~f by PSCOMP_1:71; A7: p`1 = W-bound L~f by PSCOMP_1:84; now per cases by A3,A6,A7,Th23; suppose p = f/.i; hence thesis by A4,PARTFUN2:4; suppose p = f/.(i+1); hence thesis by A4,PARTFUN2:4; suppose A8: p`1 = (f/.i)`1 & p`1 = (f/.(i+1))`1; then f/.i in W-most L~f & f/.(i+1) in W-most L~f by A5,A7,Th16; then A9: (f/.i)`2 >= p`2 & (f/.(i+1))`2 >= p`2 by PSCOMP_1:88; (f/.i)`2 <= (f/.(i+1))`2 or (f/.(i+1))`2 <= (f/.i)`2; then (f/.i)`2 <= p`2 or (f/.(i+1))`2 <= p`2 by A3,TOPREAL1:10; then p`2 = (f/.i)`2 or p`2 = (f/.(i+1))`2 by A9,AXIOMS:21; then p = (f/.i) or p = (f/.(i+1)) by A8,TOPREAL3:11; hence thesis by A4,PARTFUN2:4; end; hence thesis; end; theorem Th48: W-max L~f in rng f proof set p = W-max L~f; A1: len f >= 2 by SPPOL_1:2; p in L~f by SPRECT_1:15; then consider i be Nat such that A2: 1 <= i & i+1 <= len f and A3: p in LSeg(f/.i,f/.(i+1)) by SPPOL_2:14; i <= i+1 by NAT_1:29; then i+1 >= 1 & i <= len f by A2,AXIOMS:22; then A4: i in dom f & i+1 in dom f by A2,FINSEQ_3:27; then A5: f/.i in L~f & f/.(i+1) in L~f by A1,GOBOARD1:16; then A6: (f/.i)`1 >= W-bound L~f & (f/.(i+1))`1 >= W-bound L~f by PSCOMP_1:71; A7: p`1 = W-bound L~f by PSCOMP_1:84; now per cases by A3,A6,A7,Th23; suppose p = f/.i; hence thesis by A4,PARTFUN2:4; suppose p = f/.(i+1); hence thesis by A4,PARTFUN2:4; suppose A8: p`1 = (f/.i)`1 & p`1 = (f/.(i+1))`1; then f/.i in W-most L~f & f/.(i+1) in W-most L~f by A5,A7,Th16; then A9: (f/.i)`2 <= p`2 & (f/.(i+1))`2 <= p`2 by PSCOMP_1:88; (f/.i)`2 >= (f/.(i+1))`2 or (f/.(i+1))`2 >= (f/.i)`2; then (f/.i)`2 >= p`2 or (f/.(i+1))`2 >= p`2 by A3,TOPREAL1:10; then p`2 = (f/.i)`2 or p`2 = (f/.(i+1))`2 by A9,AXIOMS:21; then p = (f/.i) or p = (f/.(i+1)) by A8,TOPREAL3:11; hence thesis by A4,PARTFUN2:4; end; hence thesis; end; theorem Th49: E-min L~f in rng f proof set p = E-min L~f; A1: len f >= 2 by SPPOL_1:2; p in L~f by SPRECT_1:16; then consider i be Nat such that A2: 1 <= i & i+1 <= len f and A3: p in LSeg(f/.i,f/.(i+1)) by SPPOL_2:14; i <= i+1 by NAT_1:29; then i+1 >= 1 & i <= len f by A2,AXIOMS:22; then A4: i in dom f & i+1 in dom f by A2,FINSEQ_3:27; then A5: f/.i in L~f & f/.(i+1) in L~f by A1,GOBOARD1:16; then A6: (f/.i)`1 <= E-bound L~f & (f/.(i+1))`1 <= E-bound L~f by PSCOMP_1:71; A7: p`1 = E-bound L~f by PSCOMP_1:104; now per cases by A3,A6,A7,Th21; suppose p = f/.i; hence thesis by A4,PARTFUN2:4; suppose p = f/.(i+1); hence thesis by A4,PARTFUN2:4; suppose A8: p`1 = (f/.i)`1 & p`1 = (f/.(i+1))`1; then f/.i in E-most L~f & f/.(i+1) in E-most L~f by A5,A7,Th17; then A9: (f/.i)`2 >= p`2 & (f/.(i+1))`2 >= p`2 by PSCOMP_1:108; (f/.i)`2 <= (f/.(i+1))`2 or (f/.(i+1))`2 <= (f/.i)`2; then (f/.i)`2 <= p`2 or (f/.(i+1))`2 <= p`2 by A3,TOPREAL1:10; then p`2 = (f/.i)`2 or p`2 = (f/.(i+1))`2 by A9,AXIOMS:21; then p = (f/.i) or p = (f/.(i+1)) by A8,TOPREAL3:11; hence thesis by A4,PARTFUN2:4; end; hence thesis; end; theorem Th50: E-max L~f in rng f proof set p = E-max L~f; A1: len f >= 2 by SPPOL_1:2; p in L~f by SPRECT_1:16; then consider i be Nat such that A2: 1 <= i & i+1 <= len f and A3: p in LSeg(f/.i,f/.(i+1)) by SPPOL_2:14; i <= i+1 by NAT_1:29; then i+1 >= 1 & i <= len f by A2,AXIOMS:22; then A4: i in dom f & i+1 in dom f by A2,FINSEQ_3:27; then A5: f/.i in L~f & f/.(i+1) in L~f by A1,GOBOARD1:16; then A6: (f/.i)`1 <= E-bound L~f & (f/.(i+1))`1 <= E-bound L~f by PSCOMP_1:71; A7: p`1 = E-bound L~f by PSCOMP_1:104; now per cases by A3,A6,A7,Th21; suppose p = f/.i; hence thesis by A4,PARTFUN2:4; suppose p = f/.(i+1); hence thesis by A4,PARTFUN2:4; suppose A8: p`1 = (f/.i)`1 & p`1 = (f/.(i+1))`1; then f/.i in E-most L~f & f/.(i+1) in E-most L~f by A5,A7,Th17; then A9: (f/.i)`2 <= p`2 & (f/.(i+1))`2 <= p`2 by PSCOMP_1:108; (f/.i)`2 >= (f/.(i+1))`2 or (f/.(i+1))`2 >= (f/.i)`2; then (f/.i)`2 >= p`2 or (f/.(i+1))`2 >= p`2 by A3,TOPREAL1:10; then p`2 = (f/.i)`2 or p`2 = (f/.(i+1))`2 by A9,AXIOMS:21; then p = (f/.i) or p = (f/.(i+1)) by A8,TOPREAL3:11; hence thesis by A4,PARTFUN2:4; end; hence thesis; end; reserve f for non constant standard special_circular_sequence; theorem Th51: 1 <= i & i <= j & j < m & m <= n & n <= len f & (1 < i or n < len f) implies L~mid(f,i,j) misses L~mid(f,m,n) proof assume that A1: 1 <= i and A2: i <= j and A3: j < m and A4: m <= n and A5: n <= len f and A6: 1 < i or n < len f; set A = { LSeg(f,k): i <= k & k < j}, B = { LSeg(f,l): m <= l & l < n}; m <= len f by A4,A5,AXIOMS:22; then j < len f by A3,AXIOMS:22; then A7: L~mid(f,i,j) = union A by A1,A2,Th18; 1 <= j by A1,A2,AXIOMS:22; then 1 < m by A3,AXIOMS:22; then A8: L~mid(f,m,n) = union B by A4,A5,Th18; for x,y being set st x in A & y in B holds x misses y proof let x,y be set; assume x in A; then consider k such that A9: x = LSeg(f,k) and A10: i <= k and A11: k < j; assume y in B; then consider l such that A12: y = LSeg(f,l) and A13: m <= l and A14: l < n; k+1 <= j by A11,NAT_1:38; then k+1 < m by A3,AXIOMS:22; then A15: k+1 < l by A13,AXIOMS:22; A16: l < len f by A5,A14,AXIOMS:22; l+1 <= n by A14,NAT_1:38; then k > 1 or l+1 < len f by A6,A10,AXIOMS:22; hence x misses y by A9,A12,A15,A16,GOBOARD5:def 4; end; hence L~mid(f,i,j) misses L~mid(f,m,n) by A7,A8,Th4; end; theorem Th52: 1 <= i & i <= j & j < m & m <= n & n <= len f & (1 < i or n < len f) implies L~mid(f,i,j) misses L~mid(f,n,m) proof mid(f,n,m) = Rev mid(f,m,n) by JORDAN4:30; then L~mid(f,n,m) = L~mid(f,m,n) by SPPOL_2:22; hence thesis by Th51; end; theorem Th53: 1 <= i & i <= j & j < m & m <= n & n <= len f & (1 < i or n < len f) implies L~mid(f,j,i) misses L~mid(f,n,m) proof mid(f,i,j) = Rev mid(f,j,i) by JORDAN4:30; then L~mid(f,i,j) = L~mid(f,j,i) by SPPOL_2:22; hence thesis by Th52; end; theorem Th54: 1 <= i & i <= j & j < m & m <= n & n <= len f & (1 < i or n < len f) implies L~mid(f,j,i) misses L~mid(f,m,n) proof mid(f,i,j) = Rev mid(f,j,i) by JORDAN4:30; then L~mid(f,i,j) = L~mid(f,j,i) by SPPOL_2:22; hence thesis by Th51; end; theorem Th55: (N-min L~f)`1 < (N-max L~f)`1 proof set p = N-min L~f, i = p..f; A1: len f > 3+1 by GOBOARD7:36; then A2: len f >= 1+1 by AXIOMS:22; A3: p in rng f by Th43; then A4: i in dom f by FINSEQ_4:30; A5: p = f.i by A3,FINSEQ_4:29 .= f/.i by A4,FINSEQ_4:def 4; A6: 1 <= i & i <= len f by A4,FINSEQ_3:27; A7: p`2 = N-bound L~f by PSCOMP_1:94; per cases by A6,REAL_1:def 5; suppose A8: i = 1 or i = len f; A9: 1 in dom f by FINSEQ_5:6; A10: len f in dom f by FINSEQ_5:6; A11: f/.1 = f/.len f by FINSEQ_6:def 1; A12: p = f/.1 by A5,A8,FINSEQ_6:def 1; len f >= 1 by A1,AXIOMS:22; then A13: len f -' 1+1 = len f by AMI_5:4; then len f -' 1 > 3 by A1,AXIOMS:24; then A14: len f -' 1 > 1 by AXIOMS:22; len f -' 1 <= len f by A13,NAT_1:29; then A15: len f -' 1 in dom f by A14,FINSEQ_3:27; A16: p in LSeg(f,len f -' 1) by A5,A8,A11,A13,A14,TOPREAL1:27; A17: p in LSeg(f,1) by A2,A12,TOPREAL1:27; A18: p <> f/.(len f -' 1) by A5,A8,A10,A11,A13,A15,GOBOARD7:31; A19: 1+1 in dom f by A2,FINSEQ_3:27; then A20: p <> f/.(1+1) by A5,A8,A9,A11,GOBOARD7:31; A21: f/.(len f -' 1) in LSeg(f,len f -' 1) by A13,A14,TOPREAL1:27; A22: f/.(1+1) in LSeg(f,1) by A2,TOPREAL1:27; A23: f/.(len f -' 1) in L~f by A2,A15,GOBOARD1:16; A24: f/.(1+1) in L~f by A2,A19,GOBOARD1:16; A25: not(LSeg(f,len f -' 1) is vertical & LSeg(f,1) is vertical) proof assume that A26: LSeg(f,len f -' 1) is vertical and A27: LSeg(f,1) is vertical; A28: LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A2,TOPREAL1:def 5; A29: LSeg(f,len f -' 1) = LSeg(f/.1,f/.(len f -' 1)) by A11,A13,A14,TOPREAL1: def 5; A30: p`1 = (f/.(1+1))`1 & p`1 = (f/.(len f -' 1))`1 by A16,A17,A21,A22,A26,A27,SPPOL_1:def 3; A31: p`2 >= (f/.(1+1))`2 & p`2 >= (f/.(len f -' 1))`2 by A7,A23,A24,PSCOMP_1:71; (f/.(1+1))`2 <= (f/.(len f -' 1))`2 or (f/.(1+1))`2 >= (f/.(len f -' 1))`2; then f/.(len f -' 1) in LSeg(f,1) or f/.(1+1) in LSeg(f,len f -' 1) by A5,A8,A11,A28,A29,A30,A31,GOBOARD7:8; then A32: f/.(len f -' 1) in LSeg(f,len f -' 1) /\ LSeg(f,1) or f/.(1+1) in LSeg(f,len f -' 1) /\ LSeg(f,1) by A21,A22,XBOOLE_0:def 3; A33: f.1 = f/.1 by A9,FINSEQ_4:def 4; LSeg(f,len f -' 1) /\ LSeg(f,1) <> {f/.1} by A5,A8,A11,A18,A20,A32,TARSKI:def 1; hence contradiction by A33,JORDAN4:54; end; now per cases by A25,SPPOL_1:41; suppose LSeg(f,len f -' 1) is horizontal; then A34: p`2 = (f/.(len f -' 1))`2 by A16,A21,SPPOL_1:def 2; then A35: (f/.(len f -' 1))`1 <> p`1 by A18,TOPREAL3:11; A36: f/.(len f -' 1) in N-most L~f by A7,A23,A34,Th14; then (f/.(len f -' 1))`1 >= p`1 by PSCOMP_1:98; then A37: (f/.(len f -' 1))`1 > p`1 by A35,REAL_1:def 5; (f/.(len f -' 1))`1 <= (N-max L~f)`1 by A36,PSCOMP_1:98; hence thesis by A37,AXIOMS:22; suppose LSeg(f,1) is horizontal; then A38: p`2 = (f/.(1+1))`2 by A17,A22,SPPOL_1:def 2; then A39: (f/.(1+1))`1 <> p`1 by A20,TOPREAL3:11; A40: f/.(1+1) in N-most L~f by A7,A24,A38,Th14; then (f/.(1+1))`1 >= p`1 by PSCOMP_1:98; then A41: (f/.(1+1))`1 > p`1 by A39,REAL_1:def 5; (f/.(1+1))`1 <= (N-max L~f)`1 by A40,PSCOMP_1:98; hence thesis by A41,AXIOMS:22; end; hence thesis; suppose that A42: 1 < i and A43: i < len f; A44: i-'1+1 = i by A42,AMI_5:4; then A45: i-'1 >= 1 by A42,NAT_1:38; i-'1 <= i by A44,NAT_1:29; then i-'1 <= len f by A43,AXIOMS:22; then A46: i-'1 in dom f by A45,FINSEQ_3:27; A47: p in LSeg(f,i-'1) by A5,A43,A44,A45,TOPREAL1:27; A48: i+1 <= len f by A43,NAT_1:38; then A49: p in LSeg(f,i) by A5,A42,TOPREAL1:27; A50: p <> f/.(i-'1) by A4,A5,A44,A46,GOBOARD7:31; i+1 >= 1 by NAT_1:29; then A51: i+1 in dom f by A48,FINSEQ_3:27; then A52: p <> f/.(i+1) by A4,A5,GOBOARD7:31; A53: f/.(i-'1) in LSeg(f,i-'1) by A43,A44,A45,TOPREAL1:27; A54: f/.(i+1) in LSeg(f,i) by A42,A48,TOPREAL1:27; A55: f/.(i-'1) in L~f by A2,A46,GOBOARD1:16; A56: f/.(i+1) in L~f by A2,A51,GOBOARD1:16; A57: not(LSeg(f,i-'1) is vertical & LSeg(f,i) is vertical) proof assume that A58: LSeg(f,i-'1) is vertical and A59: LSeg(f,i) is vertical; A60: i-'1+1+1 = i-'1+(1+1) by XCMPLX_1:1; A61: LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A42,A48,TOPREAL1:def 5; A62: LSeg(f,i-'1) = LSeg(f/.i,f/.(i-'1)) by A43,A44,A45,TOPREAL1:def 5; A63: p`1 = (f/.(i+1))`1 & p`1 = (f/.(i-'1))`1 by A47,A49,A53,A54,A58,A59,SPPOL_1:def 3; A64: p`2 >= (f/.(i+1))`2 & p`2 >= (f/.(i-'1))`2 by A7,A55,A56,PSCOMP_1:71; (f/.(i+1))`2 <= (f/.(i-'1))`2 or (f/.(i+1))`2 >= (f/.(i-'1))`2; then f/.(i-'1) in LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1) by A5,A61,A62,A63,A64,GOBOARD7:8; then f/.(i-'1) in LSeg(f,i-'1) /\ LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1) /\ LSeg(f,i) by A53,A54,XBOOLE_0:def 3; then LSeg(f,i-'1) /\ LSeg(f,i) <> {f/.i} by A5,A50,A52,TARSKI:def 1; hence contradiction by A44,A45,A48,A60,TOPREAL1:def 8; end; now per cases by A57,SPPOL_1:41; suppose LSeg(f,i-'1) is horizontal; then A65: p`2 = (f/.(i-'1))`2 by A47,A53,SPPOL_1:def 2; then A66: (f/.(i-'1))`1 <> p`1 by A50,TOPREAL3:11; A67: f/.(i-'1) in N-most L~f by A7,A55,A65,Th14; then (f/.(i-'1))`1 >= p`1 by PSCOMP_1:98; then A68: (f/.(i-'1))`1 > p`1 by A66,REAL_1:def 5; (f/.(i-'1))`1 <= (N-max L~f)`1 by A67,PSCOMP_1:98; hence thesis by A68,AXIOMS:22; suppose LSeg(f,i) is horizontal; then A69: p`2 = (f/.(i+1))`2 by A49,A54,SPPOL_1:def 2; then A70: (f/.(i+1))`1 <> p`1 by A52,TOPREAL3:11; A71: f/.(i+1) in N-most L~f by A7,A56,A69,Th14; then (f/.(i+1))`1 >= p`1 by PSCOMP_1:98; then A72: (f/.(i+1))`1 > p`1 by A70,REAL_1:def 5; (f/.(i+1))`1 <= (N-max L~f)`1 by A71,PSCOMP_1:98; hence thesis by A72,AXIOMS:22; end; hence thesis; end; theorem Th56: N-min L~f <> N-max L~f proof (N-min L~f)`1 < (N-max L~f)`1 by Th55; hence thesis; end; theorem Th57: (E-min L~f)`2 < (E-max L~f)`2 proof set p = E-min L~f, i = p..f; A1: len f > 3+1 by GOBOARD7:36; then A2: len f >= 1+1 by AXIOMS:22; A3: p in rng f by Th49; then A4: i in dom f by FINSEQ_4:30; A5: p = f.i by A3,FINSEQ_4:29 .= f/.i by A4,FINSEQ_4:def 4; A6: 1 <= i & i <= len f by A4,FINSEQ_3:27; A7: p`1 = E-bound L~f by PSCOMP_1:104; per cases by A6,REAL_1:def 5; suppose A8: i = 1 or i = len f; A9: 1 in dom f by FINSEQ_5:6; A10: len f in dom f by FINSEQ_5:6; A11: f/.1 = f/.len f by FINSEQ_6:def 1; A12: p = f/.1 by A5,A8,FINSEQ_6:def 1; len f >= 1 by A1,AXIOMS:22; then A13: len f -' 1+1 = len f by AMI_5:4; then len f -' 1 > 3 by A1,AXIOMS:24; then A14: len f -' 1 > 1 by AXIOMS:22; len f -' 1 <= len f by A13,NAT_1:29; then A15: len f -' 1 in dom f by A14,FINSEQ_3:27; A16: p in LSeg(f,len f -' 1) by A5,A8,A11,A13,A14,TOPREAL1:27; A17: p in LSeg(f,1) by A2,A12,TOPREAL1:27; A18: p <> f/.(len f -' 1) by A5,A8,A10,A11,A13,A15,GOBOARD7:31; A19: 1+1 in dom f by A2,FINSEQ_3:27; then A20: p <> f/.(1+1) by A5,A8,A9,A11,GOBOARD7:31; A21: f/.(len f -' 1) in LSeg(f,len f -' 1) by A13,A14,TOPREAL1:27; A22: f/.(1+1) in LSeg(f,1) by A2,TOPREAL1:27; A23: f/.(len f -' 1) in L~f by A2,A15,GOBOARD1:16; A24: f/.(1+1) in L~f by A2,A19,GOBOARD1:16; A25: not(LSeg(f,len f -' 1) is horizontal & LSeg(f,1) is horizontal) proof assume that A26: LSeg(f,len f -' 1) is horizontal and A27: LSeg(f,1) is horizontal; A28: LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A2,TOPREAL1:def 5; A29: LSeg(f,len f -' 1) = LSeg(f/.1,f/.(len f -' 1)) by A11,A13,A14,TOPREAL1: def 5; A30: p`2 = (f/.(1+1))`2 & p`2 = (f/.(len f -' 1))`2 by A16,A17,A21,A22,A26,A27,SPPOL_1:def 2; A31: p`1 >= (f/.(1+1))`1 & p`1 >= (f/.(len f -' 1))`1 by A7,A23,A24,PSCOMP_1:71; (f/.(1+1))`1 <= (f/.(len f -' 1))`1 or (f/.(1+1))`1 >= (f/.(len f -' 1))`1; then f/.(len f -' 1) in LSeg(f,1) or f/.(1+1) in LSeg(f,len f -' 1) by A5,A8,A11,A28,A29,A30,A31,GOBOARD7:9; then A32: f/.(len f -' 1) in LSeg(f,len f -' 1) /\ LSeg(f,1) or f/.(1+1) in LSeg(f,len f -' 1) /\ LSeg(f,1) by A21,A22,XBOOLE_0:def 3; A33: f.1 = f/.1 by A9,FINSEQ_4:def 4; LSeg(f,len f -' 1) /\ LSeg(f,1) <> {f/.1} by A5,A8,A11,A18,A20,A32,TARSKI:def 1; hence contradiction by A33,JORDAN4:54; end; now per cases by A25,SPPOL_1:41; suppose LSeg(f,len f -' 1) is vertical; then A34: p`1 = (f/.(len f -' 1))`1 by A16,A21,SPPOL_1:def 3; then A35: (f/.(len f -' 1))`2 <> p`2 by A18,TOPREAL3:11; A36: f/.(len f -' 1) in E-most L~f by A7,A23,A34,Th17; then (f/.(len f -' 1))`2 >= p`2 by PSCOMP_1:108; then A37: (f/.(len f -' 1))`2 > p`2 by A35,REAL_1:def 5; (f/.(len f -' 1))`2 <= (E-max L~f)`2 by A36,PSCOMP_1:108; hence thesis by A37,AXIOMS:22; suppose LSeg(f,1) is vertical; then A38: p`1 = (f/.(1+1))`1 by A17,A22,SPPOL_1:def 3; then A39: (f/.(1+1))`2 <> p`2 by A20,TOPREAL3:11; A40: f/.(1+1) in E-most L~f by A7,A24,A38,Th17; then (f/.(1+1))`2 >= p`2 by PSCOMP_1:108; then A41: (f/.(1+1))`2 > p`2 by A39,REAL_1:def 5; (f/.(1+1))`2 <= (E-max L~f)`2 by A40,PSCOMP_1:108; hence thesis by A41,AXIOMS:22; end; hence thesis; suppose that A42: 1 < i and A43: i < len f; A44: i-'1+1 = i by A42,AMI_5:4; then A45: i-'1 >= 1 by A42,NAT_1:38; i-'1 <= i by A44,NAT_1:29; then i-'1 <= len f by A43,AXIOMS:22; then A46: i-'1 in dom f by A45,FINSEQ_3:27; A47: p in LSeg(f,i-'1) by A5,A43,A44,A45,TOPREAL1:27; A48: i+1 <= len f by A43,NAT_1:38; then A49: p in LSeg(f,i) by A5,A42,TOPREAL1:27; A50: p <> f/.(i-'1) by A4,A5,A44,A46,GOBOARD7:31; i+1 >= 1 by NAT_1:29; then A51: i+1 in dom f by A48,FINSEQ_3:27; then A52: p <> f/.(i+1) by A4,A5,GOBOARD7:31; A53: f/.(i-'1) in LSeg(f,i-'1) by A43,A44,A45,TOPREAL1:27; A54: f/.(i+1) in LSeg(f,i) by A42,A48,TOPREAL1:27; A55: f/.(i-'1) in L~f by A2,A46,GOBOARD1:16; A56: f/.(i+1) in L~f by A2,A51,GOBOARD1:16; A57: not(LSeg(f,i-'1) is horizontal & LSeg(f,i) is horizontal) proof assume that A58: LSeg(f,i-'1) is horizontal and A59: LSeg(f,i) is horizontal; A60: i-'1+1+1 = i-'1+(1+1) by XCMPLX_1:1; A61: LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A42,A48,TOPREAL1:def 5; A62: LSeg(f,i-'1) = LSeg(f/.i,f/.(i-'1)) by A43,A44,A45,TOPREAL1:def 5; A63: p`2 = (f/.(i+1))`2 & p`2 = (f/.(i-'1))`2 by A47,A49,A53,A54,A58,A59,SPPOL_1:def 2; A64: p`1 >= (f/.(i+1))`1 & p`1 >= (f/.(i-'1))`1 by A7,A55,A56,PSCOMP_1:71; (f/.(i+1))`1 <= (f/.(i-'1))`1 or (f/.(i+1))`1 >= (f/.(i-'1))`1; then f/.(i-'1) in LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1) by A5,A61,A62,A63,A64,GOBOARD7:9; then f/.(i-'1) in LSeg(f,i-'1) /\ LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1) /\ LSeg(f,i) by A53,A54,XBOOLE_0:def 3; then LSeg(f,i-'1) /\ LSeg(f,i) <> {f/.i} by A5,A50,A52,TARSKI:def 1; hence contradiction by A44,A45,A48,A60,TOPREAL1:def 8; end; now per cases by A57,SPPOL_1:41; suppose LSeg(f,i-'1) is vertical; then A65: p`1 = (f/.(i-'1))`1 by A47,A53,SPPOL_1:def 3; then A66: (f/.(i-'1))`2 <> p`2 by A50,TOPREAL3:11; A67: f/.(i-'1) in E-most L~f by A7,A55,A65,Th17; then (f/.(i-'1))`2 >= p`2 by PSCOMP_1:108; then A68: (f/.(i-'1))`2 > p`2 by A66,REAL_1:def 5; (f/.(i-'1))`2 <= (E-max L~f)`2 by A67,PSCOMP_1:108; hence thesis by A68,AXIOMS:22; suppose LSeg(f,i) is vertical; then A69: p`1 = (f/.(i+1))`1 by A49,A54,SPPOL_1:def 3; then A70: (f/.(i+1))`2 <> p`2 by A52,TOPREAL3:11; A71: f/.(i+1) in E-most L~f by A7,A56,A69,Th17; then (f/.(i+1))`2 >= p`2 by PSCOMP_1:108; then A72: (f/.(i+1))`2 > p`2 by A70,REAL_1:def 5; (f/.(i+1))`2 <= (E-max L~f)`2 by A71,PSCOMP_1:108; hence thesis by A72,AXIOMS:22; end; hence thesis; end; theorem E-min L~f <> E-max L~f proof (E-min L~f)`2 < (E-max L~f)`2 by Th57; hence thesis; end; theorem Th59: (S-min L~f)`1 < (S-max L~f)`1 proof set p = S-min L~f, i = p..f; A1: len f > 3+1 by GOBOARD7:36; then A2: len f >= 1+1 by AXIOMS:22; A3: p in rng f by Th45; then A4: i in dom f by FINSEQ_4:30; A5: p = f.i by A3,FINSEQ_4:29 .= f/.i by A4,FINSEQ_4:def 4; A6: 1 <= i & i <= len f by A4,FINSEQ_3:27; A7: p`2 = S-bound L~f by PSCOMP_1:114; per cases by A6,REAL_1:def 5; suppose A8: i = 1 or i = len f; A9: 1 in dom f by FINSEQ_5:6; A10: len f in dom f by FINSEQ_5:6; A11: f/.1 = f/.len f by FINSEQ_6:def 1; A12: p = f/.1 by A5,A8,FINSEQ_6:def 1; len f >= 1 by A1,AXIOMS:22; then A13: len f -' 1+1 = len f by AMI_5:4; then len f -' 1 > 3 by A1,AXIOMS:24; then A14: len f -' 1 > 1 by AXIOMS:22; len f -' 1 <= len f by A13,NAT_1:29; then A15: len f -' 1 in dom f by A14,FINSEQ_3:27; A16: p in LSeg(f,len f -' 1) by A5,A8,A11,A13,A14,TOPREAL1:27; A17: p in LSeg(f,1) by A2,A12,TOPREAL1:27; A18: p <> f/.(len f -' 1) by A5,A8,A10,A11,A13,A15,GOBOARD7:31; A19: 1+1 in dom f by A2,FINSEQ_3:27; then A20: p <> f/.(1+1) by A5,A8,A9,A11,GOBOARD7:31; A21: f/.(len f -' 1) in LSeg(f,len f -' 1) by A13,A14,TOPREAL1:27; A22: f/.(1+1) in LSeg(f,1) by A2,TOPREAL1:27; A23: f/.(len f -' 1) in L~f by A2,A15,GOBOARD1:16; A24: f/.(1+1) in L~f by A2,A19,GOBOARD1:16; A25: not(LSeg(f,len f -' 1) is vertical & LSeg(f,1) is vertical) proof assume that A26: LSeg(f,len f -' 1) is vertical and A27: LSeg(f,1) is vertical; A28: LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A2,TOPREAL1:def 5; A29: LSeg(f,len f -' 1) = LSeg(f/.1,f/.(len f -' 1)) by A11,A13,A14,TOPREAL1: def 5; A30: p`1 = (f/.(1+1))`1 & p`1 = (f/.(len f -' 1))`1 by A16,A17,A21,A22,A26,A27,SPPOL_1:def 3; A31: p`2 <= (f/.(1+1))`2 & p`2 <= (f/.(len f -' 1))`2 by A7,A23,A24,PSCOMP_1:71; (f/.(1+1))`2 <= (f/.(len f -' 1))`2 or (f/.(1+1))`2 >= (f/.(len f -' 1))`2; then f/.(len f -' 1) in LSeg(f,1) or f/.(1+1) in LSeg(f,len f -' 1) by A5,A8,A11,A28,A29,A30,A31,GOBOARD7:8; then A32: f/.(len f -' 1) in LSeg(f,len f -' 1) /\ LSeg(f,1) or f/.(1+1) in LSeg(f,len f -' 1) /\ LSeg(f,1) by A21,A22,XBOOLE_0:def 3; A33: f.1 = f/.1 by A9,FINSEQ_4:def 4; LSeg(f,len f -' 1) /\ LSeg(f,1) <> {f/.1} by A5,A8,A11,A18,A20,A32,TARSKI:def 1; hence contradiction by A33,JORDAN4:54; end; now per cases by A25,SPPOL_1:41; suppose LSeg(f,len f -' 1) is horizontal; then A34: p`2 = (f/.(len f -' 1))`2 by A16,A21,SPPOL_1:def 2; then A35: (f/.(len f -' 1))`1 <> p`1 by A18,TOPREAL3:11; A36: f/.(len f -' 1) in S-most L~f by A7,A23,A34,Th15; then (f/.(len f -' 1))`1 >= p`1 by PSCOMP_1:118; then A37: (f/.(len f -' 1))`1 > p`1 by A35,REAL_1:def 5; (f/.(len f -' 1))`1 <= (S-max L~f)`1 by A36,PSCOMP_1:118; hence thesis by A37,AXIOMS:22; suppose LSeg(f,1) is horizontal; then A38: p`2 = (f/.(1+1))`2 by A17,A22,SPPOL_1:def 2; then A39: (f/.(1+1))`1 <> p`1 by A20,TOPREAL3:11; A40: f/.(1+1) in S-most L~f by A7,A24,A38,Th15; then (f/.(1+1))`1 >= p`1 by PSCOMP_1:118; then A41: (f/.(1+1))`1 > p`1 by A39,REAL_1:def 5; (f/.(1+1))`1 <= (S-max L~f)`1 by A40,PSCOMP_1:118; hence thesis by A41,AXIOMS:22; end; hence thesis; suppose that A42: 1 < i and A43: i < len f; A44: i-'1+1 = i by A42,AMI_5:4; then A45: i-'1 >= 1 by A42,NAT_1:38; i-'1 <= i by A44,NAT_1:29; then i-'1 <= len f by A43,AXIOMS:22; then A46: i-'1 in dom f by A45,FINSEQ_3:27; A47: p in LSeg(f,i-'1) by A5,A43,A44,A45,TOPREAL1:27; A48: i+1 <= len f by A43,NAT_1:38; then A49: p in LSeg(f,i) by A5,A42,TOPREAL1:27; A50: p <> f/.(i-'1) by A4,A5,A44,A46,GOBOARD7:31; i+1 >= 1 by NAT_1:29; then A51: i+1 in dom f by A48,FINSEQ_3:27; then A52: p <> f/.(i+1) by A4,A5,GOBOARD7:31; A53: f/.(i-'1) in LSeg(f,i-'1) by A43,A44,A45,TOPREAL1:27; A54: f/.(i+1) in LSeg(f,i) by A42,A48,TOPREAL1:27; A55: f/.(i-'1) in L~f by A2,A46,GOBOARD1:16; A56: f/.(i+1) in L~f by A2,A51,GOBOARD1:16; A57: not(LSeg(f,i-'1) is vertical & LSeg(f,i) is vertical) proof assume that A58: LSeg(f,i-'1) is vertical and A59: LSeg(f,i) is vertical; A60: i-'1+1+1 = i-'1+(1+1) by XCMPLX_1:1; A61: LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A42,A48,TOPREAL1:def 5; A62: LSeg(f,i-'1) = LSeg(f/.i,f/.(i-'1)) by A43,A44,A45,TOPREAL1:def 5; A63: p`1 = (f/.(i+1))`1 & p`1 = (f/.(i-'1))`1 by A47,A49,A53,A54,A58,A59,SPPOL_1:def 3; A64: p`2 <= (f/.(i+1))`2 & p`2 <= (f/.(i-'1))`2 by A7,A55,A56,PSCOMP_1:71; (f/.(i+1))`2 <= (f/.(i-'1))`2 or (f/.(i+1))`2 >= (f/.(i-'1))`2; then f/.(i-'1) in LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1) by A5,A61,A62,A63,A64,GOBOARD7:8; then f/.(i-'1) in LSeg(f,i-'1) /\ LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1) /\ LSeg(f,i) by A53,A54,XBOOLE_0:def 3; then LSeg(f,i-'1) /\ LSeg(f,i) <> {f/.i} by A5,A50,A52,TARSKI:def 1; hence contradiction by A44,A45,A48,A60,TOPREAL1:def 8; end; now per cases by A57,SPPOL_1:41; suppose LSeg(f,i-'1) is horizontal; then A65: p`2 = (f/.(i-'1))`2 by A47,A53,SPPOL_1:def 2; then A66: (f/.(i-'1))`1 <> p`1 by A50,TOPREAL3:11; A67: f/.(i-'1) in S-most L~f by A7,A55,A65,Th15; then (f/.(i-'1))`1 >= p`1 by PSCOMP_1:118; then A68: (f/.(i-'1))`1 > p`1 by A66,REAL_1:def 5; (f/.(i-'1))`1 <= (S-max L~f)`1 by A67,PSCOMP_1:118; hence thesis by A68,AXIOMS:22; suppose LSeg(f,i) is horizontal; then A69: p`2 = (f/.(i+1))`2 by A49,A54,SPPOL_1:def 2; then A70: (f/.(i+1))`1 <> p`1 by A52,TOPREAL3:11; A71: f/.(i+1) in S-most L~f by A7,A56,A69,Th15; then (f/.(i+1))`1 >= p`1 by PSCOMP_1:118; then A72: (f/.(i+1))`1 > p`1 by A70,REAL_1:def 5; (f/.(i+1))`1 <= (S-max L~f)`1 by A71,PSCOMP_1:118; hence thesis by A72,AXIOMS:22; end; hence thesis; end; theorem Th60: S-min L~f <> S-max L~f proof (S-min L~f)`1 < (S-max L~f)`1 by Th59; hence thesis; end; theorem Th61: (W-min L~f)`2 < (W-max L~f)`2 proof set p = W-min L~f, i = p..f; A1: len f > 3+1 by GOBOARD7:36; then A2: len f >= 1+1 by AXIOMS:22; A3: p in rng f by Th47; then A4: i in dom f by FINSEQ_4:30; A5: p = f.i by A3,FINSEQ_4:29 .= f/.i by A4,FINSEQ_4:def 4; A6: 1 <= i & i <= len f by A4,FINSEQ_3:27; A7: p`1 = W-bound L~f by PSCOMP_1:84; per cases by A6,REAL_1:def 5; suppose A8: i = 1 or i = len f; A9: 1 in dom f by FINSEQ_5:6; A10: len f in dom f by FINSEQ_5:6; A11: f/.1 = f/.len f by FINSEQ_6:def 1; A12: p = f/.1 by A5,A8,FINSEQ_6:def 1; len f >= 1 by A1,AXIOMS:22; then A13: len f -' 1+1 = len f by AMI_5:4; then len f -' 1 > 3 by A1,AXIOMS:24; then A14: len f -' 1 > 1 by AXIOMS:22; len f -' 1 <= len f by A13,NAT_1:29; then A15: len f -' 1 in dom f by A14,FINSEQ_3:27; A16: p in LSeg(f,len f -' 1) by A5,A8,A11,A13,A14,TOPREAL1:27; A17: p in LSeg(f,1) by A2,A12,TOPREAL1:27; A18: p <> f/.(len f -' 1) by A5,A8,A10,A11,A13,A15,GOBOARD7:31; A19: 1+1 in dom f by A2,FINSEQ_3:27; then A20: p <> f/.(1+1) by A5,A8,A9,A11,GOBOARD7:31; A21: f/.(len f -' 1) in LSeg(f,len f -' 1) by A13,A14,TOPREAL1:27; A22: f/.(1+1) in LSeg(f,1) by A2,TOPREAL1:27; A23: f/.(len f -' 1) in L~f by A2,A15,GOBOARD1:16; A24: f/.(1+1) in L~f by A2,A19,GOBOARD1:16; A25: not(LSeg(f,len f -' 1) is horizontal & LSeg(f,1) is horizontal) proof assume that A26: LSeg(f,len f -' 1) is horizontal and A27: LSeg(f,1) is horizontal; A28: LSeg(f,1) = LSeg(f/.1,f/.(1+1)) by A2,TOPREAL1:def 5; A29: LSeg(f,len f -' 1) = LSeg(f/.1,f/.(len f -' 1)) by A11,A13,A14,TOPREAL1: def 5; A30: p`2 = (f/.(1+1))`2 & p`2 = (f/.(len f -' 1))`2 by A16,A17,A21,A22,A26,A27,SPPOL_1:def 2; A31: p`1 <= (f/.(1+1))`1 & p`1 <= (f/.(len f -' 1))`1 by A7,A23,A24,PSCOMP_1:71; (f/.(1+1))`1 <= (f/.(len f -' 1))`1 or (f/.(1+1))`1 >= (f/.(len f -' 1))`1; then f/.(len f -' 1) in LSeg(f,1) or f/.(1+1) in LSeg(f,len f -' 1) by A5,A8,A11,A28,A29,A30,A31,GOBOARD7:9; then A32: f/.(len f -' 1) in LSeg(f,len f -' 1) /\ LSeg(f,1) or f/.(1+1) in LSeg(f,len f -' 1) /\ LSeg(f,1) by A21,A22,XBOOLE_0:def 3; A33: f.1 = f/.1 by A9,FINSEQ_4:def 4; LSeg(f,len f -' 1) /\ LSeg(f,1) <> {f/.1} by A5,A8,A11,A18,A20,A32,TARSKI:def 1; hence contradiction by A33,JORDAN4:54; end; now per cases by A25,SPPOL_1:41; suppose LSeg(f,len f -' 1) is vertical; then A34: p`1 = (f/.(len f -' 1))`1 by A16,A21,SPPOL_1:def 3; then A35: (f/.(len f -' 1))`2 <> p`2 by A18,TOPREAL3:11; A36: f/.(len f -' 1) in W-most L~f by A7,A23,A34,Th16; then (f/.(len f -' 1))`2 >= p`2 by PSCOMP_1:88; then A37: (f/.(len f -' 1))`2 > p`2 by A35,REAL_1:def 5; (f/.(len f -' 1))`2 <= (W-max L~f)`2 by A36,PSCOMP_1:88; hence thesis by A37,AXIOMS:22; suppose LSeg(f,1) is vertical; then A38: p`1 = (f/.(1+1))`1 by A17,A22,SPPOL_1:def 3; then A39: (f/.(1+1))`2 <> p`2 by A20,TOPREAL3:11; A40: f/.(1+1) in W-most L~f by A7,A24,A38,Th16; then (f/.(1+1))`2 >= p`2 by PSCOMP_1:88; then A41: (f/.(1+1))`2 > p`2 by A39,REAL_1:def 5; (f/.(1+1))`2 <= (W-max L~f)`2 by A40,PSCOMP_1:88; hence thesis by A41,AXIOMS:22; end; hence thesis; suppose that A42: 1 < i and A43: i < len f; A44: i-'1+1 = i by A42,AMI_5:4; then A45: i-'1 >= 1 by A42,NAT_1:38; i-'1 <= i by A44,NAT_1:29; then i-'1 <= len f by A43,AXIOMS:22; then A46: i-'1 in dom f by A45,FINSEQ_3:27; A47: p in LSeg(f,i-'1) by A5,A43,A44,A45,TOPREAL1:27; A48: i+1 <= len f by A43,NAT_1:38; then A49: p in LSeg(f,i) by A5,A42,TOPREAL1:27; A50: p <> f/.(i-'1) by A4,A5,A44,A46,GOBOARD7:31; i+1 >= 1 by NAT_1:29; then A51: i+1 in dom f by A48,FINSEQ_3:27; then A52: p <> f/.(i+1) by A4,A5,GOBOARD7:31; A53: f/.(i-'1) in LSeg(f,i-'1) by A43,A44,A45,TOPREAL1:27; A54: f/.(i+1) in LSeg(f,i) by A42,A48,TOPREAL1:27; A55: f/.(i-'1) in L~f by A2,A46,GOBOARD1:16; A56: f/.(i+1) in L~f by A2,A51,GOBOARD1:16; A57: not(LSeg(f,i-'1) is horizontal & LSeg(f,i) is horizontal) proof assume that A58: LSeg(f,i-'1) is horizontal and A59: LSeg(f,i) is horizontal; A60: i-'1+1+1 = i-'1+(1+1) by XCMPLX_1:1; A61: LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A42,A48,TOPREAL1:def 5; A62: LSeg(f,i-'1) = LSeg(f/.i,f/.(i-'1)) by A43,A44,A45,TOPREAL1:def 5; A63: p`2 = (f/.(i+1))`2 & p`2 = (f/.(i-'1))`2 by A47,A49,A53,A54,A58,A59,SPPOL_1:def 2; A64: p`1 <= (f/.(i+1))`1 & p`1 <= (f/.(i-'1))`1 by A7,A55,A56,PSCOMP_1:71; (f/.(i+1))`1 <= (f/.(i-'1))`1 or (f/.(i+1))`1 >= (f/.(i-'1))`1; then f/.(i-'1) in LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1) by A5,A61,A62,A63,A64,GOBOARD7:9; then f/.(i-'1) in LSeg(f,i-'1) /\ LSeg(f,i) or f/.(i+1) in LSeg(f,i-'1) /\ LSeg(f,i) by A53,A54,XBOOLE_0:def 3; then LSeg(f,i-'1) /\ LSeg(f,i) <> {f/.i} by A5,A50,A52,TARSKI:def 1; hence contradiction by A44,A45,A48,A60,TOPREAL1:def 8; end; now per cases by A57,SPPOL_1:41; suppose LSeg(f,i-'1) is vertical; then A65: p`1 = (f/.(i-'1))`1 by A47,A53,SPPOL_1:def 3; then A66: (f/.(i-'1))`2 <> p`2 by A50,TOPREAL3:11; A67: f/.(i-'1) in W-most L~f by A7,A55,A65,Th16; then (f/.(i-'1))`2 >= p`2 by PSCOMP_1:88; then A68: (f/.(i-'1))`2 > p`2 by A66,REAL_1:def 5; (f/.(i-'1))`2 <= (W-max L~f)`2 by A67,PSCOMP_1:88; hence thesis by A68,AXIOMS:22; suppose LSeg(f,i) is vertical; then A69: p`1 = (f/.(i+1))`1 by A49,A54,SPPOL_1:def 3; then A70: (f/.(i+1))`2 <> p`2 by A52,TOPREAL3:11; A71: f/.(i+1) in W-most L~f by A7,A56,A69,Th16; then (f/.(i+1))`2 >= p`2 by PSCOMP_1:88; then A72: (f/.(i+1))`2 > p`2 by A70,REAL_1:def 5; (f/.(i+1))`2 <= (W-max L~f)`2 by A71,PSCOMP_1:88; hence thesis by A72,AXIOMS:22; end; hence thesis; end; theorem Th62: W-min L~f <> W-max L~f proof (W-min L~f)`2 < (W-max L~f)`2 by Th61; hence thesis; end; theorem Th63: LSeg(NW-corner L~f,N-min L~f) misses LSeg(N-max L~f,NE-corner L~f) proof assume LSeg(NW-corner L~f,N-min L~f) meets LSeg(N-max L~f,NE-corner L~f) ; then consider p being set such that A1: p in LSeg(NW-corner L~f,N-min L~f) and A2: p in LSeg(N-max L~f,NE-corner L~f) by XBOOLE_0:3; reconsider p as Point of TOP-REAL 2 by A1; (NW-corner L~f)`1 <= (N-min L~f)`1 by PSCOMP_1:97; then A3: p`1 <= (N-min L~f)`1 by A1,TOPREAL1:9; (N-max L~f)`1 <= (NE-corner L~f)`1 by PSCOMP_1:97; then (N-max L~f)`1 <= p`1 by A2,TOPREAL1:9; then A4:(N-min L~f)`1 >= (N-max L~f)`1 by A3,AXIOMS:22; (N-min L~f)`1 <= (N-max L~f)`1 by PSCOMP_1:97; then A5:(N-min L~f)`1 = (N-max L~f)`1 by A4,AXIOMS:21; (N-min L~f)`2 = (N-max L~f)`2 by PSCOMP_1:95; then N-min L~f = N-max L~f by A5,TOPREAL3:11; hence contradiction by Th56; end; theorem Th64: for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st f is_S-Seq & p <> f/.1 & (p`1 = (f/.1)`1 or p`2 = (f/.1)`2) & LSeg(p,f/.1) /\ L~f = {f/.1} holds <*p*>^f is S-Sequence_in_R2 proof let f be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2 such that A1: f is_S-Seq and A2: p <> f/.1 and A3: p`1 = (f/.1)`1 or p`2 = (f/.1)`2 and A4: LSeg(p,f/.1) /\ L~f = {f/.1}; reconsider f as S-Sequence_in_R2 by A1; A5: 1 in dom f by FINSEQ_5:6; A6: len f >= 1+1 by TOPREAL1:def 10; then A7: f/.1 in LSeg(f,1) by TOPREAL1:27; set g = <*p*>^f; g is being_S-Seq proof A8: <*p*> is one-to-one by FINSEQ_3:102; now assume A9: p in rng f; A10: rng f c= L~f by A6,SPPOL_2:18; p in LSeg(p,f/.1) by TOPREAL1:6; then p in {f/.1} by A4,A9,A10,XBOOLE_0:def 3; hence contradiction by A2,TARSKI:def 1; end; then {p} misses rng f by ZFMISC_1:56; then rng<*p*> misses rng f by FINSEQ_1:56; hence g is one-to-one by A8,FINSEQ_3:98; len g = len<*p*> + len f by FINSEQ_1:35; then len g >= len f by NAT_1:29; hence len g >= 2 by A6,AXIOMS:22; LSeg(f,1) c= L~f by TOPREAL3:26; then LSeg(p,f/.1) /\ LSeg(f,1) = {f/.1} by A4,A7,Th2; hence g is unfolded by SPPOL_2:30; A11: len<*p*> = 1 by FINSEQ_1:56; then A12: <*p*> is s.n.c. by SPPOL_2:34; A13: <*p*>/.len <*p*> = p by A11,FINSEQ_4:25; L~<*p*> = {} by SPPOL_2:12; then L~<*p*> /\ L~f = {}; then A14: L~<*p*> misses L~f by XBOOLE_0:def 7; A15: now let i such that 1<=i; assume A16: i+2 <= len <*p*>; 2 <= i+2 by NAT_1:29; hence LSeg(<*p*>,i) misses LSeg(p,f/.1) by A11,A16,AXIOMS:22; end; now let i such that A17: 1+1<=i and A18: i+1 <= len f; A19: 2 in dom f by A6,FINSEQ_3:27; now assume f/.1 in LSeg(f,i); then A20: f/.1 in LSeg(f,1) /\ LSeg(f,i) by A7,XBOOLE_0:def 3; then A21: LSeg(f,1) meets LSeg(f,i) by XBOOLE_0:4; now per cases by A17,REAL_1:def 5; case A22: i = 1+1; then LSeg(f,1) /\ LSeg(f,1+1) = {f/.2} by A18,TOPREAL1:def 8; hence f/.1 = f/.2 by A20,A22,TARSKI:def 1; case i > 1+1; hence contradiction by A21,TOPREAL1:def 9; end; then f.1 = f/.2 by A5,FINSEQ_4:def 4 .= f.2 by A19,FINSEQ_4:def 4; hence contradiction by A5,A19,FUNCT_1:def 8; end; then not f/.1 in LSeg(f,i) /\ LSeg(p,f/.1) by XBOOLE_0:def 3; then A23: LSeg(f,i) /\ LSeg(p,f/.1) <> {f/.1} by TARSKI:def 1; LSeg(f,i) c= L~f by TOPREAL3:26; then LSeg(f,i) /\ LSeg(p,f/.1) c= {f/.1} by A4,XBOOLE_1:26; then LSeg(f,i) /\ LSeg(p,f/.1) = {} by A23,ZFMISC_1:39; hence LSeg(f,i) misses LSeg(p,f/.1) by XBOOLE_0:def 7; end; hence g is s.n.c. by A12,A13,A14,A15,SPPOL_2:37; A24: <*p*> is special by SPPOL_2:39; <*p*>/.len <*p*> = <*p*>/.1 by FINSEQ_1:56 .= p by FINSEQ_4:25; hence g is special by A3,A24,GOBOARD2:13; end; hence thesis; end; theorem Th65: for f being FinSequence of TOP-REAL 2, p being Point of TOP-REAL 2 st f is_S-Seq & p <> f/.len f & (p`1 = (f/.len f)`1 or p`2 = (f/.len f)`2) & LSeg(p,f/.len f) /\ L~f = {f/.len f} holds f^<*p*> is S-Sequence_in_R2 proof let f be FinSequence of TOP-REAL 2, p be Point of TOP-REAL 2 such that A1: f is_S-Seq and A2: p <> f/.len f and A3: p`1 = (f/.len f)`1 or p`2 = (f/.len f)`2 and A4: LSeg(p,f/.len f) /\ L~f = {f/.len f}; set g = <*f/.len f,p*>; reconsider f' = f as S-Sequence_in_R2 by A1; A5: len f' in dom f' by FINSEQ_5:6; A6: len g = 1+1 by FINSEQ_1:61; A7: g.1 = f/.len f by FINSEQ_1:61 .= f.len f by A5,FINSEQ_4:def 4; A8: g is_S-Seq by A2,A3,SPPOL_2:46; A9: L~f /\ L~g ={ f/.len f } by A4,SPPOL_2:21 .={f.len f} by A5,FINSEQ_4:def 4; mid(g,2,len g) = <*g/.2*> by A6,JORDAN4:27 .= <*p*> by FINSEQ_4:26; hence thesis by A1,A7,A8,A9,JORDAN3:73; end; begin :: Appending corners theorem Th66: for i,j st i in dom f & j in dom f & mid(f,i,j) is S-Sequence_in_R2 & f/.j = N-max L~f & N-max L~f <> NE-corner L~f holds mid(f,i,j)^<*NE-corner L~f*> is S-Sequence_in_R2 proof set p = NE-corner L~f; let i,j such that A1: i in dom f and A2: j in dom f and A3: mid(f,i,j) is S-Sequence_in_R2 and A4: f/.j = N-max L~f and A5: N-max L~f <> NE-corner L~f; A6: (mid(f,i,j))/.len mid(f,i,j) = N-max L~f by A1,A2,A4,Th13; then A7: p`2 = ((mid(f,i,j))/.len mid(f,i,j))`2 by PSCOMP_1:95; A8: LSeg(NE-corner L~f, N-max L~f)/\L~f = {N-max L~f} by PSCOMP_1:102; len mid(f,i,j) >= 2 by A3,TOPREAL1:def 10; then A9: N-max L~f in L~mid(f,i,j) by A6,JORDAN3:34; 1<=i & i<=len f & 1<=j & j<=len f by A1,A2,FINSEQ_3:27; then L~mid(f,i,j) c= L~f by JORDAN4:47; then LSeg(p, (mid(f,i,j))/.len mid(f,i,j)) /\ L~mid(f,i,j) = {(mid(f,i,j))/.len mid(f,i,j)} by A6,A8,A9,Th2; hence mid(f,i,j)^<*NE-corner L~f*> is S-Sequence_in_R2 by A3,A5,A6,A7,Th65; end; theorem for i,j st i in dom f & j in dom f & mid(f,i,j) is S-Sequence_in_R2 & f/.j = E-max L~f & E-max L~f <> NE-corner L~f holds mid(f,i,j)^<*NE-corner L~f*> is S-Sequence_in_R2 proof set p = NE-corner L~f; let i,j such that A1: i in dom f and A2: j in dom f and A3: mid(f,i,j) is S-Sequence_in_R2 and A4: f/.j = E-max L~f and A5: E-max L~f <> NE-corner L~f; A6: (mid(f,i,j))/.len mid(f,i,j) = E-max L~f by A1,A2,A4,Th13; then A7: p`1 = ((mid(f,i,j))/.len mid(f,i,j))`1 by PSCOMP_1:105; A8: LSeg(NE-corner L~f, E-max L~f)/\L~f = {E-max L~f} by PSCOMP_1:112; len mid(f,i,j) >= 2 by A3,TOPREAL1:def 10; then A9: E-max L~f in L~mid(f,i,j) by A6,JORDAN3:34; 1<=i & i<=len f & 1<=j & j<=len f by A1,A2,FINSEQ_3:27; then L~mid(f,i,j) c= L~f by JORDAN4:47; then LSeg(p, (mid(f,i,j))/.len mid(f,i,j)) /\ L~mid(f,i,j) = {(mid(f,i,j))/.len mid(f,i,j)} by A6,A8,A9,Th2; hence mid(f,i,j)^<*NE-corner L~f*> is S-Sequence_in_R2 by A3,A5,A6,A7,Th65; end; theorem Th68: for i,j st i in dom f & j in dom f & mid(f,i,j) is S-Sequence_in_R2 & f/.j = S-max L~f & S-max L~f <> SE-corner L~f holds mid(f,i,j)^<*SE-corner L~f*> is S-Sequence_in_R2 proof set p = SE-corner L~f; let i,j such that A1: i in dom f and A2: j in dom f and A3: mid(f,i,j) is S-Sequence_in_R2 and A4: f/.j = S-max L~f and A5: S-max L~f <> SE-corner L~f; A6: (mid(f,i,j))/.len mid(f,i,j) = S-max L~f by A1,A2,A4,Th13; then A7: p`2 = ((mid(f,i,j))/.len mid(f,i,j))`2 by PSCOMP_1:115; A8: LSeg(SE-corner L~f, S-max L~f)/\L~f = {S-max L~f} by PSCOMP_1:122; len mid(f,i,j) >= 2 by A3,TOPREAL1:def 10; then A9: S-max L~f in L~mid(f,i,j) by A6,JORDAN3:34; 1<=i & i<=len f & 1<=j & j<=len f by A1,A2,FINSEQ_3:27; then L~mid(f,i,j) c= L~f by JORDAN4:47; then LSeg(p, (mid(f,i,j))/.len mid(f,i,j)) /\ L~mid(f,i,j) = {(mid(f,i,j))/.len mid(f,i,j)} by A6,A8,A9,Th2; hence mid(f,i,j)^<*SE-corner L~f*> is S-Sequence_in_R2 by A3,A5,A6,A7,Th65; end; theorem Th69: for i,j st i in dom f & j in dom f & mid(f,i,j) is S-Sequence_in_R2 & f/.j = E-max L~f & E-max L~f <> NE-corner L~f holds mid(f,i,j)^<*NE-corner L~f*> is S-Sequence_in_R2 proof set p = NE-corner L~f; let i,j such that A1: i in dom f and A2: j in dom f and A3: mid(f,i,j) is S-Sequence_in_R2 and A4: f/.j = E-max L~f and A5: E-max L~f <> NE-corner L~f; A6: (mid(f,i,j))/.len mid(f,i,j) = E-max L~f by A1,A2,A4,Th13; then A7: p`1 = ((mid(f,i,j))/.len mid(f,i,j))`1 by PSCOMP_1:105; A8: LSeg(NE-corner L~f, E-max L~f)/\L~f = {E-max L~f} by PSCOMP_1:112; len mid(f,i,j) >= 2 by A3,TOPREAL1:def 10; then A9: E-max L~f in L~mid(f,i,j) by A6,JORDAN3:34; 1<=i & i<=len f & 1<=j & j<=len f by A1,A2,FINSEQ_3:27; then L~mid(f,i,j) c= L~f by JORDAN4:47; then LSeg(p, (mid(f,i,j))/.len mid(f,i,j)) /\ L~mid(f,i,j) = {(mid(f,i,j))/.len mid(f,i,j)} by A6,A8,A9,Th2; hence mid(f,i,j)^<*NE-corner L~f*> is S-Sequence_in_R2 by A3,A5,A6,A7,Th65; end; theorem Th70: for i,j st i in dom f & j in dom f & mid(f,i,j) is S-Sequence_in_R2 & f/.i = N-min L~f & N-min L~f <> NW-corner L~f holds <*NW-corner L~f*>^mid(f,i,j) is S-Sequence_in_R2 proof set p = NW-corner L~f; let i,j such that A1: i in dom f and A2: j in dom f and A3: mid(f,i,j) is S-Sequence_in_R2 and A4: f/.i = N-min L~f and A5: N-min L~f <> NW-corner L~f; A6: (mid(f,i,j))/.1 = N-min L~f by A1,A2,A4,Th12; then A7: p`2 = ((mid(f,i,j))/.1)`2 by PSCOMP_1:95; A8: LSeg(NW-corner L~f, N-min L~f)/\L~f = {N-min L~f} by PSCOMP_1:102; len mid(f,i,j) >= 2 by A3,TOPREAL1:def 10; then A9: N-min L~f in L~mid(f,i,j) by A6,JORDAN3:34; 1<=i & i<=len f & 1<=j & j<=len f by A1,A2,FINSEQ_3:27; then L~mid(f,i,j) c= L~f by JORDAN4:47; then LSeg(p, (mid(f,i,j))/.1) /\ L~mid(f,i,j) = {(mid(f,i,j))/.1} by A6,A8,A9,Th2; hence <*NW-corner L~f*>^mid(f,i,j) is S-Sequence_in_R2 by A3,A5,A6,A7,Th64; end; theorem Th71: for i,j st i in dom f & j in dom f & mid(f,i,j) is S-Sequence_in_R2 & f/.i = W-min L~f & W-min L~f <> SW-corner L~f holds <*SW-corner L~f*>^mid(f,i,j) is S-Sequence_in_R2 proof set p = SW-corner L~f; let i,j such that A1: i in dom f and A2: j in dom f and A3: mid(f,i,j) is S-Sequence_in_R2 and A4: f/.i = W-min L~f and A5: W-min L~f <> SW-corner L~f; A6: (mid(f,i,j))/.1 = W-min L~f by A1,A2,A4,Th12; then A7: p`1 = ((mid(f,i,j))/.1)`1 by PSCOMP_1:85; A8: LSeg(SW-corner L~f, W-min L~f)/\L~f = {W-min L~f} by PSCOMP_1:92; len mid(f,i,j) >= 2 by A3,TOPREAL1:def 10; then A9: W-min L~f in L~mid(f,i,j) by A6,JORDAN3:34; 1<=i & i<=len f & 1<=j & j<=len f by A1,A2,FINSEQ_3:27; then L~mid(f,i,j) c= L~f by JORDAN4:47; then LSeg(p, (mid(f,i,j))/.1) /\ L~mid(f,i,j) = {(mid(f,i,j))/.1} by A6,A8,A9,Th2; hence <*SW-corner L~f*>^mid(f,i,j) is S-Sequence_in_R2 by A3,A5,A6,A7,Th64; end; Lm3: for i,j st i in dom f & j in dom f & mid(f,i,j) is S-Sequence_in_R2 & f/.i = N-min L~f & N-min L~f <> NW-corner L~f & f/.j = N-max L~f & N-max L~f <> NE-corner L~f holds <*NW-corner L~f*>^mid(f,i,j)^<*NE-corner L~f*> is S-Sequence_in_R2 proof set p = NW-corner L~f, q = NE-corner L~f; let i,j such that A1: i in dom f and A2: j in dom f and A3: mid(f,i,j) is S-Sequence_in_R2 and A4: f/.i = N-min L~f and A5: N-min L~f <> NW-corner L~f and A6: f/.j = N-max L~f and A7: N-max L~f <> NE-corner L~f; set g = <*NW-corner L~f*>^mid(f,i,j); A8: g is S-Sequence_in_R2 by A1,A2,A3,A4,A5,Th70; A9: len g = len<*NW-corner L~f*> + len mid(f,i,j) by FINSEQ_1:35; len mid(f,i,j) in dom mid(f,i,j) by A3,FINSEQ_5:6; then A10: g/.len g = (mid(f,i,j))/.len mid(f,i,j) by A9,GROUP_5:96; then A11: g/.len g = N-max L~f by A1,A2,A6,Th13; then A12: q`2 = (g/.len g)`2 by PSCOMP_1:95; A13: LSeg(NE-corner L~f, N-max L~f)/\L~f = {N-max L~f} by PSCOMP_1:102; len mid(f,i,j) >= 2 by A3,TOPREAL1:def 10; then A14: N-max L~f in L~mid(f,i,j) by A10,A11,JORDAN3:34; 1<=i & i<=len f & 1<=j & j<=len f by A1,A2,FINSEQ_3:27; then A15: L~mid(f,i,j) c= L~f by JORDAN4:47; (mid(f,i,j))/.1 = f/.i by A1,A2,Th12; then A16: L~g = LSeg(p,N-min L~f) \/ L~mid(f,i,j) by A3,A4,SPPOL_2:20; LSeg(g/.len g,q) misses LSeg(p,N-min L~f) by A11,Th63; then LSeg(q, g/.len g) /\ LSeg(p,N-min L~f) = {} by XBOOLE_0:def 7; then LSeg(q, g/.len g) /\ L~g = LSeg(q, g/.len g) /\ L~mid(f,i,j) \/ {} by A16,XBOOLE_1:23 .= {g/.len g} by A11,A13,A14,A15,Th2; hence <*NW-corner L~f*>^mid(f,i,j)^<*NE-corner L~f*> is S-Sequence_in_R2 by A7,A8,A11,A12,Th65; end; definition let f be non constant standard special_circular_sequence; cluster L~f -> being_simple_closed_curve; coherence by JORDAN4:63; end; Lm4: LSeg(S-max L~f,SE-corner L~f) misses LSeg(NW-corner L~f,N-min L~f) proof assume LSeg(S-max L~f,SE-corner L~f) meets LSeg(NW-corner L~f,N-min L~f); then LSeg(S-max L~f,SE-corner L~f) /\ LSeg(NW-corner L~f,N-min L~f) <> {} by XBOOLE_0:def 7; then consider x being set such that A1: x in LSeg(S-max L~f,SE-corner L~f) /\ LSeg(NW-corner L~f,N-min L~f) by XBOOLE_0:def 1; A2: x in LSeg(S-max L~f,SE-corner L~f) by A1,XBOOLE_0:def 3; reconsider p = x as Point of TOP-REAL 2 by A1; A3: p in LSeg(NW-corner L~f,N-min L~f) by A1,XBOOLE_0:def 3; (NW-corner L~f)`2 = N-bound L~f & (N-min L~f)`2 = N-bound L~f by PSCOMP_1:75,94; then N-bound L~f <= p`2 & p`2 <= N-bound L~f by A3,TOPREAL1:10; then A4: p`2 = N-bound L~f by AXIOMS:21; (SE-corner L~f)`2 = S-bound L~f & (S-max L~f)`2 = S-bound L~f by PSCOMP_1:79,114 ; then S-bound L~f <= p`2 & p`2 <= S-bound L~f by A2,TOPREAL1:10; hence contradiction by A4,TOPREAL5:22; end; Lm5: for i,j st i in dom f & j in dom f & mid(f,i,j) is S-Sequence_in_R2 & f/.i = N-min L~f & N-min L~f <> NW-corner L~f & f/.j = S-max L~f & S-max L~f <> SE-corner L~f holds <*NW-corner L~f*>^mid(f,i,j)^<*SE-corner L~f*> is S-Sequence_in_R2 proof set p = NW-corner L~f, q = SE-corner L~f; let i,j such that A1: i in dom f and A2: j in dom f and A3: mid(f,i,j) is S-Sequence_in_R2 and A4: f/.i = N-min L~f and A5: N-min L~f <> NW-corner L~f and A6: f/.j = S-max L~f and A7: S-max L~f <> SE-corner L~f; set g = <*NW-corner L~f*>^mid(f,i,j); A8: g is S-Sequence_in_R2 by A1,A2,A3,A4,A5,Th70; A9: len g = len<*NW-corner L~f*> + len mid(f,i,j) by FINSEQ_1:35; len mid(f,i,j) in dom mid(f,i,j) by A3,FINSEQ_5:6; then A10: g/.len g = (mid(f,i,j))/.len mid(f,i,j) by A9,GROUP_5:96; then A11: g/.len g = S-max L~f by A1,A2,A6,Th13; then A12: q`2 = (g/.len g)`2 by PSCOMP_1:115; A13: LSeg(SE-corner L~f, S-max L~f)/\L~f = {S-max L~f} by PSCOMP_1:122; len mid(f,i,j) >= 2 by A3,TOPREAL1:def 10; then A14: S-max L~f in L~mid(f,i,j) by A10,A11,JORDAN3:34; 1<=i & i<=len f & 1<=j & j<=len f by A1,A2,FINSEQ_3:27; then A15: L~mid(f,i,j) c= L~f by JORDAN4:47; (mid(f,i,j))/.1 = f/.i by A1,A2,Th12; then A16: L~g = LSeg(p,N-min L~f) \/ L~mid(f,i,j) by A3,A4,SPPOL_2:20; LSeg(g/.len g,q) misses LSeg(p,N-min L~f) by A11,Lm4; then LSeg(q, g/.len g) /\ LSeg(p,N-min L~f) = {} by XBOOLE_0:def 7; then LSeg(q, g/.len g) /\ L~g = LSeg(q, g/.len g) /\ L~mid(f,i,j) \/ {} by A16,XBOOLE_1:23 .= {g/.len g} by A11,A13,A14,A15,Th2; hence <*NW-corner L~f*>^mid(f,i,j)^<*SE-corner L~f*> is S-Sequence_in_R2 by A7,A8,A11,A12,Th65; end; begin :: The order theorem Th72: f/.1 = N-min L~f implies (N-min L~f)..f < (N-max L~f)..f proof A1: N-min L~f in rng f by Th43; A2: N-max L~f in rng f by Th44; N-min L~f <> N-max L~f by Th56; then A3: (N-min L~f)..f <> (N-max L~f)..f by A1,A2,FINSEQ_5:10; (N-max L~f)..f in dom f by A2,FINSEQ_4:30; then A4: (N-max L~f)..f >= 1 by FINSEQ_3:27; assume f/.1 = N-min L~f; then (N-min L~f)..f = 1 by FINSEQ_6:47; hence (N-min L~f)..f < (N-max L~f)..f by A3,A4,REAL_1:def 5; end; theorem f/.1 = N-min L~f implies (N-max L~f)..f > 1 proof assume A1: f/.1 = N-min L~f; then (N-min L~f)..f = 1 by FINSEQ_6:47; hence thesis by A1,Th72; end; Lm6: f/.1 = N-min L~f implies (N-min L~f)..f < (E-max L~f)..f proof A1: E-max L~f in rng f by Th50; A2: N-min L~f in rng f by Th43; A3: (N-min L~f)`1 < (N-max L~f)`1 by Th55; (N-max L~f)`1 <= (NE-corner L~f)`1 by PSCOMP_1:97; then (N-max L~f)`1 <= E-bound L~f by PSCOMP_1:76; then (N-min L~f)`1 < E-bound L~f by A3,AXIOMS:22; then (N-min L~f)`1 < (E-max L~f)`1 by PSCOMP_1:104; then A4: (N-min L~f)..f <> (E-max L~f)..f by A1,A2,FINSEQ_5:10; assume f/.1 = N-min L~f; then A5: (N-min L~f)..f = 1 by FINSEQ_6:47; (E-max L~f)..f >= 1 by A1,FINSEQ_4:31; hence (N-min L~f)..f < (E-max L~f)..f by A4,A5,REAL_1:def 5; end; reserve z for clockwise_oriented (non constant standard special_circular_sequence); Lm7: z/.1 = N-min L~z implies (N-max L~z)..z < (S-max L~z)..z proof set i1 = (N-max L~z)..z, i2 = (S-max L~z)..z; assume that A1: z/.1 = N-min L~z and A2: i1 >= i2; A3: N-max L~z in rng z by Th44; A4: S-max L~z in rng z by Th46; A5: i1 in dom z by A3,FINSEQ_4:30; then A6: 1 <= i1 & i1 <= len z by FINSEQ_3:27; A7: i2 in dom z by A4,FINSEQ_4:30; then A8: 1 <= i2 & i2 <= len z by FINSEQ_3:27; A9: z/.i2 = z.i2 by A7,FINSEQ_4:def 4 .= S-max L~z by A4,FINSEQ_4:29; A10: z/.len z = N-min L~z by A1,FINSEQ_6:def 1; A11: z/.i1 = z.i1 by A5,FINSEQ_4:def 4 .= N-max L~z by A3,FINSEQ_4:29; (N-max L~z)`2 = N-bound L~z & (S-max L~z)`2 = S-bound L~z by PSCOMP_1:94,114; then z/.i1 <> z/.i2 by A9,A11,TOPREAL5:22; then A12: i1 > i2 by A2,REAL_1:def 5; then A13: i1 > 1 by A8,AXIOMS:22; A14: len z in dom z by FINSEQ_5:6; A15: z/.1 = z/.len z by FINSEQ_6:def 1; A16: 2 <= len z by SPPOL_1:2; then A17: 2 in dom z by FINSEQ_3:27; z/.2 in N-most L~z by A1,Th34; then A18: (z/.2)`2 = (N-min L~z)`2 by PSCOMP_1:98 .= N-bound L~z by PSCOMP_1:94; A19: (z/.1)`2 = N-bound L~z by A1,PSCOMP_1:94; A20: i2 <> 0 by A7,FINSEQ_3:27; (z/.i2)`2 = S-bound L~z by A9,PSCOMP_1:114; then i2 <> 1 & i2 <> 2 by A18,A19,TOPREAL5:22; then A21: i2 > 2 by A20,CQC_THE1:3; then reconsider h = mid(z,i2,2) as S-Sequence_in_R2 by A8,Th41; A22: h is_in_the_area_of z by A7,A17,Th27; h/.1 = S-max L~z by A7,A9,A17,Th12; then A23: (h/.1)`2 = S-bound L~z by PSCOMP_1:114; A24: L~h c= L~z by A8,A16,JORDAN4:47; (h/.len h)`2 = N-bound L~z by A7,A17,A18,Th13; then A25: h is_a_v.c._for z by A22,A23,Def3; N-min L~z <> N-max L~z by Th56; then A26: i1 < len z by A6,A10,A11,REAL_1:def 5; then reconsider M = mid(z,len z,i1) as S-Sequence_in_R2 by A13,Th41; A27: L~M misses L~h by A6,A12,A21,Th53; A28: M/.len M = z/.i1 by A5,A14,Th13 .= N-max L~z by A3,FINSEQ_5:41; A29: len M = len z -' i1 + 1 by A6,JORDAN4:21; i1 + 1 <= len z by A26,NAT_1:38; then len z - i1 >= 1 by REAL_1:84; then len z -' i1 >= 1 by JORDAN3:1; then A30: len z -' i1 + 1 >= 1+1 by AXIOMS:24; then A31: M/.len M in L~M by A29,JORDAN3:34; A32: 2 <= len h by TOPREAL1:def 10; A33: 1 in dom M by FINSEQ_5:6; A34: M/.1 = z/.1 by A5,A14,A15,Th12; per cases; suppose that A35: NW-corner L~z = N-min L~z and A36: NE-corner L~z = N-max L~z; A37: M is_in_the_area_of z by A5,A14,Th27; M/.1 = z/.len z by A5,A14,Th12; then A38: (M/.1)`1 = W-bound L~z by A1,A15,A35,PSCOMP_1:74; (M/.len M)`1 = E-bound L~z by A28,A36,PSCOMP_1:76; then M is_a_h.c._for z by A37,A38,Def2; hence contradiction by A25,A27,A29,A30,A32,Th33; suppose that A39: NW-corner L~z = N-min L~z and A40: NE-corner L~z <> N-max L~z; reconsider g = M^<*NE-corner L~z*> as S-Sequence_in_R2 by A5,A11,A14,A40,Th66; A41: len g >= 2 by TOPREAL1:def 10; A42: M is_in_the_area_of z by A5,A14,Th27; <*NE-corner L~z*> is_in_the_area_of z by Th29; then A43: g is_in_the_area_of z by A42,Th28; g/.1 = M/.1 by A33,GROUP_5:95 .= z/.1 by A5,A14,A15,Th12; then A44: (g/.1)`1 = W-bound L~z by A1,A39,PSCOMP_1:74; len g = len M + len<*NE-corner L~z*> by FINSEQ_1:35 .= len M + 1 by FINSEQ_1:56; then g/.len g = NE-corner L~z by TOPREAL4:1; then (g/.len g)`1 = E-bound L~z by PSCOMP_1:76; then A45: g is_a_h.c._for z by A43,A44,Def2; A46: L~g = L~M \/ LSeg(M/.len M,NE-corner L~z) by SPPOL_2:19; LSeg(M/.len M,NE-corner L~z) /\ L~h c= LSeg(M/.len M,NE-corner L~z) /\ L~z by A24,XBOOLE_1:26; then LSeg(M/.len M,NE-corner L~z) /\ L~h c= {M/.len M} by A28,PSCOMP_1:102; then L~g misses L~h by A27,A31,A46,Th1; hence contradiction by A25,A32,A41,A45,Th33; suppose that A47: NW-corner L~z <> N-min L~z and A48: NE-corner L~z = N-max L~z; reconsider g = <*NW-corner L~z*>^M as S-Sequence_in_R2 by A1,A5,A14,A15,A47,Th70; A49: len g >= 2 by TOPREAL1:def 10; A50: M is_in_the_area_of z by A5,A14,Th27; <*NW-corner L~z*> is_in_the_area_of z by Th30; then A51: g is_in_the_area_of z by A50,Th28; g/.1 = NW-corner L~z by FINSEQ_5:16; then A52: (g/.1)`1 = W-bound L~z by PSCOMP_1:74; A53: len M in dom M by FINSEQ_5:6; len g = len M + len<*NW-corner L~z*> by FINSEQ_1:35; then g/.len g = M/.len M by A53,GROUP_5:96 .= z/.i1 by A5,A14,Th13 .= N-max L~z by A3,FINSEQ_5:41; then (g/.len g)`1 = E-bound L~z by A48,PSCOMP_1:76; then A54: g is_a_h.c._for z by A51,A52,Def2; A55: L~g = L~M \/ LSeg(NW-corner L~z,M/.1) by SPPOL_2:20; LSeg(M/.1,NW-corner L~z) /\ L~h c= LSeg(M/.1,NW-corner L~z) /\ L~z by A24,XBOOLE_1:26; then A56: LSeg(M/.1,NW-corner L~z) /\ L~h c= {M/.1} by A1,A34,PSCOMP_1:102; M/.1 in L~M by A29,A30,JORDAN3:34; then L~g misses L~h by A27,A55,A56,Th1; hence contradiction by A25,A32,A49,A54,Th33; suppose that A57: NW-corner L~z <> N-min L~z and A58: NE-corner L~z <> N-max L~z; set K = <*NW-corner L~z*>^M; reconsider g = K^<*NE-corner L~z*> as S-Sequence_in_R2 by A1,A5,A11,A14,A15,A57,A58,Lm3; A59: len g >= 2 by TOPREAL1:def 10; A60: M is_in_the_area_of z by A5,A14,Th27; <*NW-corner L~z*> is_in_the_area_of z by Th30; then A61: <*NW-corner L~z*>^M is_in_the_area_of z by A60,Th28; <*NE-corner L~z*> is_in_the_area_of z by Th29; then A62: g is_in_the_area_of z by A61,Th28; 1 in dom(<*NW-corner L~z*>^M) by FINSEQ_5:6; then g/.1 = (<*NW-corner L~z*>^M)/.1 by GROUP_5:95 .= NW-corner L~z by FINSEQ_5:16; then A63: (g/.1)`1 = W-bound L~z by PSCOMP_1:74; len g = len(<*NW-corner L~z*>^M) + len<*NE-corner L~z*> by FINSEQ_1:35 .= len(<*NW-corner L~z*>^M) + 1 by FINSEQ_1:56; then g/.len g = NE-corner L~z by TOPREAL4:1; then (g/.len g)`1 = E-bound L~z by PSCOMP_1:76; then A64: g is_a_h.c._for z by A62,A63,Def2; A65: L~K = L~M \/ LSeg(NW-corner L~z,M/.1) by SPPOL_2:20; LSeg(M/.1,NW-corner L~z) /\ L~h c= LSeg(M/.1,NW-corner L~z) /\ L~z by A24,XBOOLE_1:26; then A66: LSeg(M/.1,NW-corner L~z) /\ L~h c= {M/.1} by A1,A34,PSCOMP_1:102; M/.1 in L~M by A29,A30,JORDAN3:34; then A67: L~K misses L~h by A27,A65,A66,Th1; len K = len M + len<*NW-corner L~z*> by FINSEQ_1:35; then len K >= len M by NAT_1:29; then len K >= 2 by A29,A30,AXIOMS:22; then A68: K/.len K in L~K by JORDAN3:34; A69: L~g = L~K \/ LSeg(K/.len K,NE-corner L~z) by SPPOL_2:19; A70: len M in dom M by FINSEQ_5:6; len K = len M + len<*NW-corner L~z*> by FINSEQ_1:35; then A71: K/.len K = M/.len M by A70,GROUP_5:96 .= z/.i1 by A5,A14,Th13 .= N-max L~z by A3,FINSEQ_5:41; LSeg(K/.len K,NE-corner L~z) /\ L~h c= LSeg(K/.len K,NE-corner L~z) /\ L~z by A24,XBOOLE_1:26; then LSeg(K/.len K,NE-corner L~z) /\ L~h c= {K/.len K} by A71,PSCOMP_1:102; then L~g misses L~h by A67,A68,A69,Th1; hence contradiction by A25,A32,A59,A64,Th33; end; Lm8: z/.1 = N-min L~z implies (N-max L~z)..z < (S-min L~z)..z proof set i1 = (N-max L~z)..z, i2 = (S-min L~z)..z; assume that A1: z/.1 = N-min L~z and A2: i1 >= i2; A3: N-max L~z in rng z by Th44; A4: S-min L~z in rng z by Th45; A5: i1 in dom z by A3,FINSEQ_4:30; then A6: 1 <= i1 & i1 <= len z by FINSEQ_3:27; A7: i2 in dom z by A4,FINSEQ_4:30; then A8: 1 <= i2 & i2 <= len z by FINSEQ_3:27; A9: z/.i2 = z.i2 by A7,FINSEQ_4:def 4 .= S-min L~z by A4,FINSEQ_4:29; A10: z/.len z = N-min L~z by A1,FINSEQ_6:def 1; A11: z/.i1 = z.i1 by A5,FINSEQ_4:def 4 .= N-max L~z by A3,FINSEQ_4:29; (N-max L~z)`2 = N-bound L~z & (S-min L~z)`2 = S-bound L~z by PSCOMP_1:94,114; then z/.i1 <> z/.i2 by A9,A11,TOPREAL5:22; then A12: i1 > i2 by A2,REAL_1:def 5; then A13: i1 > 1 by A8,AXIOMS:22; A14: len z in dom z by FINSEQ_5:6; A15: z/.1 = z/.len z by FINSEQ_6:def 1; A16: 2 <= len z by SPPOL_1:2; then A17: 2 in dom z by FINSEQ_3:27; z/.2 in N-most L~z by A1,Th34; then A18: (z/.2)`2 = (N-min L~z)`2 by PSCOMP_1:98 .= N-bound L~z by PSCOMP_1:94; A19: (z/.1)`2 = N-bound L~z by A1,PSCOMP_1:94; A20: i2 <> 0 by A7,FINSEQ_3:27; A21: (z/.i2)`2 = S-bound L~z by A9,PSCOMP_1:114; S-bound L~z < N-bound L~z by TOPREAL5:22; then A22: i2 > 2 by A18,A19,A20,A21,CQC_THE1:3; then reconsider h = mid(z,i2,2) as S-Sequence_in_R2 by A8,Th41; A23: len h >= 2 by TOPREAL1:def 10; A24: h is_in_the_area_of z by A7,A17,Th27; h/.1 = S-min L~z by A7,A9,A17,Th12; then A25: (h/.1)`2 = S-bound L~z by PSCOMP_1:114; A26: L~h c= L~z by A8,A16,JORDAN4:47; h/.len h = z/.2 by A7,A17,Th13; then A27: h is_a_v.c._for z by A18,A24,A25,Def3; N-min L~z <> N-max L~z by Th56; then A28: i1 < len z by A6,A10,A11,REAL_1:def 5; then reconsider M = mid(z,len z,i1) as S-Sequence_in_R2 by A13,Th41; A29: L~M misses L~h by A6,A12,A22,Th53; A30: M/.len M = z/.i1 by A5,A14,Th13 .= N-max L~z by A3,FINSEQ_5:41; A31: len M = len z -' i1 + 1 by A6,JORDAN4:21; i1 + 1 <= len z by A28,NAT_1:38; then len z - i1 >= 1 by REAL_1:84; then len z -' i1 >= 1 by JORDAN3:1; then A32: len z -' i1 + 1 >= 1+1 by AXIOMS:24; then A33: M/.len M in L~M by A31,JORDAN3:34; A34: 1 in dom M by FINSEQ_5:6; A35: M/.1 = z/.1 by A5,A14,A15,Th12; per cases; suppose that A36: NW-corner L~z = N-min L~z and A37: NE-corner L~z = N-max L~z; A38: M is_in_the_area_of z by A5,A14,Th27; M/.1 = z/.len z by A5,A14,Th12; then A39: (M/.1)`1 = W-bound L~z by A1,A15,A36,PSCOMP_1:74; (M/.len M)`1 = E-bound L~z by A30,A37,PSCOMP_1:76; then M is_a_h.c._for z by A38,A39,Def2; hence contradiction by A23,A27,A29,A31,A32,Th33; suppose that A40: NW-corner L~z = N-min L~z and A41: NE-corner L~z <> N-max L~z; reconsider g = M^<*NE-corner L~z*> as S-Sequence_in_R2 by A5,A11,A14,A41,Th66; A42: len g >= 2 by TOPREAL1:def 10; A43: M is_in_the_area_of z by A5,A14,Th27; <*NE-corner L~z*> is_in_the_area_of z by Th29; then A44: g is_in_the_area_of z by A43,Th28; g/.1 = M/.1 by A34,GROUP_5:95 .= z/.1 by A5,A14,A15,Th12; then A45: (g/.1)`1 = W-bound L~z by A1,A40,PSCOMP_1:74; len g = len M + len<*NE-corner L~z*> by FINSEQ_1:35 .= len M + 1 by FINSEQ_1:56; then g/.len g = NE-corner L~z by TOPREAL4:1; then (g/.len g)`1 = E-bound L~z by PSCOMP_1:76; then A46: g is_a_h.c._for z by A44,A45,Def2; A47: L~g = L~M \/ LSeg(M/.len M,NE-corner L~z) by SPPOL_2:19; LSeg(M/.len M,NE-corner L~z) /\ L~h c= LSeg(M/.len M,NE-corner L~z) /\ L~z by A26,XBOOLE_1:26; then LSeg(M/.len M,NE-corner L~z) /\ L~h c= {M/.len M} by A30,PSCOMP_1:102; then L~g misses L~h by A29,A33,A47,Th1; hence contradiction by A23,A27,A42,A46,Th33; suppose that A48: NW-corner L~z <> N-min L~z and A49: NE-corner L~z = N-max L~z; reconsider g = <*NW-corner L~z*>^M as S-Sequence_in_R2 by A1,A5,A14,A15,A48,Th70; A50: len g >= 2 by TOPREAL1:def 10; A51: M is_in_the_area_of z by A5,A14,Th27; <*NW-corner L~z*> is_in_the_area_of z by Th30; then A52: g is_in_the_area_of z by A51,Th28; g/.1 = NW-corner L~z by FINSEQ_5:16; then A53: (g/.1)`1 = W-bound L~z by PSCOMP_1:74; A54: len M in dom M by FINSEQ_5:6; len g = len M + len<*NW-corner L~z*> by FINSEQ_1:35; then g/.len g = M/.len M by A54,GROUP_5:96 .= z/.i1 by A5,A14,Th13 .= N-max L~z by A3,FINSEQ_5:41; then (g/.len g)`1 = E-bound L~z by A49,PSCOMP_1:76; then A55: g is_a_h.c._for z by A52,A53,Def2; A56: L~g = L~M \/ LSeg(NW-corner L~z,M/.1) by SPPOL_2:20; LSeg(M/.1,NW-corner L~z) /\ L~h c= LSeg(M/.1,NW-corner L~z) /\ L~z by A26,XBOOLE_1:26; then A57: LSeg(M/.1,NW-corner L~z) /\ L~h c= {M/.1} by A1,A35,PSCOMP_1:102; M/.1 in L~M by A31,A32,JORDAN3:34; then L~g misses L~h by A29,A56,A57,Th1; hence contradiction by A23,A27,A50,A55,Th33; suppose that A58: NW-corner L~z <> N-min L~z and A59: NE-corner L~z <> N-max L~z; set K = <*NW-corner L~z*>^M; reconsider g = K^<*NE-corner L~z*> as S-Sequence_in_R2 by A1,A5,A11,A14,A15,A58,A59,Lm3; A60: len g >= 2 by TOPREAL1:def 10; A61: M is_in_the_area_of z by A5,A14,Th27; <*NW-corner L~z*> is_in_the_area_of z by Th30; then A62: <*NW-corner L~z*>^M is_in_the_area_of z by A61,Th28; <*NE-corner L~z*> is_in_the_area_of z by Th29; then A63: g is_in_the_area_of z by A62,Th28; 1 in dom(<*NW-corner L~z*>^M) by FINSEQ_5:6; then g/.1 = (<*NW-corner L~z*>^M)/.1 by GROUP_5:95 .= NW-corner L~z by FINSEQ_5:16; then A64: (g/.1)`1 = W-bound L~z by PSCOMP_1:74; len g = len(<*NW-corner L~z*>^M) + len<*NE-corner L~z*> by FINSEQ_1:35 .= len(<*NW-corner L~z*>^M) + 1 by FINSEQ_1:56; then g/.len g = NE-corner L~z by TOPREAL4:1; then (g/.len g)`1 = E-bound L~z by PSCOMP_1:76; then A65: g is_a_h.c._for z by A63,A64,Def2; A66: L~K = L~M \/ LSeg(NW-corner L~z,M/.1) by SPPOL_2:20; LSeg(M/.1,NW-corner L~z) /\ L~h c= LSeg(M/.1,NW-corner L~z) /\ L~z by A26,XBOOLE_1:26; then A67: LSeg(M/.1,NW-corner L~z) /\ L~h c= {M/.1} by A1,A35,PSCOMP_1:102; M/.1 in L~M by A31,A32,JORDAN3:34; then A68: L~K misses L~h by A29,A66,A67,Th1; len K = len M + len<*NW-corner L~z*> by FINSEQ_1:35; then len K >= len M by NAT_1:29; then len K >= 2 by A31,A32,AXIOMS:22; then A69: K/.len K in L~K by JORDAN3:34; A70: L~g = L~K \/ LSeg(K/.len K,NE-corner L~z) by SPPOL_2:19; A71: len M in dom M by FINSEQ_5:6; len K = len M + len<*NW-corner L~z*> by FINSEQ_1:35; then A72: K/.len K = M/.len M by A71,GROUP_5:96 .= z/.i1 by A5,A14,Th13 .= N-max L~z by A3,FINSEQ_5:41; LSeg(K/.len K,NE-corner L~z) /\ L~h c= LSeg(K/.len K,NE-corner L~z) /\ L~z by A26,XBOOLE_1:26; then LSeg(K/.len K,NE-corner L~z) /\ L~h c= {K/.len K} by A72,PSCOMP_1:102; then L~g misses L~h by A68,A69,A70,Th1; hence contradiction by A23,A27,A60,A65,Th33; end; theorem z/.1 = N-min L~z & N-max L~z <> E-max L~z implies (N-max L~z)..z < (E-max L~z)..z proof set i1 = (N-max L~z)..z, i2 = (E-max L~z)..z, j = (S-max L~z)..z; assume that A1: z/.1 = N-min L~z and A2: N-max L~z <> E-max L~z and A3: i1 >= i2; A4: E-max L~z in rng z by Th50; A5: S-max L~z in rng z by Th46; A6: N-max L~z in rng z by Th44; A7: 1 in dom z by FINSEQ_5:6; A8: i1 in dom z by A6,FINSEQ_4:30; then A9: 1 <= i1 & i1 <= len z by FINSEQ_3:27; A10: j in dom z by A5,FINSEQ_4:30; then A11: 1 <= j & j <= len z by FINSEQ_3:27; A12: z/.j = z.j by A10,FINSEQ_4:def 4 .= S-max L~z by A5,FINSEQ_4:29; A13: i2 in dom z by A4,FINSEQ_4:30; then A14: 1 <= i2 & i2 <= len z by FINSEQ_3:27; A15: z/.i1 = z.i1 by A8,FINSEQ_4:def 4 .= N-max L~z by A6,FINSEQ_4:29; A16: j > i1 by A1,Lm7; (N-min L~z)`2 = N-bound L~z & (S-max L~z)`2 = S-bound L~z by PSCOMP_1:94,114; then A17: N-min L~z <> S-max L~z by TOPREAL5:22; z/.len z = z/.1 by FINSEQ_6:def 1; then A18: j < len z by A1,A11,A12,A17,REAL_1:def 5; then reconsider h = mid(z,j,i1) as S-Sequence_in_R2 by A9,A16,Th41; A19: h is_in_the_area_of z by A8,A10,Th27; h/.1 = S-max L~z by A8,A10,A12,Th12; then A20: (h/.1)`2 = S-bound L~z by PSCOMP_1:114; A21: L~h c= L~z by A9,A11,JORDAN4:47; h/.len h = z/.i1 by A8,A10,Th13; then (h/.len h)`2 = N-bound L~z by A15,PSCOMP_1:94; then A22: h is_a_v.c._for z by A19,A20,Def3; (N-min L~z)..z = 1 by A1,FINSEQ_6:47; then A23: 1 < i2 by A1,Lm6; z/.i2 = z.i2 by A13,FINSEQ_4:def 4 .= E-max L~z by A4,FINSEQ_4:29; then A24: i1 > i2 by A2,A3,A15,REAL_1:def 5; then i2 < len z by A9,AXIOMS:22; then reconsider M = mid(z,1,i2) as S-Sequence_in_R2 by A23,Th42; A25: len M >= 2 & len h >= 2 by TOPREAL1:def 10; A26: L~M misses L~h by A16,A18,A23,A24,Th52; A27: M/.len M = z/.i2 by A7,A13,Th13 .= E-max L~z by A4,FINSEQ_5:41; per cases; suppose A28: NW-corner L~z = N-min L~z; A29: M is_in_the_area_of z by A7,A13,Th27; M/.1 = z/.1 by A7,A13,Th12; then A30: (M/.1)`1 = W-bound L~z by A1,A28,PSCOMP_1:74; (M/.len M)`1 = E-bound L~z by A27,PSCOMP_1:104; then M is_a_h.c._for z by A29,A30,Def2; hence contradiction by A22,A25,A26,Th33; suppose NW-corner L~z <> N-min L~z; then reconsider g = <*NW-corner L~z*>^M as S-Sequence_in_R2 by A1,A7,A13,Th70; A31: len g >= 2 by TOPREAL1:def 10; A32: M is_in_the_area_of z by A7,A13,Th27; <*NW-corner L~z*> is_in_the_area_of z by Th30; then A33: g is_in_the_area_of z by A32,Th28; g/.1 = NW-corner L~z by FINSEQ_5:16; then A34: (g/.1)`1 = W-bound L~z by PSCOMP_1:74; A35: len M in dom M by FINSEQ_5:6; len g = len M + len<*NW-corner L~z*> by FINSEQ_1:35; then g/.len g = M/.len M by A35,GROUP_5:96 .= z/.i2 by A7,A13,Th13 .= E-max L~z by A4,FINSEQ_5:41; then (g/.len g)`1 = E-bound L~z by PSCOMP_1:104; then A36: g is_a_h.c._for z by A33,A34,Def2; A37: L~g = L~M \/ LSeg(NW-corner L~z,M/.1) by SPPOL_2:20; A38: M/.1 = z/.1 by A7,A13,Th12; len M = i2 -' 1 + 1 by A14,JORDAN4:20 .= i2 by A23,AMI_5:4; then A39: len M >= 1+1 by A23,NAT_1:38; LSeg(M/.1,NW-corner L~z) /\ L~h c= LSeg(M/.1,NW-corner L~z) /\ L~z by A21,XBOOLE_1:26; then A40: LSeg(M/.1,NW-corner L~z) /\ L~h c= {M/.1} by A1,A38,PSCOMP_1:102; M/.1 in L~M by A39,JORDAN3:34; then L~g misses L~h by A26,A37,A40,Th1; hence contradiction by A22,A25,A31,A36,Th33; end; Lm9: z/.1 = N-min L~z implies (E-max L~z)..z < (S-max L~z)..z proof set i1 = (E-max L~z)..z, i2 = (S-max L~z)..z; assume that A1: z/.1 = N-min L~z and A2: i1 >= i2; A3: E-max L~z in rng z by Th50; A4: S-max L~z in rng z by Th46; A5: i1 in dom z by A3,FINSEQ_4:30; then A6: 1 <= i1 & i1 <= len z by FINSEQ_3:27; A7: i2 in dom z by A4,FINSEQ_4:30; then A8: 1 <= i2 & i2 <= len z by FINSEQ_3:27; A9: z/.i2 = z.i2 by A7,FINSEQ_4:def 4 .= S-max L~z by A4,FINSEQ_4:29; A10: z/.len z = N-min L~z by A1,FINSEQ_6:def 1; A11: z/.i1 = z.i1 by A5,FINSEQ_4:def 4 .= E-max L~z by A3,FINSEQ_4:29; A12:(E-min L~z)`2 < (E-max L~z)`2 by Th57; E-min L~z in L~z by SPRECT_1:16; then S-bound L~z <= (E-min L~z)`2 by PSCOMP_1:71; then E-max L~z <> S-max L~z by A12,PSCOMP_1:114; then A13: i1 > i2 by A2,A9,A11,REAL_1:def 5; then A14: i1 > 1 by A8,AXIOMS:22; A15: len z in dom z by FINSEQ_5:6; A16: z/.1 = z/.len z by FINSEQ_6:def 1; A17: 2 <= len z by SPPOL_1:2; then A18: 2 in dom z by FINSEQ_3:27; z/.2 in N-most L~z by A1,Th34; then A19: (z/.2)`2 = (N-min L~z)`2 by PSCOMP_1:98 .= N-bound L~z by PSCOMP_1:94; A20: (z/.1)`2 = N-bound L~z by A1,PSCOMP_1:94; A21: i2 <> 0 by A7,FINSEQ_3:27; A22: (z/.i2)`2 = S-bound L~z by A9,PSCOMP_1:114; S-bound L~z < N-bound L~z by TOPREAL5:22; then A23: i2 > 2 by A19,A20,A21,A22,CQC_THE1:3; then reconsider h = mid(z,i2,2) as S-Sequence_in_R2 by A8,Th41; A24: len h >= 2 by TOPREAL1:def 10; A25: h is_in_the_area_of z by A7,A18,Th27; h/.1 = S-max L~z by A7,A9,A18,Th12; then A26: (h/.1)`2 = S-bound L~z by PSCOMP_1:114; A27: L~h c= L~z by A8,A17,JORDAN4:47; h/.len h = z/.2 by A7,A18,Th13; then A28: h is_a_v.c._for z by A19,A25,A26,Def3; A29: (N-min L~z)`1 < (N-max L~z)`1 by Th55; N-max L~z in L~z by SPRECT_1:13; then (N-max L~z)`1 <= E-bound L~z by PSCOMP_1:71; then i1 <> len z by A10,A11,A29,PSCOMP_1:104; then A30: i1 < len z by A6,REAL_1:def 5; then reconsider M = mid(z,len z,i1) as S-Sequence_in_R2 by A14,Th41; A31: len M >= 2 by TOPREAL1:def 10; A32: L~M misses L~h by A6,A13,A23,Th53; A33: M/.len M = z/.i1 by A5,A15,Th13 .= E-max L~z by A3,FINSEQ_5:41; A34: len M = len z -' i1 + 1 by A6,JORDAN4:21; i1 + 1 <= len z by A30,NAT_1:38; then len z - i1 >= 1 by REAL_1:84; then len z -' i1 >= 1 by JORDAN3:1; then A35: len z -' i1 + 1 >= 1+1 by AXIOMS:24; A36: M/.1 = z/.1 by A5,A15,A16,Th12; per cases; suppose that A37: NW-corner L~z = N-min L~z; A38: M is_in_the_area_of z by A5,A15,Th27; M/.1 = z/.len z by A5,A15,Th12; then A39: (M/.1)`1 = W-bound L~z by A1,A16,A37,PSCOMP_1:74; (M/.len M)`1 = E-bound L~z by A33,PSCOMP_1:104; then M is_a_h.c._for z by A38,A39,Def2; hence contradiction by A24,A28,A31,A32,Th33; suppose NW-corner L~z <> N-min L~z; then reconsider g = <*NW-corner L~z*>^M as S-Sequence_in_R2 by A1,A5,A15,A16,Th70; A40: len g >= 2 by TOPREAL1:def 10; A41: M is_in_the_area_of z by A5,A15,Th27; <*NW-corner L~z*> is_in_the_area_of z by Th30; then A42: g is_in_the_area_of z by A41,Th28; g/.1 = NW-corner L~z by FINSEQ_5:16; then A43: (g/.1)`1 = W-bound L~z by PSCOMP_1:74; A44: len M in dom M by FINSEQ_5:6; len g = len M + len<*NW-corner L~z*> by FINSEQ_1:35; then g/.len g = M/.len M by A44,GROUP_5:96 .= z/.i1 by A5,A15,Th13 .= E-max L~z by A3,FINSEQ_5:41; then (g/.len g)`1 = E-bound L~z by PSCOMP_1:104; then A45: g is_a_h.c._for z by A42,A43,Def2; A46: L~g = L~M \/ LSeg(NW-corner L~z,M/.1) by SPPOL_2:20; LSeg(M/.1,NW-corner L~z) /\ L~h c= LSeg(M/.1,NW-corner L~z) /\ L~z by A27,XBOOLE_1:26; then A47: LSeg(M/.1,NW-corner L~z) /\ L~h c= {M/.1} by A1,A36,PSCOMP_1:102; M/.1 in L~M by A34,A35,JORDAN3:34; then L~g misses L~h by A32,A46,A47,Th1; hence contradiction by A24,A28,A40,A45,Th33; end; Lm10: LSeg(N-min L~f,NW-corner L~f) /\ LSeg(NE-corner L~f,E-max L~f) = {} proof assume LSeg(N-min L~f,NW-corner L~f) /\ LSeg(NE-corner L~f,E-max L~f) <> {}; then consider x being set such that A1: x in LSeg(N-min L~f,NW-corner L~f) /\ LSeg(NE-corner L~f,E-max L~f) by XBOOLE_0:def 1; A2: x in LSeg(N-min L~f,NW-corner L~f) by A1,XBOOLE_0:def 3; reconsider p = x as Point of TOP-REAL 2 by A1; A3: p in LSeg(NE-corner L~f,E-max L~f) by A1,XBOOLE_0:def 3; (NE-corner L~f)`1 = E-bound L~f & (E-max L~f)`1 = E-bound L~f by PSCOMP_1:76,104; then E-bound L~f <= p`1 & p`1 <= E-bound L~f by A3,TOPREAL1:9; then A4: p`1 = E-bound L~f by AXIOMS:21; (NW-corner L~f)`1 <= (N-min L~f)`1 by PSCOMP_1:97; then A5: p`1 <= (N-min L~f)`1 by A2,TOPREAL1:9; A6: (N-max L~f)`1 <= (NE-corner L~f)`1 by PSCOMP_1:97; (N-min L~f)`1 < (N-max L~f)`1 by Th55; then (N-min L~f)`1 < (NE-corner L~f)`1 by A6,AXIOMS:22; hence contradiction by A4,A5,PSCOMP_1:76; end; theorem z/.1 = N-min L~z implies (E-max L~z)..z < (E-min L~z)..z proof set i1 = (E-max L~z)..z, i2 = (E-min L~z)..z, j = (S-max L~z)..z; assume that A1: z/.1 = N-min L~z and A2: i1 >= i2; A3: E-max L~z in rng z by Th50; A4: S-max L~z in rng z by Th46; A5: E-min L~z in rng z by Th49; A6: 1 in dom z by FINSEQ_5:6; A7: i1 in dom z by A3,FINSEQ_4:30; then A8: 1 <= i1 & i1 <= len z by FINSEQ_3:27; A9: i2 in dom z by A5,FINSEQ_4:30; then A10: 1 <= i2 & i2 <= len z by FINSEQ_3:27; A11: z/.i2 = z.i2 by A9,FINSEQ_4:def 4 .= E-min L~z by A5,FINSEQ_4:29; A12: z/.len z = N-min L~z by A1,FINSEQ_6:def 1; A13: z/.i1 = z.i1 by A7,FINSEQ_4:def 4 .= E-max L~z by A3,FINSEQ_4:29; (E-min L~z)`2 < (E-max L~z)`2 by Th57; then A14: i1 > i2 by A2,A11,A13,REAL_1:def 5; then A15: i1 > 1 by A10,AXIOMS:22; A16: j in dom z by A4,FINSEQ_4:30; then A17: 1 <= j & j <= len z by FINSEQ_3:27; A18: i2 < len z by A8,A14,AXIOMS:22; A19: z/.j = z.j by A16,FINSEQ_4:def 4 .= S-max L~z by A4,FINSEQ_4:29; A20: i1 < j by A1,Lm9; then reconsider h = mid(z,j,i1) as S-Sequence_in_R2 by A15,A17,Th41; A21: h is_in_the_area_of z by A7,A16,Th27; h/.1 = S-max L~z by A7,A16,A19,Th12; then A22: (h/.1)`2 = S-bound L~z by PSCOMP_1:114; A23: L~h c= L~z by A8,A17,JORDAN4:47; A24: h/.len h = z/.i1 by A7,A16,Th13; A25: (N-min L~z)`1 < (N-max L~z)`1 by Th55; A26: S-bound L~z < N-bound L~z by TOPREAL5:22; (N-min L~z)`2 = N-bound L~z & (S-max L~z)`2 = S-bound L~z by PSCOMP_1:94, 114 ; then A27: j < len z by A12,A17,A19,A26,REAL_1:def 5; N-max L~z in L~z by SPRECT_1:13; then (N-max L~z)`1 <= E-bound L~z by PSCOMP_1:71; then (N-min L~z)`1 < E-bound L~z by A25,AXIOMS:22; then (N-min L~z)`1 < (E-min L~z)`1 by PSCOMP_1:104; then A28: i2 > 1 by A1,A10,A11,REAL_1:def 5; then reconsider M = mid(z,1,i2) as S-Sequence_in_R2 by A18,Th42; A29: L~M misses L~h by A10,A14,A20,A27,Th52; 1 <= len z by A10,AXIOMS:22; then A30: L~M c= L~z by A10,JORDAN4:47; A31: M/.len M = z/.i2 by A6,A9,Th13 .= E-min L~z by A5,FINSEQ_5:41; len M = i2 -' 1 + 1 by A10,JORDAN4:20 .= i2 by A10,AMI_5:4; then A32: len M >= 1+1 by A28,NAT_1:38; A33: len h >= 1 by A7,A16,Th9; len h <> 1 by A7,A16,A20,Th10; then len h > 1 by A33,REAL_1:def 5; then A34: len h >= 1+1 by NAT_1:38; A35: M/.1 = z/.1 by A6,A9,Th12; A36: M is_in_the_area_of z by A6,A9,Th27; A37: (M/.len M)`1 = E-bound L~z by A31,PSCOMP_1:104; per cases; suppose that A38: NW-corner L~z = N-min L~z and A39: NE-corner L~z = E-max L~z; (h/.len h)`2 = N-bound L~z by A13,A24,A39,PSCOMP_1:77; then A40: h is_a_v.c._for z by A21,A22,Def3; (M/.1)`1 = W-bound L~z by A1,A35,A38,PSCOMP_1:74; then M is_a_h.c._for z by A36,A37,Def2; hence contradiction by A29,A32,A34,A40,Th33; suppose that A41: NW-corner L~z <> N-min L~z and A42: NE-corner L~z = E-max L~z; (h/.len h)`2 = N-bound L~z by A13,A24,A42,PSCOMP_1:77; then A43: h is_a_v.c._for z by A21,A22,Def3; reconsider g = <*NW-corner L~z*>^M as S-Sequence_in_R2 by A1,A6,A9,A41,Th70; A44:2 <= len g by TOPREAL1:def 10; <*NW-corner L~z*> is_in_the_area_of z by Th30; then A45: g is_in_the_area_of z by A36,Th28; g/.1 = NW-corner L~z by FINSEQ_5:16; then A46: (g/.1)`1 = W-bound L~z by PSCOMP_1:74; A47: len M in dom M by FINSEQ_5:6; len g = len M + len<*NW-corner L~z*> by FINSEQ_1:35; then g/.len g = M/.len M by A47,GROUP_5:96 .= z/.i2 by A6,A9,Th13 .= E-min L~z by A5,FINSEQ_5:41; then (g/.len g)`1 = E-bound L~z by PSCOMP_1:104; then A48: g is_a_h.c._for z by A45,A46,Def2; A49: L~g = L~M \/ LSeg(NW-corner L~z,M/.1) by SPPOL_2:20; LSeg(M/.1,NW-corner L~z) /\ L~h c= LSeg(M/.1,NW-corner L~z) /\ L~z by A23,XBOOLE_1:26; then A50: LSeg(M/.1,NW-corner L~z) /\ L~h c= {M/.1} by A1,A35,PSCOMP_1:102; M/.1 in L~M by A32,JORDAN3:34; then L~g misses L~h by A29,A49,A50,Th1; hence contradiction by A34,A43,A44,A48,Th33; suppose that A51: NW-corner L~z = N-min L~z and A52: NE-corner L~z<> E-max L~z; M/.1 = z/.1 by A6,A9,Th12; then (M/.1)`1 = W-bound L~z by A1,A51,PSCOMP_1:74; then A53: M is_a_h.c._for z by A36,A37,Def2; reconsider N = h^<*NE-corner L~z*> as S-Sequence_in_R2 by A7,A13,A16,A52,Th69; A54:len M >= 2 & len N >= 2 by TOPREAL1:def 10; <*NE-corner L~z*> is_in_the_area_of z by Th29; then A55: N is_in_the_area_of z by A21,Th28; 1 in dom h by FINSEQ_5:6; then A56: (N/.1)`2 = S-bound L~z by A22,GROUP_5:95; len N = len h + len<*NE-corner L~z*> by FINSEQ_1:35 .= len h + 1 by FINSEQ_1:56; then N/.len N = NE-corner L~z by TOPREAL4:1; then (N/.len N)`2 = N-bound L~z by PSCOMP_1:77; then A57: N is_a_v.c._for z by A55,A56,Def3; A58: L~N = L~h \/ LSeg(NE-corner L~z,h/.len h) by SPPOL_2:19; LSeg(h/.len h,NE-corner L~z) /\ L~M c= LSeg(h/.len h,NE-corner L~z) /\ L~z by A30,XBOOLE_1:26; then A59: LSeg(h/.len h,NE-corner L~z) /\ L~M c= {h/.len h} by A13,A24,PSCOMP_1 :112; h/.len h in L~h by A34,JORDAN3:34; then L~M misses L~N by A29,A58,A59,Th1; hence contradiction by A53,A54,A57,Th33; suppose that A60: NW-corner L~z <> N-min L~z and A61: NE-corner L~z <> E-max L~z; reconsider g = <*NW-corner L~z*>^M as S-Sequence_in_R2 by A1,A6,A9,A60,Th70; <*NW-corner L~z*> is_in_the_area_of z by Th30; then A62: g is_in_the_area_of z by A36,Th28; g/.1 = NW-corner L~z by FINSEQ_5:16; then A63: (g/.1)`1 = W-bound L~z by PSCOMP_1:74; A64: len M in dom M by FINSEQ_5:6; len g = len M + len<*NW-corner L~z*> by FINSEQ_1:35; then g/.len g = M/.len M by A64,GROUP_5:96 .= z/.i2 by A6,A9,Th13 .= E-min L~z by A5,FINSEQ_5:41; then (g/.len g)`1 = E-bound L~z by PSCOMP_1:104; then A65: g is_a_h.c._for z by A62,A63,Def2; reconsider N = h^<*NE-corner L~z*> as S-Sequence_in_R2 by A7,A13,A16,A61,Th69; A66:len g >= 2 & len N >= 2 by TOPREAL1:def 10; <*NE-corner L~z*> is_in_the_area_of z by Th29; then A67: N is_in_the_area_of z by A21,Th28; 1 in dom h by FINSEQ_5:6; then A68: (N/.1)`2 = S-bound L~z by A22,GROUP_5:95; len N = len h + len<*NE-corner L~z*> by FINSEQ_1:35 .= len h + 1 by FINSEQ_1:56; then N/.len N = NE-corner L~z by TOPREAL4:1; then (N/.len N)`2 = N-bound L~z by PSCOMP_1:77; then A69: N is_a_v.c._for z by A67,A68,Def3; A70: L~N = L~h \/ LSeg(NE-corner L~z,h/.len h) by SPPOL_2:19; LSeg(h/.len h,NE-corner L~z) /\ L~M c= LSeg(h/.len h,NE-corner L~z) /\ L~z by A30,XBOOLE_1:26; then A71: LSeg(h/.len h,NE-corner L~z) /\ L~M c= {h/.len h} by A13,A24,PSCOMP_1 :112; h/.len h in L~h by A34,JORDAN3:34; then A72: L~M misses L~N by A29,A70,A71,Th1; A73: L~g = L~M \/ LSeg(NW-corner L~z,M/.1) by SPPOL_2:20; LSeg(M/.1,NW-corner L~z) /\ LSeg(NE-corner L~z,h/.len h) = {} by A1,A13,A24,A35,Lm10; then LSeg(M/.1,NW-corner L~z) /\ L~N = LSeg(M/.1,NW-corner L~z) /\ L~h \/ {} by A70,XBOOLE_1:23 .= LSeg(M/.1,NW-corner L~z) /\ L~h; then LSeg(M/.1,NW-corner L~z) /\ L~N c= LSeg(M/.1,NW-corner L~z) /\ L~z by A23,XBOOLE_1:26; then A74: LSeg(M/.1,NW-corner L~z) /\ L~N c= {M/.1} by A1,A35,PSCOMP_1:102; M/.1 in L~M by A32,JORDAN3:34; then L~g misses L~N by A72,A73,A74,Th1; hence contradiction by A65,A66,A69,Th33; end; theorem Th76: z/.1 = N-min L~z & E-min L~z <> S-max L~z implies (E-min L~z)..z < (S-max L~z)..z proof set i1 = (E-min L~z)..z, i2 = (S-max L~z)..z; assume that A1: z/.1 = N-min L~z and A2: E-min L~z <> S-max L~z and A3: i1 >= i2; A4: E-min L~z in rng z by Th49; A5: S-max L~z in rng z by Th46; A6: i1 in dom z by A4,FINSEQ_4:30; then A7: 1 <= i1 & i1 <= len z by FINSEQ_3:27; A8: i2 in dom z by A5,FINSEQ_4:30; then A9: 1 <= i2 & i2 <= len z by FINSEQ_3:27; A10: z/.i2 = z.i2 by A8,FINSEQ_4:def 4 .= S-max L~z by A5,FINSEQ_4:29; A11: z/.len z = N-min L~z by A1,FINSEQ_6:def 1; A12: z/.i1 = z.i1 by A6,FINSEQ_4:def 4 .= E-min L~z by A4,FINSEQ_4:29; then A13: i1 > i2 by A2,A3,A10,REAL_1:def 5; then A14: i1 > 1 by A9,AXIOMS:22; A15: len z in dom z by FINSEQ_5:6; A16: z/.1 = z/.len z by FINSEQ_6:def 1; A17: 2 <= len z by SPPOL_1:2; then A18: 2 in dom z by FINSEQ_3:27; z/.2 in N-most L~z by A1,Th34; then A19: (z/.2)`2 = (N-min L~z)`2 by PSCOMP_1:98 .= N-bound L~z by PSCOMP_1:94; A20: (z/.1)`2 = N-bound L~z by A1,PSCOMP_1:94; A21: i2 <> 0 by A8,FINSEQ_3:27; A22: (z/.i2)`2 = S-bound L~z by A10,PSCOMP_1:114; S-bound L~z < N-bound L~z by TOPREAL5:22; then A23: i2 > 2 by A19,A20,A21,A22,CQC_THE1:3; then reconsider h = mid(z,i2,2) as S-Sequence_in_R2 by A9,Th41; A24: len h >= 2 by TOPREAL1:def 10; A25: h is_in_the_area_of z by A8,A18,Th27; h/.1 = S-max L~z by A8,A10,A18,Th12; then A26: (h/.1)`2 = S-bound L~z by PSCOMP_1:114; A27: L~h c= L~z by A9,A17,JORDAN4:47; h/.len h = z/.2 by A8,A18,Th13; then A28: h is_a_v.c._for z by A19,A25,A26,Def3; A29: (N-min L~z)`1 < (N-max L~z)`1 by Th55; N-max L~z in L~z by SPRECT_1:13; then (N-max L~z)`1 <= E-bound L~z by PSCOMP_1:71; then (N-min L~z)`1 < E-bound L~z by A29,AXIOMS:22; then (N-min L~z)`1 < (E-min L~z)`1 by PSCOMP_1:104; then A30: i1 < len z by A7,A11,A12,REAL_1:def 5; then reconsider M = mid(z,len z,i1) as S-Sequence_in_R2 by A14,Th41; A31: L~M misses L~h by A7,A13,A23,Th53; A32: M/.len M = z/.i1 by A6,A15,Th13 .= E-min L~z by A4,FINSEQ_5:41; A33: len M = len z -' i1 + 1 by A7,JORDAN4:21; i1 + 1 <= len z by A30,NAT_1:38; then len z - i1 >= 1 by REAL_1:84; then len z -' i1 >= 1 by JORDAN3:1; then A34: len z -' i1 + 1 >= 1+1 by AXIOMS:24; A35: M/.1 = z/.1 by A6,A15,A16,Th12; per cases; suppose that A36: NW-corner L~z = N-min L~z; A37: M is_in_the_area_of z by A6,A15,Th27; M/.1 = z/.len z by A6,A15,Th12; then A38: (M/.1)`1 = W-bound L~z by A1,A16,A36,PSCOMP_1:74; (M/.len M)`1 = E-bound L~z by A32,PSCOMP_1:104; then M is_a_h.c._for z by A37,A38,Def2; hence contradiction by A24,A28,A31,A33,A34,Th33; suppose NW-corner L~z <> N-min L~z; then reconsider g = <*NW-corner L~z*>^M as S-Sequence_in_R2 by A1,A6,A15,A16,Th70; A39: len g >= 2 by TOPREAL1:def 10; A40: M is_in_the_area_of z by A6,A15,Th27; <*NW-corner L~z*> is_in_the_area_of z by Th30; then A41: g is_in_the_area_of z by A40,Th28; g/.1 = NW-corner L~z by FINSEQ_5:16; then A42: (g/.1)`1 = W-bound L~z by PSCOMP_1:74; A43: len M in dom M by FINSEQ_5:6; len g = len M + len<*NW-corner L~z*> by FINSEQ_1:35; then g/.len g = M/.len M by A43,GROUP_5:96 .= z/.i1 by A6,A15,Th13 .= E-min L~z by A4,FINSEQ_5:41; then (g/.len g)`1 = E-bound L~z by PSCOMP_1:104; then A44: g is_a_h.c._for z by A41,A42,Def2; A45: L~g = L~M \/ LSeg(NW-corner L~z,M/.1) by SPPOL_2:20; LSeg(M/.1,NW-corner L~z) /\ L~h c= LSeg(M/.1,NW-corner L~z) /\ L~z by A27,XBOOLE_1:26; then A46: LSeg(M/.1,NW-corner L~z) /\ L~h c= {M/.1} by A1,A35,PSCOMP_1:102; M/.1 in L~M by A33,A34,JORDAN3:34; then L~g misses L~h by A31,A45,A46,Th1; hence contradiction by A24,A28,A39,A44,Th33; end; theorem Th77: z/.1 = N-min L~z implies (S-max L~z)..z < (S-min L~z)..z proof set i1 = (S-max L~z)..z, i2 = (S-min L~z)..z, j = (N-max L~z)..z; assume that A1: z/.1 = N-min L~z and A2: i1 >= i2; A3: N-max L~z in rng z by Th44; A4: S-min L~z in rng z by Th45; A5: S-max L~z in rng z by Th46; then A6: i1 in dom z by FINSEQ_4:30; then A7: 1 <= i1 & i1 <= len z by FINSEQ_3:27; A8: i2 in dom z by A4,FINSEQ_4:30; then A9: 1 <= i2 & i2 <= len z by FINSEQ_3:27; A10: z/.i2 = z.i2 by A8,FINSEQ_4:def 4 .= S-min L~z by A4,FINSEQ_4:29; A11: z/.i1 = z.i1 by A6,FINSEQ_4:def 4 .= S-max L~z by A5,FINSEQ_4:29; S-min L~z <> S-max L~z by Th60; then A12: i1 > i2 by A2,A10,A11,REAL_1:def 5; A13: z/.1 = z/.len z by FINSEQ_6:def 1; (N-min L~z)`2 = N-bound L~z & (S-max L~z)`2 = S-bound L~z by PSCOMP_1:94,114; then N-min L~z <> S-max L~z by TOPREAL5:22; then A14: i1 < len z by A1,A7,A11,A13,REAL_1:def 5; A15: len z in dom z by FINSEQ_5:6; A16: j in dom z by A3,FINSEQ_4:30; then A17: 1 <= j & j <= len z by FINSEQ_3:27; A18: z/.j = z.j by A16,FINSEQ_4:def 4 .= N-max L~z by A3,FINSEQ_4:29; then A19: (z/.j)`2 = N-bound L~z by PSCOMP_1:94; A20: i2 > j by A1,Lm8; N-min L~z <> N-max L~z by Th56; then A21: 1 < j by A1,A17,A18,REAL_1:def 5; then reconsider h = mid(z,i2,j) as S-Sequence_in_R2 by A9,A20,Th41; A22: len h >= 2 by TOPREAL1:def 10; A23: h is_in_the_area_of z by A8,A16,Th27; h/.1 = S-min L~z by A8,A10,A16,Th12; then A24: (h/.1)`2 = S-bound L~z by PSCOMP_1:114; A25: L~h c= L~z by A9,A17,JORDAN4:47; h/.len h = z/.j by A8,A16,Th13; then A26: h is_a_v.c._for z by A19,A23,A24,Def3; j < i1 by A1,Lm7; then i1 > 1 by A17,AXIOMS:22; then reconsider M = mid(z,len z,i1) as S-Sequence_in_R2 by A14,Th41; A27: L~h misses L~M by A7,A12,A20,A21,Th53; A28: M/.len M = S-max L~z by A6,A11,A15,Th13; A29: len M = len z -' i1 + 1 by A7,JORDAN4:21; i1 + 1 <= len z by A14,NAT_1:38; then len z - i1 >= 1 by REAL_1:84; then len z -' i1 >= 1 by JORDAN3:1; then A30: len z -' i1 + 1 >= 1+1 by AXIOMS:24; then A31: M/.len M in L~M by A29,JORDAN3:34; A32: 1 in dom M by FINSEQ_5:6; A33: M/.1 = z/.len z by A6,A15,Th12; per cases; suppose that A34: NW-corner L~z = N-min L~z and A35: SE-corner L~z = S-max L~z; A36: M is_in_the_area_of z by A6,A15,Th27; A37: (M/.1)`1 = W-bound L~z by A1,A13,A33,A34,PSCOMP_1:74; (M/.len M)`1 = E-bound L~z by A28,A35,PSCOMP_1:78; then M is_a_h.c._for z by A36,A37,Def2; hence contradiction by A22,A26,A27,A29,A30,Th33; suppose that A38: NW-corner L~z = N-min L~z and A39: SE-corner L~z <> S-max L~z; reconsider g = M^<*SE-corner L~z*> as S-Sequence_in_R2 by A6,A11,A15,A39,Th68; A40: len g >= 2 by TOPREAL1:def 10; A41: M is_in_the_area_of z by A6,A15,Th27; <*SE-corner L~z*> is_in_the_area_of z by Th31; then A42: g is_in_the_area_of z by A41,Th28; g/.1 = M/.1 by A32,GROUP_5:95 .= z/.1 by A6,A13,A15,Th12; then A43: (g/.1)`1 = W-bound L~z by A1,A38,PSCOMP_1:74; len g = len M + len<*SE-corner L~z*> by FINSEQ_1:35 .= len M + 1 by FINSEQ_1:56; then g/.len g = SE-corner L~z by TOPREAL4:1; then (g/.len g)`1 = E-bound L~z by PSCOMP_1:78; then A44: g is_a_h.c._for z by A42,A43,Def2; A45: L~g = L~M \/ LSeg(M/.len M,SE-corner L~z) by SPPOL_2:19; LSeg(M/.len M,SE-corner L~z) /\ L~h c= LSeg(M/.len M,SE-corner L~z) /\ L~z by A25,XBOOLE_1:26; then LSeg(M/.len M,SE-corner L~z) /\ L~h c= {M/.len M} by A28,PSCOMP_1:122; then L~g misses L~h by A27,A31,A45,Th1; hence contradiction by A22,A26,A40,A44,Th33; suppose that A46: NW-corner L~z <> N-min L~z and A47: SE-corner L~z = S-max L~z; reconsider g = <*NW-corner L~z*>^M as S-Sequence_in_R2 by A1,A6,A13,A15,A46,Th70; A48: len g >= 2 by TOPREAL1:def 10; A49: M is_in_the_area_of z by A6,A15,Th27; <*NW-corner L~z*> is_in_the_area_of z by Th30; then A50: g is_in_the_area_of z by A49,Th28; g/.1 = NW-corner L~z by FINSEQ_5:16; then A51: (g/.1)`1 = W-bound L~z by PSCOMP_1:74; A52: len M in dom M by FINSEQ_5:6; len g = len M + len<*NW-corner L~z*> by FINSEQ_1:35; then g/.len g = M/.len M by A52,GROUP_5:96 .= S-max L~z by A6,A11,A15,Th13; then (g/.len g)`1 = E-bound L~z by A47,PSCOMP_1:78; then A53: g is_a_h.c._for z by A50,A51,Def2; A54: L~g = L~M \/ LSeg(NW-corner L~z,M/.1) by SPPOL_2:20; LSeg(M/.1,NW-corner L~z) /\ L~h c= LSeg(M/.1,NW-corner L~z) /\ L~z by A25,XBOOLE_1:26; then A55: LSeg(M/.1,NW-corner L~z) /\ L~h c= {M/.1} by A1,A13,A33,PSCOMP_1:102; M/.1 in L~M by A29,A30,JORDAN3:34; then L~g misses L~h by A27,A54,A55,Th1; hence contradiction by A22,A26,A48,A53,Th33; suppose that A56: NW-corner L~z <> N-min L~z and A57: SE-corner L~z <> S-max L~z; set K = <*NW-corner L~z*>^M; reconsider g = K^<*SE-corner L~z*> as S-Sequence_in_R2 by A1,A6,A11,A13,A15,A56,A57,Lm5; A58: len g >= 2 by TOPREAL1:def 10; A59: M is_in_the_area_of z by A6,A15,Th27; <*NW-corner L~z*> is_in_the_area_of z by Th30; then A60: <*NW-corner L~z*>^M is_in_the_area_of z by A59,Th28; <*SE-corner L~z*> is_in_the_area_of z by Th31; then A61: g is_in_the_area_of z by A60,Th28; 1 in dom(<*NW-corner L~z*>^M) by FINSEQ_5:6; then g/.1 = (<*NW-corner L~z*>^M)/.1 by GROUP_5:95 .= NW-corner L~z by FINSEQ_5:16; then A62: (g/.1)`1 = W-bound L~z by PSCOMP_1:74; len g = len(<*NW-corner L~z*>^M) + len<*SE-corner L~z*> by FINSEQ_1:35 .= len(<*NW-corner L~z*>^M) + 1 by FINSEQ_1:56; then g/.len g = SE-corner L~z by TOPREAL4:1; then (g/.len g)`1 = E-bound L~z by PSCOMP_1:78; then A63: g is_a_h.c._for z by A61,A62,Def2; A64: L~K = L~M \/ LSeg(NW-corner L~z,M/.1) by SPPOL_2:20; LSeg(M/.1,NW-corner L~z) /\ L~h c= LSeg(M/.1,NW-corner L~z) /\ L~z by A25,XBOOLE_1:26; then A65: LSeg(M/.1,NW-corner L~z) /\ L~h c= {M/.1} by A1,A13,A33,PSCOMP_1:102; M/.1 in L~M by A29,A30,JORDAN3:34; then A66: L~K misses L~h by A27,A64,A65,Th1; len K = len M + len<*NW-corner L~z*> by FINSEQ_1:35; then len K >= len M by NAT_1:29; then len K >= 2 by A29,A30,AXIOMS:22; then A67: K/.len K in L~K by JORDAN3:34; A68: L~g = L~K \/ LSeg(K/.len K,SE-corner L~z) by SPPOL_2:19; A69: len M in dom M by FINSEQ_5:6; len K = len M + len<*NW-corner L~z*> by FINSEQ_1:35; then A70: K/.len K = M/.len M by A69,GROUP_5:96 .= z/.i1 by A6,A15,Th13 .= S-max L~z by A5,FINSEQ_5:41; LSeg(K/.len K,SE-corner L~z) /\ L~h c= LSeg(K/.len K,SE-corner L~z) /\ L~z by A25,XBOOLE_1:26; then LSeg(K/.len K,SE-corner L~z) /\ L~h c= {K/.len K} by A70,PSCOMP_1:122; then L~g misses L~h by A66,A67,A68,Th1; hence contradiction by A22,A26,A58,A63,Th33; end; Lm11: z/.1 = N-min L~z implies (E-min L~z)..z < (S-min L~z)..z proof assume A1: z/.1 = N-min L~z; then A2: (E-min L~z)..z <= (S-max L~z)..z by Th76; (S-max L~z)..z < (S-min L~z)..z by A1,Th77; hence (E-min L~z)..z < (S-min L~z)..z by A2,AXIOMS:22; end; Lm12: z/.1 = N-min L~z & N-min L~z <> W-max L~z implies (E-min L~z)..z < (W-max L~z)..z proof set i1 = (E-min L~z)..z, i2 = (W-max L~z)..z, j = (S-min L~z)..z; assume that A1: z/.1 = N-min L~z and A2: N-min L~z <> W-max L~z and A3: i1 >= i2; A4: E-min L~z in rng z by Th49; A5: S-min L~z in rng z by Th45; A6: W-max L~z in rng z by Th48; A7: i1 in dom z by A4,FINSEQ_4:30; then A8: 1 <= i1 & i1 <= len z by FINSEQ_3:27; A9: i2 in dom z by A6,FINSEQ_4:30; then A10: 1 <= i2 & i2 <= len z by FINSEQ_3:27; A11: z/.i2 = z.i2 by A9,FINSEQ_4:def 4 .= W-max L~z by A6,FINSEQ_4:29; A12: z/.len z = N-min L~z by A1,FINSEQ_6:def 1; A13: z/.i1 = z.i1 by A7,FINSEQ_4:def 4 .= E-min L~z by A4,FINSEQ_4:29; (W-max L~z)`1 = W-bound L~z & (E-min L~z)`1 = E-bound L~z by PSCOMP_1:84,104; then (W-max L~z)`1 < (E-min L~z)`1 by TOPREAL5:23; then A14: i1 > i2 by A3,A11,A13,REAL_1:def 5; then A15: i1 > 1 by A10,AXIOMS:22; A16: len z in dom z by FINSEQ_5:6; A17: j in dom z by A5,FINSEQ_4:30; then A18: 1 <= j & j <= len z by FINSEQ_3:27; A19: z/.j = z.j by A17,FINSEQ_4:def 4 .= S-min L~z by A5,FINSEQ_4:29; A20: i2 > 1 by A1,A2,A10,A11,REAL_1:def 5; A21: z/.j = z.j by A17,FINSEQ_4:def 4 .= S-min L~z by A5,FINSEQ_4:29; (N-min L~z)`2 = N-bound L~z & (S-min L~z)`2 = S-bound L~z by PSCOMP_1:94, 114 ; then N-min L~z <> S-min L~z by TOPREAL5:22; then A22: j < len z by A12,A18,A21,REAL_1:def 5; A23: i1 < j by A1,Lm11; then j > 1 by A15,AXIOMS:22; then reconsider h = mid(z,j,len z) as S-Sequence_in_R2 by A22,Th42; A24: len h >= 2 by TOPREAL1:def 10; A25: h is_in_the_area_of z by A16,A17,Th27; h/.1 = S-min L~z by A16,A17,A19,Th12; then A26: (h/.1)`2 = S-bound L~z by PSCOMP_1:114; h/.len h = z/.len z by A16,A17,Th13; then (h/.len h)`2 = N-bound L~z by A12,PSCOMP_1:94; then A27: h is_a_v.c._for z by A25,A26,Def3; A28: (N-min L~z)`1 < (N-max L~z)`1 by Th55; N-max L~z in L~z by SPRECT_1:13; then (N-max L~z)`1 <= E-bound L~z by PSCOMP_1:71; then (N-min L~z)`1 < E-bound L~z by A28,AXIOMS:22; then (N-min L~z)`1 < (E-min L~z)`1 by PSCOMP_1:104; then i1 < len z by A8,A12,A13,REAL_1:def 5; then reconsider M = mid(z,i2,i1) as S-Sequence_in_R2 by A10,A14,Th42; A29: len M >= 2 by TOPREAL1:def 10; A30: M/.len M = z/.i1 by A7,A9,Th13 .= E-min L~z by A4,FINSEQ_5:41; A31: M/.1 = W-max L~z by A7,A9,A11,Th12; A32: M is_in_the_area_of z by A7,A9,Th27; A33: (M/.1)`1 = W-bound L~z by A31,PSCOMP_1:84; (M/.len M)`1 = E-bound L~z by A30,PSCOMP_1:104; then A34: M is_a_h.c._for z by A32,A33,Def2; L~M misses L~h by A3,A18,A20,A23,Th51; hence contradiction by A24,A27,A29,A34,Th33; end; Lm13: z/.1 = N-min L~z implies (E-min L~z)..z < (W-min L~z)..z proof set i1 = (E-min L~z)..z, i2 = (W-min L~z)..z, j = (S-min L~z)..z; assume that A1: z/.1 = N-min L~z and A2: i1 >= i2; A3: E-min L~z in rng z by Th49; A4: S-min L~z in rng z by Th45; A5: W-min L~z in rng z by Th47; A6: i1 in dom z by A3,FINSEQ_4:30; then A7: 1 <= i1 & i1 <= len z by FINSEQ_3:27; A8: i2 in dom z by A5,FINSEQ_4:30; then A9: 1 <= i2 & i2 <= len z by FINSEQ_3:27; A10: z/.i2 = z.i2 by A8,FINSEQ_4:def 4 .= W-min L~z by A5,FINSEQ_4:29; A11: z/.len z = N-min L~z by A1,FINSEQ_6:def 1; A12: z/.i1 = z.i1 by A6,FINSEQ_4:def 4 .= E-min L~z by A3,FINSEQ_4:29; (W-min L~z)`1 = W-bound L~z & (E-min L~z)`1 = E-bound L~z by PSCOMP_1:84,104; then z/.i1 <> z/.i2 by A10,A12,TOPREAL5:23; then A13: i1 > i2 by A2,REAL_1:def 5; then A14: i1 > 1 by A9,AXIOMS:22; A15: len z in dom z by FINSEQ_5:6; A16: j in dom z by A4,FINSEQ_4:30; then A17: 1 <= j & j <= len z by FINSEQ_3:27; A18: z/.j = z.j by A16,FINSEQ_4:def 4 .= S-min L~z by A4,FINSEQ_4:29; W-max L~z in L~z & (N-min L~z)`2 = N-bound L~z by PSCOMP_1:94,SPRECT_1:15 ; then (W-max L~z)`2 <= (N-min L~z)`2 by PSCOMP_1:71; then N-min L~z <> W-min L~z by Th61; then A19: i2 > 1 by A1,A9,A10,REAL_1:def 5; A20: z/.j = z.j by A16,FINSEQ_4:def 4 .= S-min L~z by A4,FINSEQ_4:29; (N-min L~z)`2 = N-bound L~z & (S-min L~z)`2 = S-bound L~z by PSCOMP_1:94, 114 ; then N-min L~z <> S-min L~z by TOPREAL5:22; then A21: j < len z by A11,A17,A20,REAL_1:def 5; A22: i1 < j by A1,Lm11; then j > 1 by A14,AXIOMS:22; then reconsider h = mid(z,j,len z) as S-Sequence_in_R2 by A21,Th42; A23: h is_in_the_area_of z by A15,A16,Th27; h/.1 = S-min L~z by A15,A16,A18,Th12; then A24: (h/.1)`2 = S-bound L~z by PSCOMP_1:114; h/.len h = z/.len z by A15,A16,Th13; then (h/.len h)`2 = N-bound L~z by A11,PSCOMP_1:94; then A25: h is_a_v.c._for z by A23,A24,Def3; A26: (N-min L~z)`1 < (N-max L~z)`1 by Th55; N-max L~z in L~z by SPRECT_1:13; then (N-max L~z)`1 <= E-bound L~z by PSCOMP_1:71; then (N-min L~z)`1 < E-bound L~z by A26,AXIOMS:22; then (N-min L~z)`1 < (E-min L~z)`1 by PSCOMP_1:104; then i1 < len z by A7,A11,A12,REAL_1:def 5; then reconsider M = mid(z,i2,i1) as S-Sequence_in_R2 by A9,A13,Th42; A27: len h >= 2 & len M >= 2 by TOPREAL1:def 10; A28: M/.len M = z/.i1 by A6,A8,Th13 .= E-min L~z by A3,FINSEQ_5:41; A29: M/.1 = W-min L~z by A6,A8,A10,Th12; A30: M is_in_the_area_of z by A6,A8,Th27; A31: (M/.1)`1 = W-bound L~z by A29,PSCOMP_1:84; (M/.len M)`1 = E-bound L~z by A28,PSCOMP_1:104; then A32: M is_a_h.c._for z by A30,A31,Def2; L~M misses L~h by A2,A17,A19,A22,Th51; hence contradiction by A25,A27,A32,Th33; end; theorem z/.1 = N-min L~z & S-min L~z <> W-min L~z implies (S-min L~z)..z < (W-min L~z)..z proof set i1 = (E-min L~z)..z, i2 = (W-min L~z)..z, j = (S-min L~z)..z; assume that A1: z/.1 = N-min L~z and A2: S-min L~z <> W-min L~z and A3: j >= i2; A4: i1 < i2 by A1,Lm13; A5: E-min L~z in rng z by Th49; A6: S-min L~z in rng z by Th45; A7: W-min L~z in rng z by Th47; A8: i1 in dom z by A5,FINSEQ_4:30; then A9: 1 <= i1 & i1 <= len z by FINSEQ_3:27; A10: i2 in dom z by A7,FINSEQ_4:30; then A11: 1 <= i2 & i2 <= len z by FINSEQ_3:27; A12: z/.i2 = z.i2 by A10,FINSEQ_4:def 4 .= W-min L~z by A7,FINSEQ_4:29; A13: z/.len z = N-min L~z by A1,FINSEQ_6:def 1; A14: j in dom z by A6,FINSEQ_4:30; then A15: z/.j = z.j by FINSEQ_4:def 4 .= S-min L~z by A6,FINSEQ_4:29; A16: z/.i1 = z.i1 by A8,FINSEQ_4:def 4 .= E-min L~z by A5,FINSEQ_4:29; A17: j > i2 by A2,A3,A12,A15,REAL_1:def 5; A18: (N-min L~z)`1 < (N-max L~z)`1 by Th55; N-max L~z in L~z by SPRECT_1:13; then (N-max L~z)`1 <= E-bound L~z by PSCOMP_1:71; then (N-min L~z)`1 < E-bound L~z by A18,AXIOMS:22; then (N-min L~z)`1 < (E-min L~z)`1 by PSCOMP_1:104; then A19: i1 > 1 by A1,A9,A16,REAL_1:def 5; A20: len z in dom z by FINSEQ_5:6; A21: 1 <= j & j <= len z by A14,FINSEQ_3:27; A22: z/.j = z.j by A14,FINSEQ_4:def 4 .= S-min L~z by A6,FINSEQ_4:29; (N-min L~z)`2 = N-bound L~z & (S-min L~z)`2 = S-bound L~z by PSCOMP_1:94, 114 ; then N-min L~z <> S-min L~z by TOPREAL5:22; then A23: j < len z by A13,A21,A22,REAL_1:def 5; i1 < j by A1,Lm11; then j > 1 by A9,AXIOMS:22; then reconsider h = mid(z,j,len z) as S-Sequence_in_R2 by A23,Th42; A24: h is_in_the_area_of z by A14,A20,Th27; h/.1 = S-min L~z by A14,A15,A20,Th12; then A25: (h/.1)`2 = S-bound L~z by PSCOMP_1:114; h/.len h = z/.len z by A14,A20,Th13; then (h/.len h)`2 = N-bound L~z by A13,PSCOMP_1:94; then A26: h is_a_v.c._for z by A24,A25,Def3; reconsider M = mid(z,i2,i1) as S-Sequence_in_R2 by A4,A11,A19,Th41; A27: len h >= 2 & len M >= 2 by TOPREAL1:def 10; A28: L~M misses L~h by A4,A17,A19,A21,Th54; A29: M/.len M = z/.i1 by A8,A10,Th13 .= E-min L~z by A5,FINSEQ_5:41; A30: M/.1 = W-min L~z by A8,A10,A12,Th12; A31: M is_in_the_area_of z by A8,A10,Th27; A32: (M/.1)`1 = W-bound L~z by A30,PSCOMP_1:84; (M/.len M)`1 = E-bound L~z by A29,PSCOMP_1:104; then M is_a_h.c._for z by A31,A32,Def2; hence contradiction by A26,A27,A28,Th33; end; theorem Th79: z/.1 = N-min L~z & N-min L~z <> W-max L~z implies (W-min L~z)..z < (W-max L~z)..z proof set i1 = (W-min L~z)..z, i2 = (W-max L~z)..z, j = (E-min L~z)..z; assume that A1: z/.1 = N-min L~z and A2: N-min L~z <> W-max L~z and A3: i1 >= i2; A4: E-min L~z in rng z by Th49; A5: W-max L~z in rng z by Th48; A6: W-min L~z in rng z by Th47; then A7: i1 in dom z by FINSEQ_4:30; then A8: 1 <= i1 & i1 <= len z by FINSEQ_3:27; A9: i2 in dom z by A5,FINSEQ_4:30; then A10: 1 <= i2 & i2 <= len z by FINSEQ_3:27; A11: z/.i2 = z.i2 by A9,FINSEQ_4:def 4 .= W-max L~z by A5,FINSEQ_4:29; A12: z/.len z = N-min L~z by A1,FINSEQ_6:def 1; A13: z/.i1 = z.i1 by A7,FINSEQ_4:def 4 .= W-min L~z by A6,FINSEQ_4:29; W-max L~z <> W-min L~z by Th62; then A14: i1 > i2 by A3,A11,A13,REAL_1:def 5; A15: z/.1 = z/.len z by FINSEQ_6:def 1; W-max L~z in L~z & (N-min L~z)`2 = N-bound L~z by PSCOMP_1:94,SPRECT_1:15 ; then (W-max L~z)`2 <= (N-min L~z)`2 by PSCOMP_1:71; then N-min L~z <> W-min L~z by Th61; then A16: i1 < len z by A1,A8,A13,A15,REAL_1:def 5; A17: len z in dom z by FINSEQ_5:6; A18: j in dom z by A4,FINSEQ_4:30; then A19: 1 <= j & j <= len z by FINSEQ_3:27; A20: z/.j = z.j by A18,FINSEQ_4:def 4 .= E-min L~z by A4,FINSEQ_4:29; then A21: (z/.j)`1 = E-bound L~z by PSCOMP_1:104; A22: i2 > j by A1,A2,Lm12; A23: (N-min L~z)`1 < (N-max L~z)`1 by Th55; N-max L~z in L~z by SPRECT_1:13; then (N-max L~z)`1 <= E-bound L~z by PSCOMP_1:71; then (N-min L~z)`1 < E-bound L~z by A23,AXIOMS:22; then (N-min L~z)`1 < (E-min L~z)`1 by PSCOMP_1:104; then A24: 1 < j by A1,A19,A20,REAL_1:def 5; then reconsider h = mid(z,i2,j) as S-Sequence_in_R2 by A10,A22,Th41; A25: len h >= 2 by TOPREAL1:def 10; A26: h is_in_the_area_of z by A9,A18,Th27; h/.1 = W-max L~z by A9,A11,A18,Th12; then A27: (h/.1)`1 = W-bound L~z by PSCOMP_1:84; A28: L~h c= L~z by A10,A19,JORDAN4:47; h/.len h = z/.j by A9,A18,Th13; then A29: h is_a_h.c._for z by A21,A26,A27,Def2; j < i1 by A1,Lm13; then i1 > 1 by A19,AXIOMS:22; then reconsider M = mid(z,i1,len z) as S-Sequence_in_R2 by A16,Th42; A30: L~M misses L~h by A8,A14,A22,A24,Th54; A31: len M = len z -' i1 + 1 by A8,JORDAN4:20; i1 + 1 <= len z by A16,NAT_1:38; then len z - i1 >= 1 by REAL_1:84; then len z -' i1 >= 1 by JORDAN3:1; then A32: len z -' i1 + 1 >= 1+1 by AXIOMS:24; A33: M/.1 = z/.i1 by A7,A17,Th12; A34: M/.len M = z/.len z by A7,A17,Th13; A35: M is_in_the_area_of z by A7,A17,Th27; per cases; suppose SW-corner L~z = W-min L~z; then A36: (M/.1)`2 = S-bound L~z by A13,A33,PSCOMP_1:73; (M/.len M)`2 = N-bound L~z by A12,A34,PSCOMP_1:94; then M is_a_v.c._for z by A35,A36,Def3; hence contradiction by A25,A29,A30,A31,A32,Th33; suppose SW-corner L~z <> W-min L~z; then reconsider g = <*SW-corner L~z*>^M as S-Sequence_in_R2 by A7,A13,A17,Th71; A37: len g >= 2 by TOPREAL1:def 10; <*SW-corner L~z*> is_in_the_area_of z by Th32; then A38: g is_in_the_area_of z by A35,Th28; g/.1 = SW-corner L~z by FINSEQ_5:16; then A39: (g/.1)`2 = S-bound L~z by PSCOMP_1:73; A40: len M in dom M by FINSEQ_5:6; len g = len M + len<*SW-corner L~z*> by FINSEQ_1:35; then g/.len g = M/.len M by A40,GROUP_5:96; then (g/.len g)`2 = N-bound L~z by A12,A34,PSCOMP_1:94; then A41: g is_a_v.c._for z by A38,A39,Def3; A42: L~g = L~M \/ LSeg(SW-corner L~z,M/.1) by SPPOL_2:20; LSeg(M/.1,SW-corner L~z) /\ L~h c= LSeg(M/.1,SW-corner L~z) /\ L~z by A28,XBOOLE_1:26; then A43: LSeg(M/.1,SW-corner L~z) /\ L~h c= {M/.1} by A13,A33,PSCOMP_1:92; M/.1 in L~M by A31,A32,JORDAN3:34; then L~g misses L~h by A30,A42,A43,Th1; hence contradiction by A25,A29,A37,A41,Th33; end; theorem z/.1 = N-min L~z implies (W-min L~z)..z < len z proof A1: W-min L~z in rng z by Th47; A2: W-max L~z in rng z by Th48; assume A3: z/.1 = N-min L~z; per cases; suppose A4: N-min L~z = W-max L~z; A5: (W-min L~z)..z in dom z by A1,FINSEQ_4:30; then A6: (W-min L~z)..z <= len z by FINSEQ_3:27; A7: z/.((W-min L~z)..z) = z.((W-min L~z)..z) by A5,FINSEQ_4:def 4 .= W-min L~z by A1,FINSEQ_4:29; z/.len z = W-max L~z by A3,A4,FINSEQ_6:def 1; then (W-min L~z)..z <> len z by A7,Th62; hence thesis by A6,REAL_1:def 5; suppose N-min L~z <> W-max L~z; then A8: (W-min L~z)..z < (W-max L~z)..z by A3,Th79; (W-max L~z)..z in dom z by A2,FINSEQ_4:30; then (W-max L~z)..z <= len z by FINSEQ_3:27; hence thesis by A8,AXIOMS:22; end; theorem f/.1 = N-min L~f implies (W-max L~f)..f < len f proof A1: W-max L~f in rng f by Th48; assume A2: f/.1 = N-min L~f; then A3: f/.len f = N-min L~f by FINSEQ_6:def 1; (W-max L~f)..f in dom f by A1,FINSEQ_4:30; then A4: f/.((W-max L~f)..f) = f.((W-max L~f)..f) by FINSEQ_4:def 4 .= W-max L~f by A1,FINSEQ_4:29; per cases; suppose N-min L~f = W-max L~f; then A5: (W-max L~f)..f = 1 by A2,FINSEQ_6:47; len f > 4 by GOBOARD7:36; hence thesis by A5,AXIOMS:22; suppose A6: N-min L~f <> W-max L~f; (W-max L~f)..f <= len f by A1,FINSEQ_4:31; hence (W-max L~f)..f < len f by A3,A4,A6,REAL_1:def 5; end;

Back to top