:: Special Polygons :: by Czes\law Byli\'nski and Yatsuka Nakamura :: :: Received January 30, 1995 :: Copyright (c) 1995-2012 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, SUBSET_1, EUCLID, FINSEQ_1, PRE_TOPC, XREAL_0, ORDINAL1, NAT_1, ARYTM_3, RLTOPSP1, FINSEQ_5, XXREAL_0, RELAT_1, PARTFUN1, CARD_1, XBOOLE_0, RFINSEQ, ARYTM_1, ORDINAL4, FINSEQ_4, TOPREAL1, STRUCT_0, TARSKI, MCART_1, FUNCT_1, ZFMISC_1, TOPREAL4, XXREAL_1, RCOMP_1, BORSUK_1, TOPS_2, ORDINAL2, SPPOL_2; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, NAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, ZFMISC_1, FINSEQ_4, RFINSEQ, STRUCT_0, PRE_TOPC, COMPTS_1, TOPS_2, RLTOPSP1, EUCLID, BORSUK_1, TOPREAL1, TOPREAL4, FINSEQ_5; constructors XXREAL_0, NAT_1, FINSEQ_4, ZFMISC_1, RFINSEQ, BINARITH, FINSEQ_5, TOPS_2, COMPTS_1, TOPMETR, TOPREAL1, TOPREAL4, REAL_1, CONVEX1; registrations XBOOLE_0, RELAT_1, ORDINAL1, XXREAL_0, XREAL_0, MEMBERED, FINSEQ_1, FINSEQ_5, STRUCT_0, PRE_TOPC, EUCLID, TOPREAL1, NAT_1, INT_1, CARD_1, RLTOPSP1, SPPOL_1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; definitions TARSKI, TOPREAL1, TOPREAL4, XBOOLE_0; theorems TARSKI, ENUMSET1, ZFMISC_1, NAT_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, TOPS_2, HEINE, TOPMETR, COMPTS_1, RFINSEQ, EUCLID, TOPREAL1, TOPREAL3, TOPREAL4, GOBOARD1, FINSEQ_5, RELAT_1, PARTFUN2, INT_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, ORDINAL1, PARTFUN1, CARD_1, RLTOPSP1, SEQ_4, NAT_D; schemes FINSEQ_2; begin :: Segments in TOP-REAL 2 reserve P for Subset of TOP-REAL 2, f,f1,f2,g for FinSequence of TOP-REAL 2, p,p1,p2,q,q1,q2 for Point of TOP-REAL 2, r1,r2,r19,r29 for real number, i,j,k,n for Element of NAT; theorem |[ r1,r2 ]| = |[ r19,r29 ]| implies r1 = r19 & r2 = r29 by FINSEQ_1:77; theorem Th2: for i, j being Nat holds i+j = len f implies LSeg(f,i) = LSeg(Rev f,j) proof let i, j be Nat; assume A1: i+j = len f; per cases; suppose that A2: 1 <= i and A3: i + 1 <= len f; A4: i+(j+1) = len f + 1 by A1; A5: i in dom f by A2,A3,SEQ_4:134; then j+1 in dom Rev f by A4,FINSEQ_5:59; then A6: j+1 <= len Rev f by FINSEQ_3:25; A7: i+1+j = len f + 1 by A1; A8: i+1 in dom f by A2,A3,SEQ_4:134; then j in dom Rev f by A7,FINSEQ_5:59; then A9: 1 <= j by FINSEQ_3:25; thus LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A2,A3,TOPREAL1:def 3 .= LSeg((Rev f)/.(j+1),f/.(i+1)) by A5,A4,FINSEQ_5:66 .= LSeg((Rev f)/.j,(Rev f)/.(j+1)) by A8,A7,FINSEQ_5:66 .= LSeg(Rev f,j) by A6,A9,TOPREAL1:def 3; end; suppose A10: not 1 <= i; then i = 0 by NAT_1:14; then not j+1 <= len f by A1,NAT_1:13; then A11: not j+1 <= len Rev f by FINSEQ_5:def 3; LSeg(f,i) = {} by A10,TOPREAL1:def 3; hence thesis by A11,TOPREAL1:def 3; end; suppose A12: not i+1 <= len f; then A13: LSeg(f,i) = {} by TOPREAL1:def 3; j < 1 by A1,A12,XREAL_1:6; hence thesis by A13,TOPREAL1:def 3; end; end; theorem Th3: for i, n being Nat holds i+1 <= len(f|n) implies LSeg(f|n,i) = LSeg(f,i) proof let i,n be Nat; assume A1: i+1 <= len(f|n); per cases; suppose i <> 0; then A2: 1 <= i by NAT_1:14; then A3: i in dom(f|n) by A1,SEQ_4:134; len(f|n) <= len f by FINSEQ_5:16; then A4: i+1 <= len f by A1,XXREAL_0:2; A5: i+1 in dom(f|n) by A1,A2,SEQ_4:134; thus LSeg(f|n,i) = LSeg((f|n)/.i,(f|n)/.(i+1)) by A1,A2,TOPREAL1:def 3 .= LSeg(f/.i,(f|n)/.(i+1)) by A3,FINSEQ_4:70 .= LSeg(f/.i,f/.(i+1)) by A5,FINSEQ_4:70 .= LSeg(f,i) by A2,A4,TOPREAL1:def 3; end; suppose A6: i = 0; hence LSeg(f|n,i) = {} by TOPREAL1:def 3 .= LSeg(f,i) by A6,TOPREAL1:def 3; end; end; theorem Th4: for i, n being Nat holds n <= len f & 1 <= i implies LSeg(f/^n,i) = LSeg(f,n+i) proof let i,n be Nat; assume that A1: n <= len f and A2: 1 <= i; per cases; suppose A3: i+1 <= len f - n; 1<=i+1 by NAT_1:11; then 1 <= len f - n by A3,XXREAL_0:2; then A4: 1+n <= len f by XREAL_1:19; n <= 1+n by NAT_1:11; then n <= len f by A4,XXREAL_0:2; then A5: len(f/^n) = len f - n by RFINSEQ:def 1; then A6: i in dom(f/^n) by A2,A3,SEQ_4:134; A7: i+1+n <= len f by A3,XREAL_1:19; i <= i+n by NAT_1:11; then A8: 1 <= i+n by A2,XXREAL_0:2; A9: i+1 in dom(f/^n) by A2,A3,A5,SEQ_4:134; thus LSeg(f/^n,i) = LSeg((f/^n)/.i,(f/^n)/.(i+1)) by A2,A3,A5, TOPREAL1:def 3 .= LSeg(f/.(i+n),(f/^n)/.(i+1)) by A6,FINSEQ_5:27 .= LSeg(f/.(i+n),f/.(i+1+n)) by A9,FINSEQ_5:27 .= LSeg(f/.(i+n),f/.(i+n+1)) .= LSeg(f,n+i) by A8,A7,TOPREAL1:def 3; end; suppose A10: i+1 > len f - n; then n+(i+1) > len f by XREAL_1:19; then A11: n+i+1 > len f; i+1 > len(f/^n) by A1,A10,RFINSEQ:def 1; hence LSeg(f/^n,i) = {} by TOPREAL1:def 3 .= LSeg(f,n+i) by A11,TOPREAL1:def 3; end; end; theorem Th5: for i, n being Nat holds 1 <= i & i+1 <= len f - n implies LSeg(f /^n,i) = LSeg(f,n+i) proof let i, n be Nat; assume A1: 1 <= i; A2: n <= i+1+n by NAT_1:11; assume i+1 <= len f - n; then i+1+n <= len f by XREAL_1:19; then n <= len f by A2,XXREAL_0:2; hence thesis by A1,Th4; end; theorem Th6: for i being Nat holds i+1 <= len f implies LSeg(f^g,i) = LSeg(f,i ) proof let i be Nat; assume A1: i+1 <= len f; per cases; suppose i <> 0; then A2: 1 <= i by NAT_1:14; then A3: i in dom f by A1,SEQ_4:134; len(f^g) = len f + len g by FINSEQ_1:22; then len(f^g) >= len f by NAT_1:11; then A4: i+1 <= len(f^g) by A1,XXREAL_0:2; A5: i+1 in dom f by A1,A2,SEQ_4:134; thus LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A1,A2,TOPREAL1:def 3 .= LSeg((f^g)/.i,f/.(i+1)) by A3,FINSEQ_4:68 .= LSeg((f^g)/.i,(f^g)/.(i+1)) by A5,FINSEQ_4:68 .= LSeg(f^g,i) by A2,A4,TOPREAL1:def 3; end; suppose A6: i = 0; hence LSeg(f^g,i) = {} by TOPREAL1:def 3 .= LSeg(f,i) by A6,TOPREAL1:def 3; end; end; theorem Th7: for i being Nat holds 1 <= i implies LSeg(f^g,len f + i) = LSeg(g ,i) proof let i be Nat; assume A1: 1 <= i; per cases; suppose A2: i+1 <= len g; len f +(i+1) = len f+i+1; then len f +i+1 <= len f + len g by A2,XREAL_1:6; then A3: len f+i+1 <= len(f^g) by FINSEQ_1:22; i <= len f+i by NAT_1:11; then A4: 1 <= len f+i by A1,XXREAL_0:2; A5: i+1 in dom g by A1,A2,SEQ_4:134; A6: i in dom g by A1,A2,SEQ_4:134; thus LSeg(g,i) = LSeg(g/.i,g/.(i+1)) by A1,A2,TOPREAL1:def 3 .= LSeg((f^g)/.(len f+i),g/.(i+1)) by A6,FINSEQ_4:69 .= LSeg((f^g)/.(len f+i), (f^g)/.(len f + (i+1))) by A5,FINSEQ_4:69 .= LSeg(f^g,len f + i) by A4,A3,TOPREAL1:def 3; end; suppose A7: i+1 > len g; then len f + (i + 1) > len f + len g by XREAL_1:6; then len f + i + 1 > len(f^g) by FINSEQ_1:22; hence LSeg(f^g,len f + i) = {} by TOPREAL1:def 3 .= LSeg(g,i) by A7,TOPREAL1:def 3; end; end; theorem Th8: f is non empty & g is non empty implies LSeg(f^g,len f) = LSeg(f /.len f,g/.1) proof assume that A1: f is non empty and A2: g is non empty; A3: 1 in dom g by A2,FINSEQ_5:6; then 1 <= len g by FINSEQ_3:25; then len f + 1 <= len f + len g by XREAL_1:6; then A4: len f + 1 <= len(f^g) by FINSEQ_1:22; A5: len f in dom f by A1,FINSEQ_5:6; then 1 <= len f by FINSEQ_3:25; hence LSeg(f^g,len f) = LSeg((f^g)/.(len f),(f^g)/.(len f+1)) by A4, TOPREAL1:def 3 .= LSeg(f/.len f,(f^g)/.(len f+1)) by A5,FINSEQ_4:68 .= LSeg(f/.len f,g/.1) by A3,FINSEQ_4:69; end; theorem Th9: for i being Nat holds i+1 <= len(f-:p) implies LSeg(f-:p,i) = LSeg(f,i) proof let i be Nat; f-:p = f|(p..f) by FINSEQ_5:def 1; hence thesis by Th3; end; theorem Th10: for i being Nat holds p in rng f implies LSeg(f:-p,i+1) = LSeg(f ,i+p..f) proof let i be Nat; A1: 1 <= i+1 by NAT_1:11; assume A2: p in rng f; then A3: len (f:-p) = len f - p..f + 1 by FINSEQ_5:50; A4: i+(1+1) = i+1+1; per cases; suppose A5: i+2 <= len(f:-p); then i+1 <= len f - p..f by A4,A3,XREAL_1:6; then A6: i+1+p..f <= len f by XREAL_1:19; 1 <= p..f by A2,FINSEQ_4:21; then i+1 <= i+p..f by XREAL_1:6; then A7: 1 <= i+p..f by A1,XXREAL_0:2; A8: i+1 in dom(f:-p) by A1,A4,A5,SEQ_4:134; A9: i+1+1 in dom(f:-p) by A1,A5,SEQ_4:134; thus LSeg(f:-p,i+1) = LSeg((f:-p)/.(i+1),(f:-p)/.(i+1+1)) by A1,A5, TOPREAL1:def 3 .= LSeg(f/.(i+p..f),(f:-p)/.(i+1+1)) by A2,A8,FINSEQ_5:52 .= LSeg(f/.(i+p..f),f/.(i+1+p..f)) by A2,A9,FINSEQ_5:52 .= LSeg(f/.(i+p..f),f/.(i+p..f+1)) .= LSeg(f,i+p..f) by A7,A6,TOPREAL1:def 3; end; suppose A10: i+2 > len(f:-p); then i+1 > len f - p..f by A4,A3,XREAL_1:6; then p..f+(i+1) > len f by XREAL_1:19; then i+p..f+1 > len f; hence LSeg(f,i+p..f) = {} by TOPREAL1:def 3 .= LSeg(f:-p,i+1) by A4,A10,TOPREAL1:def 3; end; end; theorem Th11: L~<*>(the carrier of TOP-REAL 2) = {} by TOPREAL1:22; theorem Th12: L~<*p*> = {} proof len <*p*> = 1 by FINSEQ_1:39; hence thesis by TOPREAL1:22; end; theorem Th13: p in L~f implies ex i st 1 <= i & i+1 <= len f & p in LSeg(f,i) proof set X = { LSeg(f,i) : 1 <= i & i+1 <= len f}; assume p in L~f; then consider Y being set such that A1: p in Y and A2: Y in X by TARSKI:def 4; ex i st Y = LSeg(f,i) & 1 <= i & i+1 <= len f by A2; hence thesis by A1; end; theorem Th14: p in L~f implies ex i st 1 <= i & i+1 <= len f & p in LSeg(f/.i, f/.(i+1)) proof assume p in L~f; then consider i such that A1: 1 <= i and A2: i+1 <= len f and A3: p in LSeg(f,i) by Th13; take i; thus 1 <= i & i+1 <= len f by A1,A2; thus thesis by A1,A2,A3,TOPREAL1:def 3; end; theorem Th15: 1 <= i & i+1 <= len f & p in LSeg(f/.i,f/.(i+1)) implies p in L~ f proof assume that A1: 1 <= i and A2: i+1 <= len f and A3: p in LSeg(f/.i,f/.(i+1)); set X = { LSeg(f,j) : 1 <= j & j+1 <= len f }; A4: LSeg(f,i) in X by A1,A2; LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A1,A2,TOPREAL1:def 3; hence thesis by A3,A4,TARSKI:def 4; end; theorem 1 <= i & i+1 <= len f implies LSeg(f/.i,f/.(i+1)) c= L~f proof assume that A1: 1 <= i and A2: i+1 <= len f; LSeg(f,i) = LSeg(f/.i,f/.(i+1)) by A1,A2,TOPREAL1:def 3; hence thesis by TOPREAL3:19; end; theorem p in LSeg(f,i) implies p in L~f proof LSeg(f,i) c= L~f by TOPREAL3:19; hence thesis; end; theorem Th18: len f >= 2 implies rng f c= L~f proof assume A1: len f >= 2; let x be set; assume x in rng f; then consider i such that A2: i in dom f and A3: f/.i = x by PARTFUN2:2; A4: 1 <= i by A2,FINSEQ_3:25; A5: i <= len f by A2,FINSEQ_3:25; A6: f/.i in LSeg(f/.i,f/.(i+1)) by RLTOPSP1:68; per cases; suppose A7: i = len f; then consider j be Nat such that A8: j+1 = i by A1,NAT_1:6; reconsider j as Element of NAT by ORDINAL1:def 12; 1+1 <= j+1 by A1,A7,A8; then A9: 1 <= j by XREAL_1:6; f/.(j+1) in LSeg(f/.j,f/.(j+1)) by RLTOPSP1:68; hence thesis by A3,A7,A8,A9,Th15; end; suppose i <> len f; then i < len f by A5,XXREAL_0:1; then i+1 <= len f by NAT_1:13; hence thesis by A3,A4,A6,Th15; end; end; theorem Th19: f is non empty implies L~(f^<*p*>) = L~f \/ LSeg(f/.len f,p) proof set fp = f^<*p*>; A1: len f + 1 <= len fp by FINSEQ_2:16; 1 <= len f + 1 by NAT_1:11; then A2: len f + 1 in dom fp by A1,FINSEQ_3:25; A3: fp/.(len f + 1) = p by FINSEQ_4:67; len fp = len f + 1 by FINSEQ_2:16; then A4: fp|(len f + 1) = fp by FINSEQ_1:58; A5: dom f c= dom(fp) by FINSEQ_1:26; A6: fp|len f = f by FINSEQ_5:23; assume f is non empty; then A7: len f in dom f by FINSEQ_5:6; then fp/.len f = f/.len f by FINSEQ_4:68; hence thesis by A2,A7,A3,A4,A5,A6,TOPREAL3:38; end; theorem Th20: f is non empty implies L~(<*p*>^f) = LSeg(p,f/.1) \/ L~f proof set q = f/.1; A1: len <*p*> = 1 by FINSEQ_1:39; then A2: len (<*p*>^f) = 1 + len f by FINSEQ_1:22; assume that A3: f is non empty; hereby let x be set; assume A4: x in L~(<*p*>^f); then reconsider r = x as Point of TOP-REAL 2; consider i such that A5: 1 <= i and A6: i+1 <= len (<*p*>^f) and A7: r in LSeg((<*p*>^f)/.i,(<*p*>^f)/.(i+1)) by A4,Th14; now per cases by A5,XXREAL_0:1; case A8: i = 1; then A9: p = (<*p*>^f)/.i by FINSEQ_5:15; i in dom f by A3,A8,FINSEQ_5:6; hence r in LSeg(p,q) by A1,A7,A8,A9,FINSEQ_4:69; end; case A10: i > 1; then consider j be Nat such that A11: i = j + 1 by NAT_1:6; reconsider j as Element of NAT by ORDINAL1:def 12; A12: 1 <= j by A10,A11,NAT_1:13; A13: j+1 <= len f by A2,A6,A11,XREAL_1:6; then j+1 in dom f by A12,SEQ_4:134; then A14: (<*p*>^f)/.(i+1) = f/.(j+1) by A1,A11,FINSEQ_4:69; j in dom f by A12,A13,SEQ_4:134; then (<*p*>^f)/.i = f/.j by A1,A11,FINSEQ_4:69; hence r in L~f by A7,A12,A13,A14,Th15; end; end; hence x in LSeg(p,q) \/ L~f by XBOOLE_0:def 3; end; let x be set; assume A15: x in LSeg(p,q) \/ L~f; then reconsider r = x as Point of TOP-REAL 2; per cases by A15,XBOOLE_0:def 3; suppose A16: r in LSeg(p,q); set i = 1; i <= len f by A3,NAT_1:14; then A17: i+1 <= len(<*p*>^f) by A2,XREAL_1:6; i in dom f by A3,FINSEQ_5:6; then A18: q = (<*p*>^f)/.(i+1) by A1,FINSEQ_4:69; p = (<*p*>^f)/.i by FINSEQ_5:15; hence thesis by A16,A17,A18,Th15; end; suppose r in L~f; then consider j such that A19: 1 <= j and A20: j+1 <= len f and A21: r in LSeg(f/.j,f/.(j+1)) by Th14; set i = j + 1; j in dom f by A19,A20,SEQ_4:134; then A22: (<*p*>^f)/.i = f/.j by A1,FINSEQ_4:69; j+1 in dom f by A19,A20,SEQ_4:134; then A23: (<*p*>^f)/.(i+1) = f/.(j+1) by A1,FINSEQ_4:69; i+1 <= len (<*p*>^f) by A2,A20,XREAL_1:6; hence thesis by A21,A22,A23,Th15,NAT_1:12; end; end; theorem Th21: L~<*p,q*> = LSeg(p,q) proof set f = <*p*>; A1: len f = 1 by FINSEQ_1:39; thus L~<*p,q*> = L~(f^<*q*>) by FINSEQ_1:def 9 .= L~f \/ LSeg(f/.len f,q) by Th19 .= L~f \/ LSeg(p,q) by A1,FINSEQ_4:16 .= {} \/ LSeg(p,q) by A1,TOPREAL1:22 .= LSeg(p,q); end; theorem Th22: L~f = L~(Rev f) proof defpred P[FinSequence of TOP-REAL 2] means L~$1 = L~(Rev $1); A1: for f,p st P[f] holds P[f^<*p*>] proof let f,p such that A2: P[f]; per cases; suppose A3: f is empty; hence L~(f^<*p*>) = L~<*p*> by FINSEQ_1:34 .= L~(Rev <*p*>) by FINSEQ_5:60 .= L~(Rev(f^<*p*>)) by A3,FINSEQ_1:34; end; suppose A4: f is non empty; set q9 = (Rev f)/.1; set q = f/.len f; len f = len Rev f by FINSEQ_5:def 3; then A5: Rev f is non empty by A4; q = q9 by A4,FINSEQ_5:65; hence L~(f^<*p*>) = LSeg(p,q9) \/ L~(Rev f) by A2,A4,Th19 .= L~(<*p*>^(Rev f)) by A5,Th20 .= L~(Rev(f^<*p*>)) by FINSEQ_5:63; end; end; A6: P[<*>(the carrier of TOP-REAL 2)]; for f holds P[f] from FINSEQ_2:sch 2(A6,A1); hence thesis; end; theorem Th23: f1 is non empty & f2 is non empty implies L~(f1^f2) = L~f1 \/ LSeg(f1/.len f1,f2/.1) \/ L~f2 proof set p = f1/.len f1, q = f2/.1; defpred P[FinSequence of TOP-REAL 2] means L~(f1^<*q*>^$1) = L~f1 \/ LSeg(p, q) \/ L~(<*q*>^$1); assume A1: f1 is non empty; A2: for f for o being Point of TOP-REAL 2 st P[f] holds P[f^<*o*>] proof let f; let o be Point of TOP-REAL 2 such that A3: P[f]; per cases; suppose f is empty; then A4: (f^<*o*>) = <*o*> by FINSEQ_1:34; len(f1^<*q*>) = len f1 + 1 by FINSEQ_2:16; then (f1^<*q*>)/.len(f1^<*q*>) = q by FINSEQ_4:67; hence L~(f1^<*q*>^(f^<*o*>)) = L~(f1^<*q*>) \/ LSeg(q,o) by A4,Th19 .= L~f1 \/ LSeg(p,q) \/ LSeg(q,o) by A1,Th19 .= L~f1 \/ LSeg(p,q) \/ L~<*q,o*> by Th21 .= L~f1 \/ LSeg(p,q) \/ L~(<*q*>^(f^<*o*>)) by A4,FINSEQ_1:def 9; end; suppose A5: f is non empty; set g = f1^<*q*>^f, h = <*q*>^f; len f <> 0 by A5; then consider f9 being FinSequence of TOP-REAL 2, d being Point of TOP-REAL 2 such that A6: f = f9^<*d*> by FINSEQ_2:19; A7: h = <*q*>^f9^<*d*> by A6,FINSEQ_1:32; then len h = len(<*q*>^f9)+1 by FINSEQ_2:16; then A8: h/.len h = d by A7,FINSEQ_4:67; A9: g = f1^<*q*>^f9^<*d*> by A6,FINSEQ_1:32; then len g = len(f1^<*q*>^f9)+1 by FINSEQ_2:16; then g/.len g = d by A9,FINSEQ_4:67; then A10: L~h \/ LSeg(g/.len g,o) = L~(h^<*o*>) by A8,Th19 .= L~(<*q*>^(f^<*o*>)) by FINSEQ_1:32; thus L~(f1^<*q*>^(f^<*o*>)) = L~(g^<*o*>) by FINSEQ_1:32 .= L~g \/ LSeg(g/.len g,o) by Th19 .= L~f1 \/ LSeg(p,q) \/ L~(<*q*>^(f^<*o*>)) by A3,A10,XBOOLE_1:4; end; end; assume f2 is non empty; then A11: f2 = <*q*>^(f2/^1) by FINSEQ_5:29; A12: P[<*>(the carrier of TOP-REAL 2)] proof set O = <*>(the carrier of TOP-REAL 2); thus L~(f1^<*q*>^O) = L~(f1^<*q*>) by FINSEQ_1:34 .= L~f1 \/ LSeg(p,q) \/ {} by A1,Th19 .= L~f1 \/ LSeg(p,q) \/ L~<*q*> by Th12 .= L~f1 \/ LSeg(p,q) \/ L~(<*q*>^O) by FINSEQ_1:34; end; for f holds P[f] from FINSEQ_2:sch 2(A12,A2); then L~(f1^<*q*>^(f2/^1)) = L~f1 \/ LSeg(p,q) \/ L~(<*q*>^(f2/^1)); hence thesis by A11,FINSEQ_1:32; end; Lm1: L~(f|n) c= L~f proof now per cases; suppose A1: n = 0; f|0 is empty; hence thesis by A1,Th11,XBOOLE_1:2; end; suppose A2: n <> 0; now per cases; suppose A3: n < len f; then len(f/^n) = len f - n by RFINSEQ:def 1; then len(f/^n) <> 0 by A3; then A4: f/^n is non empty; len(f|n) = n by A3,FINSEQ_1:59; then A5: f|n is non empty by A2; (f|n)^(f/^n) = f by RFINSEQ:8; then L~f = L~(f|n) \/ LSeg((f|n)/.len(f|n),(f/^n)/.1) \/ L~(f/^n) by A5,A4 ,Th23 .= L~(f|n) \/ (LSeg((f|n)/.len(f|n),(f/^n)/.1) \/ L~(f/^n)) by XBOOLE_1:4; hence thesis by XBOOLE_1:7; end; suppose n >= len f; hence thesis by FINSEQ_1:58; end; end; hence thesis; end; end; hence thesis; end; theorem Th24: q in rng f implies L~f = L~(f-:q) \/ L~(f:-q) proof set n = q..f; assume A1: q in rng f; then A2: n <= len f by FINSEQ_4:21; per cases by A2,XXREAL_0:1; suppose A3: n < len f; then len(f/^n) = len f - n by RFINSEQ:def 1; then len(f/^n) <> 0 by A3; then A4: f/^n is non empty; A5: len(f|n) = n by A3,FINSEQ_1:59; f|n = f-:q by FINSEQ_5:def 1; then A6: (f|n)/.len(f|n) = q by A1,A5,FINSEQ_5:45; A7: (f|n)^(f/^n) = f by RFINSEQ:8; f|n is non empty by A1,A5,FINSEQ_4:21; hence L~f = L~(f|n) \/ LSeg((f|n)/.len(f|n),(f/^n)/.1) \/ L~(f/^n) by A4,A7 ,Th23 .= L~(f|n) \/ (LSeg((f|n)/.len(f|n),(f/^n)/.1) \/ L~(f/^n)) by XBOOLE_1:4 .= L~(f|n) \/ L~(<*(f|n)/.len(f|n)*>^(f/^n)) by A4,Th20 .= L~(f|n) \/ L~(f:-q) by A6,FINSEQ_5:def 2 .= L~(f-:q) \/ L~(f:-q) by FINSEQ_5:def 1; end; suppose A8: n = len f; then len(f/^n) = len f - n by RFINSEQ:def 1 .= 0 by A8; then A9: f/^n is empty; f:-q = <*q*>^(f/^n) by FINSEQ_5:def 2 .= <*q*> by A9,FINSEQ_1:34; then A10: L~(f:-q) is empty by Th12; L~f = L~(f|n) by A8,FINSEQ_1:58 .= L~(f-:q) by FINSEQ_5:def 1; hence thesis by A10; end; end; theorem Th25: p in LSeg(f,n) implies L~f = L~Ins(f,n,p) proof set f1 = f|n, g1 = f1^<*p*>, f2 = f/^n; A1: g1/.len g1 = g1/.(len f1 + 1) by FINSEQ_2:16 .= p by FINSEQ_4:67; assume A2: p in LSeg(f,n); then A3: n+1 <= len f by TOPREAL1:def 3; then A4: 1 <= len f - n by XREAL_1:19; A5: n <= n+1 by NAT_1:11; then A6: len f1 = n by A3,FINSEQ_1:59,XXREAL_0:2; then A7: f1 is non empty by A2,TOPREAL1:def 3; A8: 1 <= n by A2,TOPREAL1:def 3; then A9: n in dom f1 by A6,FINSEQ_3:25; n <= len f by A3,A5,XXREAL_0:2; then 1 <= len f2 by A4,RFINSEQ:def 1; then A10: 1 in dom f2 by FINSEQ_3:25; A11: LSeg(f,n) = LSeg(f/.n,f/.(n+1)) by A8,A3,TOPREAL1:def 3 .= LSeg(f1/.len f1,f/.(n+1)) by A6,A9,FINSEQ_4:70 .= LSeg(f1/.len f1,f2/.1) by A10,FINSEQ_5:27; thus L~Ins(f,n,p) = L~(g1^f2) by FINSEQ_5:def 4 .= L~g1 \/ LSeg(g1/.len g1,f2/.1) \/ L~f2 by A10,Th23,RELAT_1:38 .= L~f1 \/ LSeg(f1/.len f1,p) \/ LSeg(g1/.len g1,f2/.1) \/ L~f2 by A9,Th19, RELAT_1:38 .= L~f1 \/ (LSeg(f1/.len f1,p) \/ LSeg(g1/.len g1,f2/.1)) \/ L~f2 by XBOOLE_1:4 .= L~f1 \/ LSeg(f1/.len f1,f2/.1) \/ L~f2 by A2,A1,A11,TOPREAL1:5 .= L~(f1^f2) by A7,A10,Th23,RELAT_1:38 .= L~f by RFINSEQ:8; end; begin registration cluster being_S-Seq for FinSequence of TOP-REAL 2; existence proof set p = |[ 0,0 ]|, q = |[ 1,1 ]|; A1: p`2 = 0 by EUCLID:52; A2: q`1 = 1 by EUCLID:52; A3: q`2 = 1 by EUCLID:52; p`1 = 0 by EUCLID:52; then <* p,|[p`1,q`2]|,q *> is being_S-Seq by A1,A2,A3,TOPREAL3:34; hence thesis; end; cluster being_S-Seq -> one-to-one unfolded s.n.c. special non trivial for FinSequence of TOP-REAL 2; coherence proof let f; assume A4: f is being_S-Seq; then len f >= 2 by TOPREAL1:def 8; hence thesis by A4,NAT_D:60,TOPREAL1:def 8; end; cluster one-to-one unfolded s.n.c. special non trivial -> being_S-Seq for FinSequence of TOP-REAL 2; coherence proof let f; assume A5: f is one-to-one unfolded s.n.c. special; assume f is non trivial; then len f >= 2 by NAT_D:60; hence thesis by A5,TOPREAL1:def 8; end; cluster being_S-Seq -> non empty for FinSequence of TOP-REAL 2; coherence by CARD_1:27,TOPREAL1:def 8; end; registration cluster one-to-one unfolded s.n.c. special non trivial for FinSequence of TOP-REAL 2; existence proof set f = the being_S-Seq FinSequence of TOP-REAL 2; f is one-to-one unfolded s.n.c. special non trivial; hence thesis; end; end; theorem Th26: len f <= 2 implies f is unfolded proof assume A1: len f <= 2; let i be Nat such that A2: 1 <= i; assume i+2 <= len f; then i+2 <= 2 by A1,XXREAL_0:2; then i <= 2-2 by XREAL_1:19; hence thesis by A2,XXREAL_0:2; end; Lm2: <*p,q*> is unfolded proof len <*p,q*> = 2 by FINSEQ_1:44; hence thesis by Th26; end; Lm3: f is unfolded implies f|n is unfolded proof assume A1: f is unfolded; set h = f|n; let i be Nat such that A2: 1 <= i and A3: i + 2 <= len h; A4: i+1 in dom h by A2,A3,SEQ_4:135; len h <= len f by FINSEQ_5:16; then A5: i+2 <= len f by A3,XXREAL_0:2; A6: i+1+1 = i+(1+1); i+1 <= i+2 by XREAL_1:6; hence LSeg(h,i) /\ LSeg(h,i+1) = LSeg(f,i) /\ LSeg(h,i+1) by A3,Th3, XXREAL_0:2 .= LSeg(f,i) /\ LSeg(f,i+1) by A3,A6,Th3 .= {f/.(i+1)} by A1,A2,A5,TOPREAL1:def 6 .= {h/.(i+1)} by A4,FINSEQ_4:70; end; Lm4: f is unfolded implies f/^n is unfolded proof assume A1: f is unfolded; per cases; suppose A2: n <= len f; set h = f/^n; let i be Nat such that A3: 1 <= i and A4: i + 2 <= len h; A5: i+1 in dom h by A3,A4,SEQ_4:135; A6: len h = len f - n by A2,RFINSEQ:def 1; then n+(i+2) <= len f by A4,XREAL_1:19; then A7: n+i+2 <= len f; i <= n+i by NAT_1:11; then A8: 1 <= n+i by A3,XXREAL_0:2; A9: i+1+1 = i+(1+1); i+1 <= i+2 by XREAL_1:6; then i+1 <= len h by A4,XXREAL_0:2; hence LSeg(h,i) /\ LSeg(h,i+1) = LSeg(f,n+i) /\ LSeg(h,i+1) by A3,A6,Th5 .= LSeg(f,n+i) /\ LSeg(f,n+(i+1)) by A4,A9,A6,Th5,NAT_1:11 .= {f/.(n+i+1)} by A1,A7,A8,TOPREAL1:def 6 .= {f/.(n+(i+1))} .= {h/.(i+1)} by A5,FINSEQ_5:27; end; suppose n > len f; then f/^n = <*>(the carrier of TOP-REAL 2) by RFINSEQ:def 1; then len(f/^n) = 0; hence thesis by Th26; end; end; registration let f be unfolded FinSequence of TOP-REAL 2, n; cluster f|n -> unfolded for FinSequence of TOP-REAL 2; coherence by Lm3; cluster f/^n -> unfolded for FinSequence of TOP-REAL 2; coherence by Lm4; end; theorem Th27: p in rng f & f is unfolded implies f:-p is unfolded proof assume p in rng f; then ex i st i+1 = p..f & f:-p = f/^i by FINSEQ_5:49; hence thesis; end; Lm5: f is unfolded implies f-:p is unfolded proof f-:p = f|(p..f) by FINSEQ_5:def 1; hence thesis; end; registration let f be unfolded FinSequence of TOP-REAL 2, p; cluster f-:p -> unfolded; coherence by Lm5; end; theorem Th28: f is unfolded implies Rev f is unfolded proof assume A1: f is unfolded; A2: dom f = Seg len f by FINSEQ_1:def 3; let i be Nat such that A3: 1 <= i and A4: i + 2 <= len Rev f; A5: len Rev f = len f by FINSEQ_5:def 3; then A6: i+1 in dom f by A3,A4,SEQ_4:135; i+1 <= i+1+1 by NAT_1:11; then reconsider j9 = len f - (i+1) as Element of NAT by A4,A5,INT_1:5 ,XXREAL_0:2; i <= i+2 by NAT_1:11; then reconsider j = len f - i as Element of NAT by A4,A5,INT_1:5,XXREAL_0:2; A7: j9+(i+1) = len f; i in dom f by A3,A4,A5,SEQ_4:135; then j + 1 in dom f by A2,FINSEQ_5:2; then A8: j9+2 <= len f by FINSEQ_3:25; A9: j + (i+1) = len f + 1; i+(1+1) = i+1+1; then A10: 1 <= j9 by A4,A5,XREAL_1:19; j+i = len f; hence LSeg(Rev f,i) /\ LSeg(Rev f,i+1) = LSeg(f,j) /\ LSeg(Rev f,i+1) by Th2 .= LSeg(f,j9+1) /\ LSeg(f,j9) by A7,Th2 .= {f/.(j9+1)} by A1,A10,A8,TOPREAL1:def 6 .= {(Rev f)/.(i+1)} by A9,A2,A6,FINSEQ_5:2,66; end; theorem Th29: g is unfolded & LSeg(p,g/.1) /\ LSeg(g,1) = {g/.1} implies <*p*> ^g is unfolded proof set f = <*p*>; A1: len f = 1 by FINSEQ_1:39; A2: f/.1 = p by FINSEQ_4:16; A3: len(f^g) = len f + len g by FINSEQ_1:22; assume that A4: g is unfolded and A5: LSeg(p,g/.1) /\ LSeg(g,1) = {g/.1}; let i be Nat such that A6: 1 <= i and A7: i + 2 <= len(f^g); A8: i+(1+1) = i+1+1; per cases; suppose A9: i = len f; then A10: LSeg(f^g,i+1) = LSeg(g,1) by Th7; now i <= i+1 by NAT_1:11; then A11: i < i+(1+1) by A8,NAT_1:13; assume len g = 0; hence contradiction by A1,A6,A7,A3,A11,XXREAL_0:2; end; then 1 <= len g by NAT_1:14; then A12: 1 in dom g by FINSEQ_3:25; then LSeg(f^g,i) = LSeg(f/.len f,g/.1) by A9,Th8,RELAT_1:38; hence thesis by A1,A5,A2,A9,A12,A10,FINSEQ_4:69; end; suppose A13: i <> len f; reconsider j = i - len f as Element of NAT by A1,A6,INT_1:5; i > len f by A1,A6,A13,XXREAL_0:1; then len f + 1 <= i by NAT_1:13; then A14: 1 <= j by XREAL_1:19; A15: i+2-len f <= len g by A7,A3,XREAL_1:20; then A16: j+(1+1) <= len g; j+1 <= j+1+1 by NAT_1:11; then j+1 <= len g by A15,XXREAL_0:2; then A17: j+1 in dom g by A14,SEQ_4:134; A18: len f + (j+1) = i+1; len f + j = i; hence LSeg(f^g,i) /\ LSeg(f^g,i+1) = LSeg(g,j) /\ LSeg(f^g,i+1) by A14,Th7 .= LSeg(g,j) /\ LSeg(g,j+1) by A18,Th7,NAT_1:11 .= {g/.(j+1)} by A4,A14,A16,TOPREAL1:def 6 .= {(f^g)/.(i+1)} by A18,A17,FINSEQ_4:69; end; end; theorem Th30: f is unfolded & k+1 = len f & LSeg(f,k) /\ LSeg(f/.len f,p) = {f /.len f} implies f^<*p*> is unfolded proof set g = <*p*>; assume that A1: f is unfolded and A2: k+1 = len f and A3: LSeg(f,k) /\ LSeg(f/.len f,p) = {f/.len f}; A4: len g = 1 by FINSEQ_1:39; A5: g/.1 = p by FINSEQ_4:16; A6: len(f^g) = len f + len g by FINSEQ_1:22; let i be Nat such that A7: 1 <= i and A8: i + 2 <= len(f^g); A9: i+(1+1) = i+1+1; per cases; suppose A10: i+2 <= len f; then A11: i+1 in dom f by A7,SEQ_4:135; i+1 <= i+1+1 by NAT_1:11; hence LSeg(f^g,i) /\ LSeg(f^g,i+1) = LSeg(f,i) /\ LSeg(f^g,i+1) by A10,Th6, XXREAL_0:2 .= LSeg(f,i) /\ LSeg(f,i+1) by A9,A10,Th6 .= {f/.(i+1)} by A1,A7,A10,TOPREAL1:def 6 .= {(f^g)/.(i+1)} by A11,FINSEQ_4:68; end; suppose i + 2 > len f; then A12: len f <= i+1 by A9,NAT_1:13; A13: f is non empty by A4,A8,A6,A9,XREAL_1:6; then A14: len f in dom f by FINSEQ_5:6; i+1 <= len f by A4,A8,A6,A9,XREAL_1:6; then A15: i+1 = len f by A12,XXREAL_0:1; then A16: LSeg(f^g,i+1) = LSeg(f/.len f,g/.1) by A13,Th8; LSeg(f^g,i) = LSeg(f,k) by A2,A15,Th6; hence thesis by A3,A5,A15,A16,A14,FINSEQ_4:68; end; end; theorem Th31: f is unfolded & g is unfolded & k+1 = len f & LSeg(f,k) /\ LSeg( f/.len f,g/.1) = {f/.len f} & LSeg(f/.len f,g/.1) /\ LSeg(g,1) = {g/.1} implies f^g is unfolded proof assume that A1: f is unfolded and A2: g is unfolded and A3: k+1 = len f and A4: LSeg(f,k) /\ LSeg(f/.len f,g/.1) = {f/.len f} and A5: LSeg(f/.len f,g/.1) /\ LSeg(g,1) = {g/.1}; let i be Nat such that A6: 1 <= i and A7: i + 2 <= len(f^g); A8: len(f^g) = len f + len g by FINSEQ_1:22; per cases; suppose A9: i+2 <= len f; then A10: i+1 in dom f by A6,SEQ_4:135; A11: i+(1+1) = i+1+1; i+1 <= i+1+1 by NAT_1:11; hence LSeg(f^g,i) /\ LSeg(f^g,i+1) = LSeg(f,i) /\ LSeg(f^g,i+1) by A9,Th6, XXREAL_0:2 .= LSeg(f,i) /\ LSeg(f,i+1) by A9,A11,Th6 .= {f/.(i+1)} by A1,A6,A9,TOPREAL1:def 6 .= {(f^g)/.(i+1)} by A10,FINSEQ_4:68; end; suppose A12: i + 2 > len f; A13: i+(1+1) = i+1+1; now per cases; suppose A14: i <= len f; len g <> 0 by A7,A8,A12; then 1 <= len g by NAT_1:14; then A15: 1 in dom g by FINSEQ_3:25; A16: f is non empty by A6,A14; now per cases; suppose A17: i = len f; then A18: LSeg(f^g,i+1) = LSeg(g,1) by Th7; LSeg(f^g,i) = LSeg(f/.len f,g/.1) by A16,A15,A17,Th8,RELAT_1:38; hence thesis by A5,A15,A17,A18,FINSEQ_4:69; end; suppose i <> len f; then i < len f by A14,XXREAL_0:1; then A19: i+1 <= len f by NAT_1:13; len f <= i+1 by A12,A13,NAT_1:13; then A20: i+1 = len f by A19,XXREAL_0:1; then A21: LSeg(f^g,i) = LSeg(f,k) by A3,Th6; A22: len f in dom f by A16,FINSEQ_5:6; LSeg(f^g,i+1) = LSeg(f/.len f,g/.1) by A16,A15,A20,Th8,RELAT_1:38; hence thesis by A4,A20,A21,A22,FINSEQ_4:68; end; end; hence thesis; end; suppose A23: i > len f; then reconsider j = i - len f as Element of NAT by INT_1:5; len f + 1 <= i by A23,NAT_1:13; then A24: 1 <= j by XREAL_1:19; A25: i+2-len f <= len g by A7,A8,XREAL_1:20; then A26: j+(1+1) <= len g; j+1 <= j+1+1 by NAT_1:11; then j+1 <= len g by A25,XXREAL_0:2; then A27: j+1 in dom g by A24,SEQ_4:134; A28: len f + (j+1) = i+1; len f + j = i; hence LSeg(f^g,i) /\ LSeg(f^g,i+1) = LSeg(g,j) /\ LSeg(f^g,i+1) by A24 ,Th7 .= LSeg(g,j) /\ LSeg(g,j+1) by A28,Th7,NAT_1:11 .= {g/.(j+1)} by A2,A24,A26,TOPREAL1:def 6 .= {(f^g)/.(i+1)} by A28,A27,FINSEQ_4:69; end; end; hence thesis; end; end; theorem Th32: f is unfolded & p in LSeg(f,n) implies Ins(f,n,p) is unfolded proof assume that A1: f is unfolded and A2: p in LSeg(f,n); set f1 = f|n, g1 = f1^<*p*>, f2 = f/^n; A3: n+1 <= len f by A2,TOPREAL1:def 3; A4: n <= n+1 by NAT_1:11; then A5: len f1 = n by A3,FINSEQ_1:59,XXREAL_0:2; then A6: n+1 = len g1 by FINSEQ_2:16; A7: n <= len f by A3,A4,XXREAL_0:2; 1 <= len f - n by A3,XREAL_1:19; then A8: 1 <= len f2 by A7,RFINSEQ:def 1; then 1 in dom f2 by FINSEQ_3:25; then A9: f/.(n+1) = f2/.1 by FINSEQ_5:27; A10: 1 <= n by A2,TOPREAL1:def 3; then A11: LSeg(f,n) = LSeg(f/.n,f/.(n+1)) by A3,TOPREAL1:def 3; A12: n in dom f1 by A10,A5,FINSEQ_3:25; then A13: f/.n = f1/.len f1 by A5,FINSEQ_4:70; A14: g1/.len g1 = g1/.(len f1 + 1) by FINSEQ_2:16 .= p by FINSEQ_4:67; then A15: LSeg(f1/.len f1,p) \/ LSeg(g1/.len g1,f2/.1) = LSeg(f1/.len f1,f2/.1) by A2,A11,A13,A9,TOPREAL1:5; A16: now len f1 <> 0 by A2,A5,TOPREAL1:def 3; then consider k be Nat such that A17: k+1 = len f1 by NAT_1:6; reconsider k as Element of NAT by ORDINAL1:def 12; A18: k+(1+1) <= len f by A3,A5,A17; per cases; suppose k <> 0; then A19: 1 <= k by NAT_1:14; LSeg(f1,k) = LSeg(f,k) by A17,Th3; then A20: LSeg(f1,k) /\ LSeg(f,n) = {f/.n} by A1,A5,A17,A18,A19,TOPREAL1:def 6; now let x be set; hereby assume A21: x in LSeg(f1,k) /\ LSeg(f1/.len f1,p); then x in LSeg(f1/.len f1,p) by XBOOLE_0:def 4; then A22: x in LSeg(f,n) by A11,A13,A9,A15,XBOOLE_0:def 3; x in LSeg(f1,k) by A21,XBOOLE_0:def 4; then x in LSeg(f1,k) /\ LSeg(f,n) by A22,XBOOLE_0:def 4; hence x = f/.n by A20,TARSKI:def 1; end; assume A23: x = f/.n; then x in LSeg(f1,k) /\ LSeg(f,n) by A20,TARSKI:def 1; then A24: x in LSeg(f1,k) by XBOOLE_0:def 4; x in LSeg(f1/.len f1,p) by A13,A23,RLTOPSP1:68; hence x in LSeg(f1,k) /\ LSeg(f1/.len f1,p) by A24,XBOOLE_0:def 4; end; then LSeg(f1,k) /\ LSeg(f1/.len f1,p) = {f1/.len f1} by A13,TARSKI:def 1; hence g1 is unfolded by A1,A17,Th30; end; suppose k = 0; then len g1 = 1+1 by A17,FINSEQ_2:16; hence g1 is unfolded by Th26; end; end; f1/.len f1 = g1/.n by A5,A12,FINSEQ_4:68; then LSeg(g1,n) = LSeg(f1/.len f1,g1/.len g1) by A10,A6,TOPREAL1:def 3; then A25: LSeg(g1,n) /\ LSeg(g1/.len g1,f2/.1) = {g1/.len g1} by A2,A14,A11,A13,A9, TOPREAL1:8; now per cases; suppose len f2 = 1; then f2 = <*f2/.1*> by FINSEQ_5:14; hence g1^f2 is unfolded by A16,A6,A25,Th30; end; suppose len f2 <> 1; then len f2 > 1 by A8,XXREAL_0:1; then A26: 1+1 <= len f2 by NAT_1:13; then LSeg(f2,1) = LSeg(f2/.1,f2/.(1+1)) by TOPREAL1:def 3; then A27: f2/.1 in LSeg(f2,1) by RLTOPSP1:68; A28: 1+1 <= len f - n by A7,A26,RFINSEQ:def 1; then n+(1+1) <= len f by XREAL_1:19; then A29: {f/.(n+1)} = LSeg(f,n) /\ LSeg(f,n+1) by A1,A10,TOPREAL1:def 6 .= LSeg(f,n) /\ LSeg(f2,1) by A28,Th5; now let x be set; hereby assume A30: x in LSeg(g1/.len g1,f2/.1) /\ LSeg(f2,1); then x in LSeg(g1/.len g1,f2/.1) by XBOOLE_0:def 4; then A31: x in LSeg(f,n) by A11,A13,A9,A15,XBOOLE_0:def 3; x in LSeg(f2,1) by A30,XBOOLE_0:def 4; then x in LSeg(f,n) /\ LSeg(f2,1) by A31,XBOOLE_0:def 4; hence x = f2/.1 by A9,A29,TARSKI:def 1; end; assume A32: x = f2/.1; then x in LSeg(g1/.len g1,f2/.1) by RLTOPSP1:68; hence x in LSeg(g1/.len g1,f2/.1) /\ LSeg(f2,1) by A27,A32, XBOOLE_0:def 4; end; then LSeg(g1/.len g1,f2/.1) /\ LSeg(f2,1) = {f2/.1} by TARSKI:def 1; hence g1^f2 is unfolded by A1,A16,A6,A25,Th31; end; end; hence thesis by FINSEQ_5:def 4; end; theorem Th33: len f <= 2 implies f is s.n.c. proof assume A1: len f <= 2; let i,j be Nat such that A2: i+1 < j; now assume that A3: 1 <= i and A4: i+1 <= len f and A5: 1 <= j and A6: j+1 <= len f; j+1 <= 1+1 by A1,A6,XXREAL_0:2; then j <= 1 by XREAL_1:6; then A7: j = 1 by A5,XXREAL_0:1; i+1 <= 1+1 by A1,A4,XXREAL_0:2; then i <= 1 by XREAL_1:6; then i = 1 by A3,XXREAL_0:1; hence contradiction by A2,A7; end; then LSeg(f,i) = {} or LSeg(f,j) = {} by TOPREAL1:def 3; hence LSeg(f,i) /\ LSeg(f,j) = {}; end; Lm6: <*p,q*> is s.n.c. proof len <*p,q*> = 2 by FINSEQ_1:44; hence thesis by Th33; end; Lm7: f is s.n.c. implies f|n is s.n.c. proof assume A1: f is s.n.c.; let i,j be Nat such that A2: i+1 < j; per cases; suppose A3: i = 0 or j+1 > len(f|n); now per cases by A3; case i = 0; hence LSeg(f|n,i) = {} by TOPREAL1:def 3; end; case j+1 > len(f|n); hence LSeg(f|n,j) = {} by TOPREAL1:def 3; end; end; then LSeg(f|n,i) /\ LSeg(f|n,j) = {}; hence thesis by XBOOLE_0:def 7; end; suppose that i <> 0 and A4: j+1 <= len(f|n); A5: LSeg(f,i) misses LSeg(f,j) by A1,A2,TOPREAL1:def 7; j <= j+1 by NAT_1:11; then i+1 < j+1 by A2,XXREAL_0:2; then LSeg(f|n,i) /\ LSeg(f|n,j) = LSeg(f,i) /\ LSeg(f|n,j) by A4,Th3, XXREAL_0:2 .= LSeg(f,i) /\ LSeg(f,j) by A4,Th3 .= {} by A5,XBOOLE_0:def 7; hence thesis by XBOOLE_0:def 7; end; end; Lm8: f is s.n.c. implies f/^n is s.n.c. proof assume A1: f is s.n.c.; per cases; suppose A2: n <= len f; let i,j be Nat such that A3: i+1 < j; now per cases; suppose A4: i = 0 or j+1 > len(f/^n); now per cases by A4; case i = 0; hence LSeg(f/^n,i) = {} by TOPREAL1:def 3; end; case j+1 > len(f/^n); hence LSeg(f/^n,j) = {} by TOPREAL1:def 3; end; end; then LSeg(f/^n,i) /\ LSeg(f/^n,j) = {}; hence thesis by XBOOLE_0:def 7; end; suppose that A5: i <> 0 and A6: j+1 <= len(f/^n); A7: i <= j by A3,NAT_1:13; 1 <= i by A5,NAT_1:14; then A8: 1 <= j by A7,XXREAL_0:2; n+(i+1) < n+j by A3,XREAL_1:6; then n+i+1 < n+j; then A9: LSeg(f,n+i) misses LSeg(f,n+j) by A1,TOPREAL1:def 7; A10: len(f/^n) = len f - n by A2,RFINSEQ:def 1; j <= j+1 by NAT_1:11; then i+1 < j+1 by A3,XXREAL_0:2; then i+1 <= len(f/^n) by A6,XXREAL_0:2; then LSeg(f/^n,i) /\ LSeg(f/^n,j) = LSeg(f,n+i) /\ LSeg(f/^n,j) by A5,A10 ,Th5,NAT_1:14 .= LSeg(f,n+i) /\ LSeg(f,n+j) by A6,A10,A8,Th5 .= {} by A9,XBOOLE_0:def 7; hence thesis by XBOOLE_0:def 7; end; end; hence thesis; end; suppose n > len f; then f/^n = <*>(the carrier of TOP-REAL 2) by RFINSEQ:def 1; then len(f/^n) = 0; hence thesis by Th33; end; end; registration let f be s.n.c. FinSequence of TOP-REAL 2, n; cluster f|n -> s.n.c. for FinSequence of TOP-REAL 2; coherence by Lm7; cluster f/^n -> s.n.c. for FinSequence of TOP-REAL 2; coherence by Lm8; end; Lm9: f is s.n.c. implies f-:p is s.n.c. proof f-:p = f|(p..f) by FINSEQ_5:def 1; hence thesis; end; registration let f be s.n.c. FinSequence of TOP-REAL 2, p; cluster f-:p -> s.n.c.; coherence by Lm9; end; theorem Th34: p in rng f & f is s.n.c. implies f:-p is s.n.c. proof assume p in rng f; then ex i st i+1 = p..f & f:-p = f/^i by FINSEQ_5:49; hence thesis; end; theorem Th35: f is s.n.c. implies Rev f is s.n.c. proof assume A1: f is s.n.c.; let i,j be Nat such that A2: i+1 < j; per cases; suppose A3: i = 0 or j+1 > len(Rev f); now per cases by A3; case i = 0; hence LSeg(Rev f,i) = {} by TOPREAL1:def 3; end; case j+1 > len(Rev f); hence LSeg(Rev f,j) = {} by TOPREAL1:def 3; end; end; then LSeg(Rev f,i) /\ LSeg(Rev f,j) = {}; hence thesis by XBOOLE_0:def 7; end; suppose that i <> 0 and A4: j+1 <= len(Rev f); A5: j <= j+1 by NAT_1:11; i <= i+1 by NAT_1:11; then A6: i < j by A2,XXREAL_0:2; A7: len Rev f = len f by FINSEQ_5:def 3; then reconsider j9 = len f - j as Element of NAT by A4,A5,INT_1:5 ,XXREAL_0:2; j <= len f by A4,A7,A5,XXREAL_0:2; then reconsider i9 = len f - i as Element of NAT by A6,INT_1:5,XXREAL_0:2; A8: j9+j = len f; len f - (i+1) > j9 by A2,XREAL_1:10; then i9 - 1 + 1 > j9+1 by XREAL_1:6; then A9: LSeg(f,i9) misses LSeg(f,j9) by A1,TOPREAL1:def 7; i9+i = len f; hence LSeg(Rev f,i) /\ LSeg(Rev f,j) = LSeg(f,i9) /\ LSeg(Rev f,j) by Th2 .= LSeg(f,i9) /\ LSeg(f,j9) by A8,Th2 .= {} by A9,XBOOLE_0:def 7; end; end; theorem Th36: f is s.n.c. & g is s.n.c. & L~f misses L~g & (for i st 1<=i & i+ 2 <= len f holds LSeg(f,i) misses LSeg(f/.len f,g/.1)) & (for i st 2<=i & i+1 <= len g holds LSeg(g,i) misses LSeg(f/.len f,g/.1)) implies f^g is s.n.c. proof assume that A1: f is s.n.c. and A2: g is s.n.c. and A3: L~f /\ L~g = {} and A4: for i st 1<=i & i+2<= len f holds LSeg(f,i) misses LSeg(f/.len f,g/. 1) and A5: for i st 2<=i & i+1 <= len g holds LSeg(g,i) misses LSeg(f/.len f,g /.1); let i,j be Nat such that A6: i+1 < j; per cases; suppose A7: i = 0 or j+1 > len(f^g); now per cases by A7; case i = 0; hence LSeg(f^g,i) = {} by TOPREAL1:def 3; end; case j+1 > len(f^g); hence LSeg(f^g,j) = {} by TOPREAL1:def 3; end; end; then LSeg(f^g,i) /\ LSeg(f^g,j) = {}; hence thesis by XBOOLE_0:def 7; end; suppose that A8: i <> 0 and A9: j+1 <= len(f^g); A10: len(f^g) = len f + len g by FINSEQ_1:22; i <= i+1 by NAT_1:11; then A11: i < j by A6,XXREAL_0:2; A12: 1 <= i by A8,NAT_1:14; now per cases; suppose A13: j+1 <= len f; j <= j+1 by NAT_1:11; then i < j+1 by A11,XXREAL_0:2; then i < len f by A13,XXREAL_0:2; then i+1 <= len f by NAT_1:13; then A14: LSeg(f^g,i) = LSeg(f,i) by Th6; LSeg(f^g,j) = LSeg(f,j) by A13,Th6; hence thesis by A1,A6,A14,TOPREAL1:def 7; end; suppose j+1 > len f; then A15: len f <= j by NAT_1:13; then reconsider j9 = j - len f as Element of NAT by INT_1:5; j+1-len f <= len g by A9,A10,XREAL_1:20; then A16: j9+1 <= len g; A17: len f + j9 = j; now per cases; suppose A18: i <= len f; then A19: f is non empty by A12; now per cases; suppose A20: i = len f; g is non empty by A16; then A21: LSeg(f^g,i) = LSeg(f/.len f,g/.1) by A19,A20,Th8; len f +1+1 <= j by A6,A20,NAT_1:13; then len f +(1+1) <= j; then A22: 1+1 <= j9 by XREAL_1:19; then LSeg(f^g,j) = LSeg(g,j9) by A17,Th7,XXREAL_0:2; hence thesis by A5,A16,A22,A21; end; suppose i <> len f; then i < len f by A18,XXREAL_0:1; then i+1 <= len f by NAT_1:13; then A23: LSeg(f^g,i) = LSeg(f,i) by Th6; now per cases; suppose A24: j = len f; then i+1+1 <= len f by A6,NAT_1:13; then A25: i+(1+1) <= len f; g is non empty by A9,A10,A24,XREAL_1:6; then A26: LSeg(f^g,j) = LSeg(f/.len f,g/.1) by A19,A24,Th8; i in NAT by ORDINAL1:def 12; hence thesis by A4,A8,A23,A25,A26,NAT_1:14; end; suppose j <> len f; then len f < j by A15,XXREAL_0:1; then len f+1 <= j by NAT_1:13; then 1 <= j9 by XREAL_1:19; then LSeg(f^g,len f+j9) = LSeg(g,j9) by Th7; then A27: LSeg(f^g,j) c= L~g by TOPREAL3:19; LSeg(f^g,i) c= L~f by A23,TOPREAL3:19; then LSeg(f^g,i) /\ LSeg(f^g,j) = {} by A3,A27,XBOOLE_1:3 ,27; hence thesis by XBOOLE_0:def 7; end; end; hence thesis; end; end; hence thesis; end; suppose A28: i > len f; then j <> len f by A6,NAT_1:13; then len f < j by A15,XXREAL_0:1; then len f+1 <= j by NAT_1:13; then 1 <= j9 by XREAL_1:19; then A29: LSeg(f^g,len f+j9) = LSeg(g,j9) by Th7; reconsider i9 = i - len f as Element of NAT by A28,INT_1:5; len f + 1 <= i by A28,NAT_1:13; then 1 <= i9 by XREAL_1:19; then A30: LSeg(f^g,len f+i9) = LSeg(g,i9) by Th7; i+1-len f < j9 by A6,XREAL_1:9; then i9+1 < j9; hence thesis by A2,A30,A29,TOPREAL1:def 7; end; end; hence thesis; end; end; hence thesis; end; end; theorem Th37: f is unfolded s.n.c. & p in LSeg(f,n) & not p in rng f implies Ins(f,n,p) is s.n.c. proof assume that A1: f is unfolded and A2: f is s.n.c. and A3: p in LSeg(f,n) and A4: not p in rng f; set fp = Ins(f,n,p); let i,j be Nat such that A5: i+1 < j; per cases; suppose A6: i = 0 or j+1 > len fp; now per cases by A6; case i = 0; hence LSeg(fp,i) = {} by TOPREAL1:def 3; end; case j+1 > len fp; hence LSeg(fp,j) = {} by TOPREAL1:def 3; end; end; then LSeg(fp,i) /\ LSeg(fp,j) = {}; hence thesis by XBOOLE_0:def 7; end; suppose that A7: i <> 0 and A8: j+1 <= len fp; A9: 1 <= i by A7,NAT_1:14; set f1 = f|n, g1 = f1^<*p*>, f2 = f/^n; A10: fp = g1^f2 by FINSEQ_5:def 4; i <= i+1 by NAT_1:11; then A11: i < j by A5,XXREAL_0:2; A12: i+1 <= i+1+1 by NAT_1:11; A13: len fp = len f + 1 by FINSEQ_5:69; A14: 1 <= n by A3,TOPREAL1:def 3; A15: n+1 <= len f by A3,TOPREAL1:def 3; A16: len g1 = len f1 + 1 by FINSEQ_2:16; then A17: g1/.len g1 = p by FINSEQ_4:67; A18: n <= n+1 by NAT_1:11; then A19: n <= len f by A15,XXREAL_0:2; A20: len f1 = n by A15,A18,FINSEQ_1:59,XXREAL_0:2; i+1+1 <= j by A5,NAT_1:13; then i+1+1+1 <= j+1 by XREAL_1:6; then A21: i+1+1+1 <= len f + 1 by A8,A13,XXREAL_0:2; then i+1+1 <= len f by XREAL_1:6; then A22: i+1 <= len f by A12,XXREAL_0:2; now per cases; suppose A23: j+1 <= n; then A24: LSeg(fp,j) = LSeg(g1,j) by A10,A16,A18,A20,Th6,XXREAL_0:2 .= LSeg(f1,j) by A20,A23,Th6 .= LSeg(f,j) by A20,A23,Th3; j <= j+1 by NAT_1:11; then i < j+1 by A11,XXREAL_0:2; then i < n by A23,XXREAL_0:2; then A25: i+1 <= n by NAT_1:13; then LSeg(fp,i) = LSeg(g1,i) by A10,A16,A18,A20,Th6,XXREAL_0:2 .= LSeg(f1,i) by A20,A25,Th6 .= LSeg(f,i) by A20,A25,Th3; hence thesis by A2,A5,A24,TOPREAL1:def 7; end; suppose j+1 > n; then A26: n <= j by NAT_1:13; now per cases; suppose A27: i <= n+1; A28: 1 <= n+1 by NAT_1:11; 1 <= len f - n by A15,XREAL_1:19; then 1 <= len f2 by A19,RFINSEQ:def 1; then 1 in dom f2 by FINSEQ_3:25; then A29: f/.(n+1) = f2/.1 by FINSEQ_5:27; len g1 in dom g1 by FINSEQ_5:6; then A30: fp/.(n+1) = g1/.len g1 by A10,A16,A20,FINSEQ_4:68; A31: fp/.(n+1+1) = f/.(n+1) by A15,FINSEQ_5:74; A32: n in dom f1 by A14,A20,FINSEQ_3:25; then A33: f/.n = f1/.len f1 by A20,FINSEQ_4:70; n+1+1 <= len fp by A13,A15,XREAL_1:6; then A34: LSeg(fp,n+1) = LSeg(p,f2/.1) by A17,A29,A31,A28,A30,TOPREAL1:def 3; A35: f1/.len f1 = g1/.len f1 by A20,A32,FINSEQ_4:68; A36: LSeg(fp,n) = LSeg(g1,n) by A10,A16,A20,Th6 .= LSeg(f1/.len f1,p) by A16,A17,A14,A20,A35,TOPREAL1:def 3; A37: LSeg(f,n) = LSeg(f/.n,f/.(n+1)) by A14,A15,TOPREAL1:def 3; then A38: LSeg(f1/.len f1,p) \/ LSeg(g1/.len g1,f2/.1) = LSeg(f1/.len f1,f2/.1) by A3,A17,A33,A29,TOPREAL1:5; A39: LSeg(f1/.len f1,p) /\ LSeg(p,f2/.1) = {p} by A3,A37,A33,A29, TOPREAL1:8; now per cases by XXREAL_0:1; suppose i < n; then A40: i+1 <= n by NAT_1:13; then A41: LSeg(fp,i) = LSeg(g1,i) by A10,A16,A18,A20,Th6,XXREAL_0:2 .= LSeg(f1,i) by A20,A40,Th6 .= LSeg(f,i) by A20,A40,Th3; now per cases; suppose A42: j = n; then A43: LSeg(f,i) misses LSeg(f,n) by A2,A5,TOPREAL1:def 7; LSeg(fp,i) /\ LSeg(fp,j) c= LSeg(f,i) /\ LSeg(f,n) by A37 ,A33,A29,A38,A36,A41,A42,XBOOLE_1:7,26; then LSeg(fp,i) /\ LSeg(fp,j) c= {} by A43,XBOOLE_0:def 7; then LSeg(fp,i) /\ LSeg(fp,j) = {} by XBOOLE_1:3; hence thesis by XBOOLE_0:def 7; end; suppose j <> n; then n < j by A26,XXREAL_0:1; then A44: n+1 <= j by NAT_1:13; now per cases; suppose A45: j = n+1; now per cases; suppose A46: i+1 = n; A47: i+(1+1) <= len f by A21,XREAL_1:6; LSeg(fp,i) = LSeg( g1,i) by A10,A16,A20,A46,Th6, NAT_1:11 .= LSeg(f1,i) by A20,A46,Th6 .= LSeg(f,i) by A20,A46,Th3; then A48: LSeg(fp,i) /\ LSeg (f,n) = {f/.n} by A1,A9,A46,A47, TOPREAL1:def 6; assume not thesis; then consider x being set such that A49: x in LSeg(fp,i) /\ LSeg(fp,j) by XBOOLE_0:4; A50: x in LSeg(fp,i) by A49,XBOOLE_0:def 4; A51: x in LSeg(fp,j) by A49,XBOOLE_0:def 4; then x in LSeg(f,n) by A17,A37,A33,A29,A38,A34,A45, XBOOLE_0:def 3; then x in {f/.n} by A48,A50,XBOOLE_0:def 4; then A52: x = f/.n by TARSKI:def 1; then x in LSeg(fp,n) by A33,A36,RLTOPSP1:68; then x in LSeg(fp,n) /\ LSeg(fp,n+1) by A45,A51, XBOOLE_0:def 4; then A53: p = f/.n by A36,A34,A39,A52,TARSKI:def 1; n in dom f by A14,A15,SEQ_4:134; hence contradiction by A4,A53,PARTFUN2:2; end; suppose i+1 <> n; then i+1 < n by A40,XXREAL_0:1; then A54: LSeg(f,i) misses LSeg(f,n) by A2,TOPREAL1:def 7; LSeg(fp,i) /\ LSeg(fp,j) c= LSeg(f,i) /\ LSeg (f,n) by A17,A37,A33,A29,A38,A34,A41,A45,XBOOLE_1:7,26; then LSeg(fp,i) /\ LSeg(fp,j) c= {} by A54, XBOOLE_0:def 7; then LSeg(fp,i) /\ LSeg(fp,j) = {} by XBOOLE_1:3; hence thesis by XBOOLE_0:def 7; end; end; hence thesis; end; suppose A55: j <> n+1; reconsider nj = j-(n+1) as Element of NAT by A44, INT_1:5; A56: n+1 < j by A44,A55,XXREAL_0:1; then n+1+1 <= j by NAT_1:13; then A57: 1 <= nj by XREAL_1:19; reconsider j9 = j - 1 as Element of NAT by A9,A11, INT_1:5,XXREAL_0:2; A58: n+nj = j9; i+1+1 <= n+1 by A40,XREAL_1:6; then i+1+1 < j by A56,XXREAL_0:2; then A59: i+1 < j9 by XREAL_1:20; j = nj+(n+1); then LSeg(fp,j) = LSeg(f2,nj) by A10,A16,A20,A57,Th7 .= LSeg(f,j9) by A19,A57,A58,Th4; hence thesis by A2,A41,A59,TOPREAL1:def 7; end; end; hence thesis; end; end; hence thesis; end; suppose A60: i = n; then reconsider nj = j-(n+1) as Element of NAT by A5,INT_1:5; A61: n+1+1 <= j by A5,A60,NAT_1:13; then A62: 1 <= nj by XREAL_1:19; reconsider j9 = j - 1 as Element of NAT by A9,A11,INT_1:5 ,XXREAL_0:2; A63: n+nj = j9; j = nj+(n+1); then A64: LSeg(fp,j) = LSeg(f2,nj) by A10,A16,A20,A62,Th7 .= LSeg(f,j9) by A19,A62,A63,Th4; now per cases; suppose j <> n+1+1; then n+1+1 < j by A61,XXREAL_0:1; then i+1 < j9 by A60,XREAL_1:20; then A65: LSeg(f,i) misses LSeg(f,j9) by A2,TOPREAL1:def 7; LSeg(fp,i) /\ LSeg(fp,j) c= LSeg(f,i) /\ LSeg(f,j9) by A37,A33,A29,A38,A36,A60,A64,XBOOLE_1:7,26; then LSeg(fp,i) /\ LSeg(fp,j) c= {} by A65,XBOOLE_0:def 7; then LSeg(fp,i) /\ LSeg(fp,j) = {} by XBOOLE_1:3; hence thesis by XBOOLE_0:def 7; end; suppose A66: j = n+1+1; then n+(1+1) <= len f by A8,A13,XREAL_1:6; then A67: LSeg(f,n) /\ LSeg(f,j9) = {f/.j9} by A1,A14,A66, TOPREAL1:def 6; assume not thesis; then consider x being set such that A68: x in LSeg(fp,i) /\ LSeg(fp,j) by XBOOLE_0:4; A69: x in LSeg(fp,j) by A68,XBOOLE_0:def 4; A70: x in LSeg(fp,i) by A68,XBOOLE_0:def 4; then x in LSeg(f,n) by A37,A33,A29,A38,A36,A60, XBOOLE_0:def 3; then x in {f/.(n+1)} by A64,A66,A67,A69,XBOOLE_0:def 4; then A71: x = f/.(n+1) by TARSKI:def 1; then x in LSeg(fp,n+1) by A29,A34,RLTOPSP1:68; then x in LSeg(fp,n) /\ LSeg(fp,n+1) by A60,A70, XBOOLE_0:def 4; then A72: p = f/.(n+1) by A36,A34,A39,A71,TARSKI:def 1; n+1 in dom f by A14,A15,SEQ_4:134; hence contradiction by A4,A72,PARTFUN2:2; end; end; hence thesis; end; suppose A73: i>n; reconsider j9 = j - 1 as Element of NAT by A9,A11,INT_1:5 ,XXREAL_0:2; i>=n+1 by A73,NAT_1:13; then A74: i = n+1 by A27,XXREAL_0:1; then n+1 < j9 by A5,XREAL_1:20; then A75: LSeg(f,n) misses LSeg(f,j9) by A2,TOPREAL1:def 7; n+1 <= n+1+1 by NAT_1:11; then reconsider nj = j-(n+1) as Element of NAT by A5,A74, INT_1:5,XXREAL_0:2; A76: 1 <= nj by A5,A74,XREAL_1:19; A77: n+nj = j9; j = nj+(n+1); then LSeg(fp,j) = LSeg(f2,nj) by A10,A16,A20,A76,Th7 .= LSeg(f,j9) by A19,A76,A77,Th4; then LSeg(fp,n+1) /\ LSeg(fp,j) c= LSeg(f,n) /\ LSeg(f,j9) by A17,A37,A33,A29,A38,A34,XBOOLE_1:7,26; then LSeg(fp,n+1) /\ LSeg(fp,j) c= {} by A75,XBOOLE_0:def 7; then LSeg(fp,n+1) /\ LSeg(fp,j) = {} by XBOOLE_1:3; hence thesis by A74,XBOOLE_0:def 7; end; end; hence thesis; end; suppose A78: i > n+1; then reconsider nj = j-(n+1) as Element of NAT by A11,INT_1:5 ,XXREAL_0:2; n+1 < j by A11,A78,XXREAL_0:2; then n+1+1 <= j by NAT_1:13; then A79: 1 <= nj by XREAL_1:19; reconsider ni = i - (n+1) as Element of NAT by A78,INT_1:5; n+1+1 <= i by A78,NAT_1:13; then A80: 1 <= ni by XREAL_1:19; len f <= len f+1 by NAT_1:11; then i+1 <= len f+1 by A22,XXREAL_0:2; then i+1-(n+1) <= len f+1- (n+1) by XREAL_1:9; then A81: ni+1 <= len f - n; reconsider i9 = i - 1 as Element of NAT by A7,INT_1:5,NAT_1:14; reconsider j9 = j - 1 as Element of NAT by A9,A11,INT_1:5 ,XXREAL_0:2; A82: n+ni = i9; i+1-1 < j9 by A5,XREAL_1:9; then A83: i9+1 < j9; A84: n+nj = j9; j = nj+(n+1); then A85: LSeg(fp,j) = LSeg(f2,nj) by A10,A16,A20,A79,Th7 .= LSeg(f,j9) by A19,A79,A84,Th4; i = ni+(n+1); then LSeg(fp,i) = LSeg(f2,ni) by A10,A16,A20,A80,Th7 .= LSeg(f,i9) by A80,A81,A82,Th5; hence thesis by A2,A83,A85,TOPREAL1:def 7; end; end; hence thesis; end; end; hence thesis; end; end; registration cluster <*>(the carrier of TOP-REAL 2) -> special; coherence proof set f = <*>(the carrier of TOP-REAL 2); let i be Nat such that 1 <= i and A1: i+1 <= len f; thus thesis by A1; end; end; registration let p; cluster <*p*> -> special for FinSequence of TOP-REAL 2; coherence proof set f = <*p*>; f is special proof let i be Nat such that A1: 1 <= i and A2: i+1 <= len f; len f = 0+1 by FINSEQ_1:39; hence thesis by A1,A2,XREAL_1:6; end; hence thesis; end; end; theorem Th38: p`1 = q`1 or p`2 = q`2 implies <*p,q*> is special proof assume A1: p`1 = q`1 or p`2 = q`2; set f = <*p,q*>; let i be Nat such that A2: 1 <= i and A3: i+1 <= len f; len f = 1+1 by FINSEQ_1:44; then i <= 1 by A3,XREAL_1:6; then A4: i = 1 by A2,XXREAL_0:1; then f/.i = p by FINSEQ_4:17; hence thesis by A1,A4,FINSEQ_4:17; end; Lm10: f is special implies f|n is special proof assume A1: f is special; let i be Nat such that A2: 1 <= i and A3: i+1 <= len(f|n); i in dom(f|n) by A2,A3,SEQ_4:134; then A4: (f|n)/.i = f/.i by FINSEQ_4:70; i+1 in dom(f|n) by A2,A3,SEQ_4:134; then A5: (f|n)/.(i+1) = f/.(i+1) by FINSEQ_4:70; len(f|n) <= len f by FINSEQ_5:16; then i+1 <= len f by A3,XXREAL_0:2; hence thesis by A1,A2,A4,A5,TOPREAL1:def 5; end; Lm11: f is special implies f/^n is special proof assume A1: f is special; per cases; suppose A2: n <= len f; let i be Nat such that A3: 1 <= i and A4: i+1 <= len(f/^n); i in dom(f/^n) by A3,A4,SEQ_4:134; then A5: (f/^n)/.i = f/.(n+i) by FINSEQ_5:27; i <= n+i by NAT_1:11; then A6: 1 <= n+i by A3,XXREAL_0:2; i+1 in dom(f/^n) by A3,A4,SEQ_4:134; then A7: (f/^n)/.(i+1) = f/.(n+(i+1)) by FINSEQ_5:27 .= f/.(n+i+1); len(f/^n) = len f - n by A2,RFINSEQ:def 1; then n+(i+1) <= len f by A4,XREAL_1:19; hence thesis by A1,A5,A7,A6,TOPREAL1:def 5; end; suppose n > len f; then f/^n = <*>(the carrier of TOP-REAL 2) by RFINSEQ:def 1; hence thesis; end; end; registration let f be special FinSequence of TOP-REAL 2, n; cluster f|n -> special for FinSequence of TOP-REAL 2; coherence by Lm10; cluster f/^n -> special for FinSequence of TOP-REAL 2; coherence by Lm11; end; theorem Th39: p in rng f & f is special implies f:-p is special proof assume p in rng f; then ex i st i+1 = p..f & f:-p = f/^i by FINSEQ_5:49; hence thesis; end; Lm12: f is special implies f-:p is special proof f-:p = f|(p..f) by FINSEQ_5:def 1; hence thesis; end; registration let f be special FinSequence of TOP-REAL 2, p; cluster f-:p -> special; coherence by Lm12; end; theorem Th40: f is special implies Rev f is special proof assume A1: f is special; A2: len Rev f = len f by FINSEQ_5:def 3; let i be Nat such that A3: 1 <= i and A4: i+1 <= len(Rev f); i <= i+1 by NAT_1:11; then reconsider j = len f - i as Element of NAT by A4,A2,INT_1:5,XXREAL_0:2; j <= len f - 1 by A3,XREAL_1:10; then A5: j+1 <= len f - 1 + 1 by XREAL_1:6; A6: 1+i+j = len f + 1; A7: i+1-i <= j by A4,A2,XREAL_1:9; then j in dom f by A5,SEQ_4:134; then A8: (Rev f)/.(i+1) = f/.j by A6,FINSEQ_5:66; A9: i+(j+1) = len f + 1; j+1 in dom f by A5,A7,SEQ_4:134; then (Rev f)/.i = f/.(j+1) by A9,FINSEQ_5:66; hence thesis by A1,A5,A7,A8,TOPREAL1:def 5; end; Lm13: f is special & g is special & ((f/.len f)`1 = (g/.1)`1 or (f/.len f)`2 = (g/.1)`2) implies f^g is special proof assume that A1: f is special and A2: g is special and A3: (f/.len f)`1 = (g/.1)`1 or (f/.len f)`2 = (g/.1)`2; let i be Nat such that A4: 1 <= i and A5: i+1 <= len(f^g); A6: len(f^g) = len f + len g by FINSEQ_1:22; per cases by XXREAL_0:1; suppose i < len f; then A7: i+1 <= len f by NAT_1:13; then i+1 in dom f by A4,SEQ_4:134; then A8: (f^g)/.(i+1)=f/.(i+1) by FINSEQ_4:68; i in dom f by A4,A7,SEQ_4:134; then (f^g)/.i=f/.i by FINSEQ_4:68; hence thesis by A1,A4,A7,A8,TOPREAL1:def 5; end; suppose A9: i = len f; then i in dom f by A4,FINSEQ_3:25; then A10: (f^g)/.i = f/.i by FINSEQ_4:68; 1 <= len g by A5,A6,A9,XREAL_1:6; then 1 in dom g by FINSEQ_3:25; hence thesis by A3,A9,A10,FINSEQ_4:69; end; suppose A11: i > len f; then reconsider j = i - len f as Element of NAT by INT_1:5; len f + 1 <= i by A11,NAT_1:13; then A12: 1 <= j by XREAL_1:19; A13: len f + (j+1) = i+1; A14: i+1-len f <= len g by A5,A6,XREAL_1:20; then j+1 in dom g by A12,SEQ_4:134; then A15: (f^g)/.(i+1)= g/.(j+1) by A13,FINSEQ_4:69; A16: len f + j = i; j+1 <= len g by A14; then j in dom g by A12,SEQ_4:134; then (f^g)/.i= g/.j by A16,FINSEQ_4:69; hence thesis by A2,A12,A14,A15,TOPREAL1:def 5; end; end; theorem Th41: f is special & p in LSeg(f,n) implies Ins(f,n,p) is special proof assume that A1: f is special and A2: p in LSeg(f,n); A3: n+1 <= len f by A2,TOPREAL1:def 3; then A4: 1 <= len f - n by XREAL_1:19; A5: 1 <= n by A2,TOPREAL1:def 3; then A6: LSeg(f,n) = LSeg(f/.n,f/.(n+1)) by A3,TOPREAL1:def 3; set f1 = f|n, g1 = f1^<*p*>, f2 = f/^n; set p1 = f1/.len f1, p2 = f2/.1; A7: p1 = |[p1`1, p1`2]| by EUCLID:53; A8: n <= n+1 by NAT_1:11; then n <= len f by A3,XXREAL_0:2; then 1 <= len f2 by A4,RFINSEQ:def 1; then 1 in dom f2 by FINSEQ_3:25; then A9: f/.(n+1) = f2/.1 by FINSEQ_5:27; A10: len f1 = n by A3,A8,FINSEQ_1:59,XXREAL_0:2; then n in dom f1 by A5,FINSEQ_3:25; then A11: f/.n = f1/.len f1 by A10,FINSEQ_4:70; then A12: p1`1 = p2`1 or p1`2 = p2`2 by A1,A5,A3,A9,TOPREAL1:def 5; set q1 = g1/.len g1; A13: p2 = |[p2`1, p2`2]| by EUCLID:53; <*p*>/.1 = p by FINSEQ_4:16; then p1`1 = (<*p*>/.1)`1 or p1`2 = (<*p*>/.1)`2 by A2,A6,A11,A9,A12,A7,A13, TOPREAL3:11,12; then A14: g1 is special by A1,Lm13; g1/.len g1 = g1/.(len f1 + 1) by FINSEQ_2:16 .= p by FINSEQ_4:67; then q1`1 = p2`1 or q1`2 = p2`2 by A2,A6,A11,A9,A12,A7,A13,TOPREAL3:11,12; then g1^f2 is special by A1,A14,Lm13; hence thesis by FINSEQ_5:def 4; end; theorem Th42: q in rng f & 1<>q..f & q..f<>len f & f is unfolded s.n.c. implies L~(f-:q) /\ L~(f:-q) = {q} proof assume that A1: q in rng f and A2: 1 <> q..f and A3: q..f <> len f and A4: f is unfolded and A5: f is s.n.c.; A6: (f:-q)/.1 = q by FINSEQ_5:53; q..f <= len f by A1,FINSEQ_4:21; then q..f < len f by A3,XXREAL_0:1; then q..f+1 <= len f by NAT_1:13; then A7: 1 <= len f - q..f by XREAL_1:19; len(f:-q) = len f - q..f + 1 by A1,FINSEQ_5:50; then 1+1<=len(f:-q) by A7,XREAL_1:6; then A8: rng(f:-q) c= L~(f:-q) by Th18; 1 in dom(f:-q) by FINSEQ_5:6; then A9: q in rng(f:-q) by A6,PARTFUN2:2; f-:q is non empty by A1,FINSEQ_5:47; then A10: len(f-:q) in dom(f-:q) by FINSEQ_5:6; A11: len(f-:q) = q..f by A1,FINSEQ_5:42; thus L~(f-:q) /\ L~(f:-q) c= {q} proof let x be set; assume A12: x in L~(f-:q) /\ L~(f:-q); then reconsider p = x as Point of TOP-REAL 2; p in L~(f-:q) by A12,XBOOLE_0:def 4; then consider i such that A13: 1 <= i and A14: i+1 <= len(f-:q) and A15: p in LSeg((f-:q),i) by Th13; A16: LSeg(f-:q,i) = LSeg(f,i) by A14,Th9; p in L~(f:-q) by A12,XBOOLE_0:def 4; then consider j such that A17: 1 <= j and j+1 <= len(f:-q) and A18: p in LSeg((f:-q),j) by Th13; consider j9 being Nat such that A19: j=j9+1 by A17,NAT_1:6; reconsider j9 as Element of NAT by ORDINAL1:def 12; A20: LSeg(f:-q,j) = LSeg(f,j9+q..f) by A1,A19,Th10; per cases; suppose that A21: i+1 = len(f-:q) and A22: j9 = 0; q..f <= len f by A1,FINSEQ_4:21; then q..f < len f by A3,XXREAL_0:1; then i+1+1 <= len f by A11,A21,NAT_1:13; then i+(1+1) <= len f; then LSeg((f-:q),i) /\ LSeg(f:-q,j) = {f/.(q..f)} by A4,A11,A13,A16,A20 ,A21,A22,TOPREAL1:def 6 .= {q} by A1,FINSEQ_5:38; hence thesis by A15,A18,XBOOLE_0:def 4; end; suppose that A23: i+1 = len(f-:q) and A24: j9 <> 0; 1 <= j9 by A24,NAT_1:14; then i+1+1 <= j9+q..f by A11,A23,XREAL_1:7; then i+1 < j9+q..f by NAT_1:13; then LSeg((f-:q),i) misses LSeg(f:-q,j) by A5,A16,A20,TOPREAL1:def 7; then LSeg((f-:q),i) /\ LSeg(f:-q,j) = {} by XBOOLE_0:def 7; hence thesis by A15,A18,XBOOLE_0:def 4; end; suppose A25: i+1 <> len(f-:q); A26: q..f <= j9+q..f by NAT_1:11; i+1 < q..f by A11,A14,A25,XXREAL_0:1; then i+1 < j9+q..f by A26,XXREAL_0:2; then LSeg((f-:q),i) misses LSeg(f:-q,j) by A5,A16,A20,TOPREAL1:def 7; then LSeg((f-:q),i) /\ LSeg(f:-q,j) = {} by XBOOLE_0:def 7; hence thesis by A15,A18,XBOOLE_0:def 4; end; end; 1 <= q..f by A1,FINSEQ_4:21; then 1 < q..f by A2,XXREAL_0:1; then 1+1 <= q..f by NAT_1:13; then A27: rng(f-:q) c= L~(f-:q) by A11,Th18; (f-:q)/.(q..f) = q by A1,FINSEQ_5:45; then q in rng(f-:q) by A11,A10,PARTFUN2:2; then q in L~(f-:q) /\ L~(f:-q) by A27,A9,A8,XBOOLE_0:def 4; hence thesis by ZFMISC_1:31; end; theorem Th43: p <> q & (p`1 = q`1 or p`2 = q`2) implies <*p,q*> is being_S-Seq proof assume that A1: p <> q and A2: p`1 = q`1 or p`2 = q`2; set f = <*p,q*>; thus f is one-to-one by A1,FINSEQ_3:94; thus len f >= 2 by FINSEQ_1:44; thus thesis by A2,Lm2,Lm6,Th38; end; definition mode S-Sequence_in_R2 is being_S-Seq FinSequence of TOP-REAL 2; end; registration let f be S-Sequence_in_R2; cluster Rev f -> being_S-Seq for FinSequence of TOP-REAL 2; coherence proof set g = Rev f; g is being_S-Seq proof thus g is one-to-one; len g = len f by FINSEQ_5:def 3; hence len g >= 2 by TOPREAL1:def 8; thus thesis by Th28,Th35,Th40; end; hence thesis; end; end; theorem for f being S-Sequence_in_R2 st i in dom f holds f/.i in L~f proof let f be S-Sequence_in_R2; len f >= 2 by TOPREAL1:def 8; hence thesis by GOBOARD1:1; end; theorem p <> q & (p`1 = q`1 or p`2 = q`2) implies LSeg(p,q) is being_S-P_arc proof assume that A1: p <> q and A2: p`1 = q`1 or p`2 = q`2; take f = <*p,q*>; thus f is being_S-Seq by A1,A2,Th43; thus thesis by Th21; end; Lm14: p in rng f implies L~(f-:p) c= L~f proof assume p in rng f; then L~f = L~(f-:p) \/ L~(f:-p) by Th24; hence thesis by XBOOLE_1:7; end; Lm15: p in rng f implies L~(f:-p) c= L~f proof assume p in rng f; then L~f = L~(f-:p) \/ L~(f:-p) by Th24; hence thesis by XBOOLE_1:7; end; theorem Th46: for f being S-Sequence_in_R2 st p in rng f & p..f <> 1 holds f-: p is being_S-Seq proof let f be S-Sequence_in_R2 such that A1: p in rng f and A2: p..f <> 1; thus f-:p is one-to-one; 1 <= p..f by A1,FINSEQ_4:21; then 1 < p..f by A2,XXREAL_0:1; then 1+1 <= p..f by NAT_1:13; hence len(f-:p) >= 2 by A1,FINSEQ_5:42; thus thesis; end; theorem for f being S-Sequence_in_R2 st p in rng f & p..f <> len f holds f:-p is being_S-Seq proof let f be S-Sequence_in_R2 such that A1: p in rng f and A2: p..f <> len f; thus f:-p is one-to-one by A1,FINSEQ_5:56; hereby p..f <= len f by A1,FINSEQ_4:21; then p..f < len f by A2,XXREAL_0:1; then 1 + p..f <= len f by NAT_1:13; then A3: len f - p..f >= 1 by XREAL_1:19; assume len(f:-p) < 2; then len f - p..f + 1 < 1 + 1 by A1,FINSEQ_5:50; hence contradiction by A3,XREAL_1:6; end; thus thesis by A1,Th27,Th34,Th39; end; theorem Th48: for f being S-Sequence_in_R2 st p in LSeg(f,i) & not p in rng f holds Ins(f,i,p) is being_S-Seq proof let f be S-Sequence_in_R2 such that A1: p in LSeg(f,i) and A2: not p in rng f; set g = Ins(f,i,p); thus g is one-to-one by A2,FINSEQ_5:76; len g = len f + 1 by FINSEQ_5:69; then A3: len g >= len f by NAT_1:11; len f >= 2 by TOPREAL1:def 8; hence len g >= 2 by A3,XXREAL_0:2; thus g is unfolded by A1,Th32; thus g is s.n.c. by A1,A2,Th37; thus thesis by A1,Th41; end; begin :: Special Polygons in TOP-REAL 2 registration cluster being_S-P_arc for Subset of TOP-REAL 2; existence proof set p = |[ 0,0 ]|, q = |[ 1,1 ]|, f = <* p,|[p`1,q`2]|,q *>; A1: p`2 = 0 by EUCLID:52; A2: q`1 = 1 by EUCLID:52; A3: q`2 = 1 by EUCLID:52; p`1 = 0 by EUCLID:52; then f is being_S-Seq by A1,A2,A3,TOPREAL3:34; then L~f is being_S-P_arc by TOPREAL1:def 9; hence thesis; end; end; theorem P is_S-P_arc_joining p1,p2 implies P is_S-P_arc_joining p2,p1 proof given f such that A1: f is being_S-Seq and A2: P = L~f and A3: p1=f/.1 and A4: p2 = f/.len f; take g = Rev f; thus g is being_S-Seq & P = L~g by A1,A2,Th22; len g = len f by FINSEQ_5:def 3; hence thesis by A1,A3,A4,FINSEQ_5:65; end; definition let p1,p2; let P be Subset of TOP-REAL 2; pred p1,p2 split P means :Def1: p1 <> p2 & ex f1,f2 being S-Sequence_in_R2 st p1 = f1/.1 & p1 = f2/.1 & p2 = f1/.len f1 & p2 = f2/.len f2 & L~f1 /\ L~f2 = {p1,p2} & P = L~f1 \/ L~f2; end; theorem Th50: p1,p2 split P implies p2,p1 split P proof assume A1: p1 <> p2; given f1,f2 being S-Sequence_in_R2 such that A2: p1 = f1/.1 and A3: p1 = f2/.1 and A4: p2 = f1/.len f1 and A5: p2 = f2/.len f2 and A6: L~f1 /\ L~f2 = {p1,p2} and A7: P = L~f1 \/ L~f2; thus p2 <> p1 by A1; reconsider g1 = Rev f1, g2 = Rev f2 as S-Sequence_in_R2; take g1, g2; A8: len g2 = len f2 by FINSEQ_5:def 3; len g1 = len f1 by FINSEQ_5:def 3; hence p2 = g1/.1 & p2 = g2/.1 & p1 = g1/.len g1 & p1 = g2/.len g2 by A2,A3,A4,A5,A8 ,FINSEQ_5:65; L~g1 = L~f1 by Th22; hence thesis by A6,A7,Th22; end; Lm16: for f1,f2 being S-Sequence_in_R2 st p1 = f1/.1 & p1 = f2/.1 & p2 = f1/. len f1 & p2 = f2/.len f2 & L~f1 /\ L~f2 = {p1,p2} & P = L~f1 \/ L~f2 & q <> p1 & q in rng f1 ex g1,g2 being S-Sequence_in_R2 st p1 = g1/.1 & p1 = g2/.1 & q = g1/.len g1 & q = g2/.len g2 & L~g1 /\ L~g2 = {p1,q} & P = L~g1 \/ L~g2 proof let f1,f2 be S-Sequence_in_R2 such that A1: p1 = f1/.1 and A2: p1 = f2/.1 and A3: p2 = f1/.len f1 and A4: p2 = f2/.len f2 and A5: L~f1 /\ L~f2 = {p1,p2} and A6: P = L~f1 \/ L~f2 and A7: q <> p1 and A8: q in rng f1; set f19 = Rev(f1:-q); A9: 1 <= q..f1 by A8,FINSEQ_4:21; A10: now assume A11: 1 = q..f1; then A12: 1 in dom f1 by A8,FINSEQ_4:20; f1.1 = q by A8,A11,FINSEQ_4:19; hence contradiction by A1,A7,A12,PARTFUN1:def 6; end; then reconsider g1 = f1-:q as S-Sequence_in_R2 by A8,Th46; A13: 1 in dom g1 by FINSEQ_5:6; 1 in dom f2 by FINSEQ_5:6; then 1 <= len f2 by FINSEQ_3:25; then reconsider l = len f2 - 1 as Element of NAT by INT_1:5; set f29 = f2|l; A14: l+1 = len f2; rng f19 = rng(f1:-q) by FINSEQ_5:57; then A15: rng f19 c= rng f1 by A8,FINSEQ_5:55; len f2 >= 2 by TOPREAL1:def 8; then A16: rng f2 c= L~f2 by Th18; len f1 >= 2 by TOPREAL1:def 8; then rng f1 c= L~f1 by Th18; then A17: rng f2 /\ rng f1 c= L~f1 /\ L~f2 by A16,XBOOLE_1:27; set g2 = f29^f19; A18: dom f29 = Seg len f29 by FINSEQ_1:def 3; len(f1:-q) >= 1 by NAT_1:14; then A19: len f19 >= 1 by FINSEQ_5:def 3; then A20: len f19 in dom f19 by FINSEQ_3:25; A21: l < len f2 by XREAL_1:44; then A22: len f29 = l by FINSEQ_1:59; len f2 >= 2 by TOPREAL1:def 8; then A23: len f2 - 1 >= 1+1-1 by XREAL_1:9; then A24: l in dom f29 by A22,FINSEQ_3:25; then A25: f29/.len f29 = f2/.l by A22,FINSEQ_4:70; A26: f19/.1 = (f1:-q)/.len(f1:-q) by FINSEQ_5:65 .= f2/.len f2 by A3,A4,A8,FINSEQ_5:54; then A27: LSeg(f29/.len f29,f19/.1) = LSeg(f2,l) by A23,A14,A25,TOPREAL1:def 3; A28: now let i such that 1<=i and A29: i+2<=len f29; i+1+1 <= len f29 by A29; then A30: i+1 < len f29 by NAT_1:13; then LSeg(f29,i) = LSeg(f2,i) by Th3; hence LSeg(f29,i) misses LSeg(f29/.len f29,f19/.1) by A22,A27,A30, TOPREAL1:def 7; end; A31: 1 in dom f1 by FINSEQ_5:6; A32: now A33: 1 + 1 <= len f1 by TOPREAL1:def 8; p1 in LSeg(f1/.1,f1/.(1+1)) by A1,RLTOPSP1:68; then A34: p1 in LSeg(f1,1) by A33,TOPREAL1:def 3; assume p1 in L~f19; then A35: p1 in L~(f1:-q) by Th22; then consider i such that A36: 1 <= i and i+1 <= len(f1:-q) and A37: p1 in LSeg(f1:-q,i) by Th13; consider j be Nat such that A38: i = j+1 by A36,NAT_1:6; A39: 1 < q..f1 by A10,A9,XXREAL_0:1; reconsider j as Element of NAT by ORDINAL1:def 12; A40: LSeg(f1:-q,i) = LSeg(f1,j+q..f1) by A8,A38,Th10; then p1 in LSeg(f1,1) /\ LSeg(f1,j+q..f1) by A37,A34,XBOOLE_0:def 4; then A41: LSeg(f1,1) meets LSeg(f1,j+q..f1) by XBOOLE_0:4; per cases; suppose A42: j = 0; A43: 1+1 <= q..f1 by A39,NAT_1:13; now per cases by A43,XXREAL_0:1; suppose A44: q..f1 = 2; A45: q..f1 <= len f1 by A8,FINSEQ_4:21; now per cases by A44,A45,XXREAL_0:1; suppose len f1 = 2; then len(f1:-q) = len f1 - len f1 + 1 by A8,A44,FINSEQ_5:50; hence contradiction by A35,TOPREAL1:22; end; suppose len f1 > 2; then 1+2 <= len f1 by NAT_1:13; then LSeg(f1,1) /\ LSeg(f1,1+1) = {f1/.(1+1)} by TOPREAL1:def 6; then p1 in {f1/.2} by A37,A34,A40,A42,A44,XBOOLE_0:def 4; then A46: p1 = f1/.2 by TARSKI:def 1; 2 in dom f1 by A8,A44,FINSEQ_4:20; hence contradiction by A1,A31,A46,PARTFUN2:10; end; end; hence contradiction; end; suppose q..f1 > 2; then 1+1 < j+q..f1 by A42; hence contradiction by A41,TOPREAL1:def 7; end; end; hence contradiction; end; suppose j <> 0; then 1+1 < j+q..f1 by A39,NAT_1:14,XREAL_1:8; hence contradiction by A41,TOPREAL1:def 7; end; end; A47: now let i such that A48: 2<=i and A49: i+1 <= len f19; reconsider m = len f19-(i+1) as Element of NAT by A49,INT_1:5; m+1+i = len(f1:-q) by FINSEQ_5:def 3; then A50: LSeg(f19,i) = LSeg(f1:-q,m+1) by Th2 .= LSeg(f1,m+q..f1) by A8,Th10; then A51: LSeg(f19,i) c= L~f1 by TOPREAL3:19; A52: now A53: len f1 >= 1+1 by TOPREAL1:def 8; then reconsider k = len f1 - 1 as Element of NAT by INT_1:5,XXREAL_0:2; A54: p2 in LSeg(f1/.k,f1/.len f1) by A3,RLTOPSP1:68; A55: k+1 = len f1; then 1 <= k by A53,XREAL_1:6; then A56: p2 in LSeg(f1,k) by A55,A54,TOPREAL1:def 3; A57: len f19 = len(f1:-q) by FINSEQ_5:def 3; A58: len f1 - i = len f1 - q..f1 + 1 - 1 + q..f1 - i .= len f19 - 1 + q..f1 - i by A8,A57,FINSEQ_5:50 .= m + q..f1; per cases; suppose A59: i = 1+1; A60: q..f1 <= m+q..f1 by NAT_1:11; 1 <= q..f1 by A8,FINSEQ_4:21; then A61: 1 <= m + q..f1 by A60,XXREAL_0:2; assume A62: p2 in LSeg(f19,i); A63: m+q..f1+(1+1) = len f1 by A58,A59; A64: 1 <= k by A53,XREAL_1:19; p2 in LSeg(f1/.k,f1/.(k+1)) by A3,RLTOPSP1:68; then A65: p2 in LSeg(f1,k) by A64,TOPREAL1:def 3; m + q..f1 + 1 = k by A58,A59; then LSeg(f1,m + q..f1) /\ LSeg(f1,k) = {f1/.k} by A61,A63, TOPREAL1:def 6; then p2 in {f1/.k} by A50,A65,A62,XBOOLE_0:def 4; then A66: f1/.len f1 = f1/.k by A3,TARSKI:def 1; k <= len f1 by A55,NAT_1:11; then A67: k in dom f1 by A64,FINSEQ_3:25; len f1 in dom f1 by FINSEQ_5:6; then len f1 - k = len f1 - len f1 by A67,A66,PARTFUN2:10 .= 0; hence contradiction; end; suppose i <> 2; then 2 < i by A48,XXREAL_0:1; then 2+1 <= i by NAT_1:13; then len f1 - i <= len f1 - (1+2) by XREAL_1:10; then len f1 - i <= len f1 - 1 - 2; then A68: len f1 - i + (1+1) <= k by XREAL_1:19; len f1 - i + (1+1) = m + q..f1 + 1 + 1 by A58; then m+q..f1 +1 < k by A68,NAT_1:13; then LSeg(f1,k) misses LSeg(f1,m+q..f1) by TOPREAL1:def 7; then LSeg(f1,k) /\ LSeg(f1,m+q..f1) = {} by XBOOLE_0:def 7; hence not p2 in LSeg(f19,i) by A50,A56,XBOOLE_0:def 4; end; end; LSeg(f19,i) c= L~f19 by TOPREAL3:19; then A69: not p1 in LSeg(f19,i) by A32; LSeg(f29/.len f29,f19/.1) c=L~f2 by A27,TOPREAL3:19; then A70: LSeg(f29/.len f29,f19/.1) /\ LSeg(f19,i) c= {p1,p2} by A5,A51,XBOOLE_1:27; now given x being set such that A71: x in LSeg(f29/.len f29,f19/.1) /\ LSeg(f19,i); x = p1 or x = p2 by A70,A71,TARSKI:def 2; hence contradiction by A69,A52,A71,XBOOLE_0:def 4; end; then LSeg(f19,i) /\ LSeg(f29/.len f29,f19/.1) = {} by XBOOLE_0:def 1; hence LSeg(f19,i) misses LSeg(f29/.len f29,f19/.1) by XBOOLE_0:def 7; end; A72: now assume len f19 <> 1; then 1 < len f19 by A19,XXREAL_0:1; then A73: 1+1 <= len f19 by NAT_1:13; now let x be set; hereby reconsider m = len f19-2 as Element of NAT by A73,INT_1:5; LSeg(f19,1) c= L~f19 by TOPREAL3:19; then not p1 in LSeg(f19,1) by A32; then A74: not p1 in LSeg(f29/.len f29,f19/.1) /\ LSeg(f19,1) by XBOOLE_0:def 4; m+1+1 = len(f1:-q) by FINSEQ_5:def 3; then LSeg(f19,1) = LSeg(f1:-q,m+1) by Th2 .= LSeg(f1,m+q..f1) by A8,Th10; then A75: LSeg(f19,1) c= L~f1 by TOPREAL3:19; LSeg(f29/.len f29,f19/.1) c=L~f2 by A27,TOPREAL3:19; then A76: LSeg(f29/.len f29,f19/.1) /\ LSeg(f19,1) c= {p1,p2} by A5,A75, XBOOLE_1:27; assume x in LSeg(f29/.len f29,f19/.1) /\ LSeg(f19,1); hence x = f19/.1 by A4,A26,A76,A74,TARSKI:def 2; end; assume A77: x = f19/.1; then x in LSeg(f19/.1,f19/.(1+1)) by RLTOPSP1:68; then A78: x in LSeg(f19,1) by A73,TOPREAL1:def 3; x in LSeg(f29/.len f29,f19/.1) by A77,RLTOPSP1:68; hence x in LSeg(f29/.len f29,f19/.1) /\ LSeg(f19,1) by A78,XBOOLE_0:def 4 ; end; hence LSeg(f29/.len f29,f19/.1) /\ LSeg(f19,1) = {f19/.1} by TARSKI:def 1; end; A79: len f29 >= 1 by A21,A23,FINSEQ_1:59; then A80: f29 is non empty; f1:-q is unfolded by A8,Th27; then A81: f19 is unfolded by Th28; A82: now per cases; suppose len f29 = 1 & len f19 = 1; then len g2 = 1+1 by FINSEQ_1:22; hence g2 is unfolded by Th26; end; suppose that A83: len f29 <> 1 and A84: len f19 = 1; consider k be Nat such that A85: k+1 = len f29 by A79,NAT_1:6; reconsider k as Element of NAT by ORDINAL1:def 12; A86: LSeg(f29,k) = LSeg(f2,k) by A85,Th3; len f29 > 1 by A22,A23,A83,XXREAL_0:1; then A87: 1 <= k by A85,NAT_1:13; A88: f19 = <*f19/.1*> by A84,FINSEQ_5:14; k+(1+1) <= len f2 by A22,A85; then LSeg(f29,k) /\ LSeg(f29/.len f29,f19/.1) = {f29/.len f29} by A22,A25 ,A27,A85,A87,A86,TOPREAL1:def 6; hence g2 is unfolded by A85,A88,Th30; end; suppose that A89: len f29 = 1 and A90: len f19 <> 1; f29 = <*f29/.len f29*> by A89,FINSEQ_5:14; hence g2 is unfolded by A81,A72,A90,Th29; end; suppose that A91: len f29 <> 1 and A92: len f19 <> 1; consider k be Nat such that A93: k+1 = len f29 by A79,NAT_1:6; reconsider k as Element of NAT by ORDINAL1:def 12; A94: k+(1+1) <= len f2 by A22,A93; A95: LSeg(f29,k) = LSeg(f2,k) by A93,Th3; len f29 > 1 by A22,A23,A91,XXREAL_0:1; then 1 <= k by A93,NAT_1:13; then LSeg(f29,k) /\ LSeg(f29/.len f29,f19/.1) = {f29/.len f29} by A22,A25 ,A27,A93,A94,A95,TOPREAL1:def 6; hence g2 is unfolded by A81,A72,A92,A93,Th31; end; end; len g1 >= 2 by TOPREAL1:def 8; then A96: rng g1 c= L~g1 by Th18; set Z = rng f29 /\ rng f19; A97: 1 in dom f29 by A22,A23,FINSEQ_3:25; A98: len f2 in dom f2 by FINSEQ_5:6; then A99: p2..f2 = len f2 by A4,FINSEQ_5:41; now assume A100: p2 in rng f29; then p2..f29 = p2..f2 by FINSEQ_5:40; hence contradiction by A22,A99,A100,FINSEQ_4:21,XREAL_1:44; end; then A101: not p2 in Z by XBOOLE_0:def 4; then A102: Z <> {p1,p2} by TARSKI:def 2; dom f2 = Seg len f2 by FINSEQ_1:def 3; then A103: len f29 in dom f2 by A22,A14,A24,A18,FINSEQ_2:8; now p2 in LSeg(f2/.len f29,p2) by RLTOPSP1:68; then A104: p2 in LSeg(f2,len f29) by A4,A22,A23,A14,TOPREAL1:def 3; assume p2 in L~f29; then consider i such that A105: 1 <= i and A106: i+1 <= len(f29) and A107: p2 in LSeg(f29,i) by Th13; LSeg(f29,i) = LSeg(f2,i) by A106,Th3; then A108: p2 in LSeg(f2,i) /\ LSeg(f2,len f29) by A107,A104,XBOOLE_0:def 4; then A109: LSeg(f2,i) meets LSeg(f2,len f29) by XBOOLE_0:4; A110: len f2 <> len f29 by A21,FINSEQ_1:59; per cases; suppose A111: i+1 = len(f29); then i + (1+1) = len f2 by A22; then LSeg(f2,i) /\ LSeg(f2,len f29) = {f2/.len f29} by A105,A111, TOPREAL1:def 6; then p2 = f2/.len f29 by A108,TARSKI:def 1; hence contradiction by A4,A98,A103,A110,PARTFUN2:10; end; suppose i+1 <> len(f29); then i+1 < len(f29) by A106,XXREAL_0:1; hence contradiction by A109,TOPREAL1:def 7; end; end; then A112: not p2 in L~f29 /\ L~f19 by XBOOLE_0:def 4; L~(f1:-q) c= L~f1 by A8,Lm15; then A113: L~f19 c= L~f1 by Th22; L~f29 c= L~f2 by Lm1; then L~f29 /\ L~f19 c= {p1,p2} by A5,A113,XBOOLE_1:27; then A114: L~f29 /\ L~f19 = {} or L~f29 /\ L~f19 = {p1} or L~f29 /\ L~f19 = { p2} or L~f29 /\ L~f19 = {p1,p2} by ZFMISC_1:36; f1:-q is special by A8,Th39; then A115: f19 is special by Th40; A116: 1 in dom(f1:-q) by FINSEQ_5:6; now set l = p1..(f1:-q); assume A117: p1 in rng(f1:-q); then A118: (f1:-q).l = p1 by FINSEQ_4:19; l <> 0 by A117,FINSEQ_4:21; then consider j be Nat such that A119: l = j+1 by NAT_1:6; reconsider j as Element of NAT by ORDINAL1:def 12; A120: l in dom(f1:-q) by A117,FINSEQ_4:20; then A121: j+q..f1 in dom f1 by A8,A119,FINSEQ_5:51; (f1:-q)/.l = f1/.(j+q..f1) by A8,A120,A119,FINSEQ_5:52; then j+q..f1 = 1 by A1,A31,A120,A118,A121,PARTFUN1:def 6,PARTFUN2:10; then A122: q..f1 <= 1 by NAT_1:11; 1 <= q..f1 by A8,FINSEQ_4:21; hence contradiction by A10,A122,XXREAL_0:1; end; then not p1 in rng f19 by FINSEQ_5:57; then not p1 in Z by XBOOLE_0:def 4; then A123: Z <> {p1} by TARSKI:def 1; rng f29 c= rng f2 by FINSEQ_5:19; then Z c= rng f2 /\ rng f1 by A15,XBOOLE_1:27; then A124: Z c= {p1,p2} by A5,A17,XBOOLE_1:1; reconsider f1q = f1:-q as one-to-one FinSequence of TOP-REAL 2 by A8, FINSEQ_5:56; A125: Rev f1q is one-to-one; f1:-q is s.n.c. by A8,Th34; then A126: f19 is s.n.c. by Th35; (f29/.len f29)`1 = (f19/.1)`1 or (f29/.len f29)`2 = (f19/.1)`2 by A23,A14,A25 ,A26,TOPREAL1:def 5; then A127: g2 is special by A115,Lm13; len f29 + len f19 >= 1+1 by A22,A19,A23,XREAL_1:7; then A128: len g2 >= 2 by FINSEQ_1:22; Z <> {p2} by A101,TARSKI:def 1; then Z = {} by A123,A102,A124,ZFMISC_1:36; then rng f29 misses rng f19 by XBOOLE_0:def 7; then A129: g2 is one-to-one by A125,FINSEQ_3:91; not p1 in L~f29 /\ L~f19 by A32,XBOOLE_0:def 4; then L~f29 misses L~f19 by A114,A112,TARSKI:def 1,def 2,XBOOLE_0:def 7; then f29^f19 is s.n.c. by A126,A28,A47,Th36; then reconsider g2 as S-Sequence_in_R2 by A129,A128,A82,A127,TOPREAL1:def 8; A130: L~f2 \/ L~f19 = L~(f29^<*p2*>) \/ L~f19 by A4,A14,FINSEQ_5:21 .= L~f29 \/ LSeg(f29/.len f29,f19/.1) \/ L~f19 by A4,A97,A26,Th19, RELAT_1:38 .= L~g2 by A20,A80,Th23,RELAT_1:38; take g1,g2; thus A131: p1 = g1/.1 by A1,A8,FINSEQ_5:44; A132: 1 in dom g2 by FINSEQ_5:6; hence A133: g2/.1 = g2.1 by PARTFUN1:def 6 .= f29.1 by A97,FINSEQ_1:def 7 .= f29/.1 by A97,PARTFUN1:def 6 .= p1 by A2,A97,FINSEQ_4:70; thus A134: q = g1/.(q..f1) by A8,FINSEQ_5:45 .= g1/.len g1 by A8,FINSEQ_5:42; A135: len g2 in dom g2 by FINSEQ_5:6; hence A136: g2/.len g2 = g2.(len g2) by PARTFUN1:def 6 .= g2.(len f29 + len f19) by FINSEQ_1:22 .= f19.(len f19) by A20,FINSEQ_1:def 7 .= f19.(len (f1:-q)) by FINSEQ_5:def 3 .= (f1:-q).1 by FINSEQ_5:62 .= (f1:-q)/.1 by A116,PARTFUN1:def 6 .= q by FINSEQ_5:53; len g2 >= 2 by TOPREAL1:def 8; then A137: rng g2 c= L~g2 by Th18; A138: len g1 in dom g1 by FINSEQ_5:6; thus {p1,q} = L~g1 /\ L~g2 proof hereby let x be set; assume A139: x in {p1,q}; per cases by A139,TARSKI:def 2; suppose A140: x = p1; A141: p1 in rng g2 by A132,A133,PARTFUN2:2; p1 in rng g1 by A131,A13,PARTFUN2:2; hence x in L~g1 /\ L~g2 by A96,A137,A140,A141,XBOOLE_0:def 4; end; suppose A142: x = q; A143: q in rng g2 by A135,A136,PARTFUN2:2; q in rng g1 by A134,A138,PARTFUN2:2; hence x in L~g1 /\ L~g2 by A96,A137,A142,A143,XBOOLE_0:def 4; end; end; A144: len f1 in dom f1 by FINSEQ_5:6; A145: L~g1 /\ L~g2 = L~g1 /\ L~f2 \/ L~g1 /\ L~f19 by A130,XBOOLE_1:23; A146: q..f1 in dom f1 by A8,FINSEQ_4:20; A147: q = f1.(q..f1) by A8,FINSEQ_4:19 .= f1/.(q..f1) by A146,PARTFUN1:def 6; A148: len g1 = q..f1 by A8,FINSEQ_5:42; per cases; suppose A149: q <> p2; now A150: q..f1 <= len f1 by A8,FINSEQ_4:21; then reconsider j = len f1 - 1 as Element of NAT by A9,INT_1:5 ,XXREAL_0:2; A151: j+1 = len f1; A152: p2 in LSeg(f1/.j,f1/.(j+1)) by A3,RLTOPSP1:68; 1 < q..f1 by A10,A9,XXREAL_0:1; then 1 < len f1 by A150,XXREAL_0:2; then 1 <= j by A151,NAT_1:13; then A153: p2 in LSeg(f1,j) by A152,TOPREAL1:def 3; assume p2 in L~g1; then consider i such that A154: 1 <= i and A155: i+1 <= len g1 and A156: p2 in LSeg(g1,i) by Th13; A157: p2 in LSeg(f1,i) by A155,A156,Th9; q..f1 < len f1 by A3,A147,A149,A150,XXREAL_0:1; then A158: q..f1 <= j by A151,NAT_1:13; then A159: i+1 <= j by A148,A155,XXREAL_0:2; per cases; suppose A160: i+1 = j; then i+(1+1) = j+1; then LSeg(f1,i) /\ LSeg(f1,i+1) = {f1/.(i+1)} by A154,TOPREAL1:def 6; then p2 in {f1/.(i+1)} by A157,A153,A160,XBOOLE_0:def 4; then p2 = f1/.(i+1) by TARSKI:def 1; hence contradiction by A148,A147,A149,A155,A158,A160,XXREAL_0:1; end; suppose i+1 <> j; then i+1 < j by A159,XXREAL_0:1; then LSeg(f1,i) misses LSeg(f1,j) by TOPREAL1:def 7; then LSeg(f1,i) /\ LSeg(f1,j) = {} by XBOOLE_0:def 7; hence contradiction by A157,A153,XBOOLE_0:def 4; end; end; then A161: not p2 in L~g1 /\ L~f2 by XBOOLE_0:def 4; L~g1 /\ L~f2 c= {p1,p2} by A5,A8,Lm14,XBOOLE_1:26; then L~g1 /\ L~f2 = {} or L~g1 /\ L~f2 = {p1} or L~g1 /\ L~f2 = {p2} or L~g1 /\ L~f2 = {p1,p2} by ZFMISC_1:36; then A162: L~g1 /\ L~f2 c= {p1} by A161,TARSKI:def 1,def 2,ZFMISC_1:33; L~g1 /\ L~f19 = L~g1 /\ L~(f1:-q) by Th22 .= {q} by A3,A8,A10,A147,A149,Th42; then L~g1 /\ L~g2 c= {p1} \/ {q} by A145,A162,XBOOLE_1:9; hence thesis by ENUMSET1:1; end; suppose A163: q = p2; p2..f1 = len f1 by A3,A144,FINSEQ_5:41; then A164: len(f1:-q) = len f1 - len f1 + 1 by A8,A163,FINSEQ_5:50 .= 0+1; L~g1 /\ L~f19 = L~g1 /\ L~(f1:-q) by Th22 .= L~g1 /\ {} by A164,TOPREAL1:22 .= {}; hence thesis by A5,A8,A145,A163,Lm14,XBOOLE_1:26; end; end; thus P = L~(f1-:q) \/ L~(f1:-q) \/ L~f2 by A6,A8,Th24 .= L~g1 \/ (L~f2 \/ L~(f1:-q)) by XBOOLE_1:4 .= L~g1 \/ L~g2 by A130,Th22; end; theorem Th51: p1,p2 split P & q in P & q <> p1 implies p1,q split P proof assume p1 <> p2; given f1,f2 being S-Sequence_in_R2 such that A1: p1 = f1/.1 and A2: p1 = f2/.1 and A3: p2 = f1/.len f1 and A4: p2 = f2/.len f2 and A5: L~f1 /\ L~f2 = {p1,p2} and A6: P = L~f1 \/ L~f2; assume A7: q in P; assume A8: q <> p1; hence p1 <> q; per cases by A6,A7,XBOOLE_0:def 3; suppose A9: q in L~f1; now per cases; suppose q in rng f1; hence thesis by A1,A2,A3,A4,A5,A6,A8,Lm16; end; suppose A10: not q in rng f1; consider i such that A11: 1 <= i and A12: i+1 <= len f1 and A13: q in LSeg(f1,i) by A9,Th13; reconsider f19 = Ins(f1,i,q) as S-Sequence_in_R2 by A10,A13,Th48; A14: L~f19 = L~f1 by A13,Th25; len f19 = len f1 + 1 by FINSEQ_5:69; then A15: p2 = f19/.len f19 by A3,A12,FINSEQ_5:74; A16: q in rng f19 by FINSEQ_5:71; p1 = f19/.1 by A1,A11,FINSEQ_5:75; hence thesis by A2,A4,A5,A6,A8,A16,A15,A14,Lm16; end; end; hence thesis; end; suppose A17: q in L~f2; now per cases; suppose q in rng f2; hence thesis by A1,A2,A3,A4,A5,A6,A8,Lm16; end; suppose A18: not q in rng f2; consider i such that A19: 1 <= i and A20: i+1 <= len f2 and A21: q in LSeg(f2,i) by A17,Th13; reconsider f29 = Ins(f2,i,q) as S-Sequence_in_R2 by A18,A21,Th48; A22: L~f29 = L~f2 by A21,Th25; len f29 = len f2 + 1 by FINSEQ_5:69; then A23: p2 = f29/.len f29 by A4,A20,FINSEQ_5:74; A24: q in rng f29 by FINSEQ_5:71; p1 = f29/.1 by A2,A19,FINSEQ_5:75; hence thesis by A1,A3,A5,A6,A8,A24,A23,A22,Lm16; end; end; hence thesis; end; end; theorem Th52: p1,p2 split P & q in P & q <> p2 implies q,p2 split P proof assume that A1: p1,p2 split P and A2: q in P and A3: q <> p2; p2,p1 split P by A1,Th50; then p2,q split P by A2,A3,Th51; hence thesis by Th50; end; theorem Th53: p1,p2 split P & q1 in P & q2 in P & q1 <> q2 implies q1,q2 split P proof assume that A1: p1,p2 split P and A2: q1 in P and A3: q2 in P and A4: q1 <> q2; A5: p2,p1 split P by A1,Th50; per cases; suppose p1 = q1; hence thesis by A1,A3,A4,Th51; end; suppose p1 = q2; hence thesis by A2,A4,A5,Th52; end; suppose p1 <> q1; then p1,q1 split P by A1,A2,Th51; then q2,q1 split P by A3,A4,Th52; hence thesis by Th50; end; suppose p2 <> q1; then q1,p2 split P by A1,A2,Th52; hence thesis by A3,A4,Th51; end; end; notation let P be Subset of TOP-REAL 2; synonym P is special_polygonal for P is being_special_polygon; end; definition let P be Subset of TOP-REAL 2; redefine attr P is special_polygonal means :Def2: ex p1,p2 st p1,p2 split P; compatibility proof thus P is being_special_polygon implies ex p1,p2 st p1,p2 split P proof given p1,p2 being Point of TOP-REAL 2, P1,P2 being Subset of TOP-REAL 2 such that A1: p1 <> p2 and p1 in P and p2 in P and A2: P1 is_S-P_arc_joining p1,p2 and A3: P2 is_S-P_arc_joining p1,p2 and A4: P1 /\ P2 = {p1,p2} and A5: P = P1 \/ P2; take p1,p2; thus p1 <> p2 by A1; consider f1 such that A6: f1 is being_S-Seq and A7: P1 = L~f1 and A8: p1=f1/.1 and A9: p2=f1/.len f1 by A2,TOPREAL4:def 1; consider f2 such that A10: f2 is being_S-Seq and A11: P2 = L~f2 and A12: p1=f2/.1 and A13: p2=f2/.len f2 by A3,TOPREAL4:def 1; reconsider f1,f2 as S-Sequence_in_R2 by A6,A10; take f1,f2; thus thesis by A4,A5,A7,A8,A9,A11,A12,A13; end; given p1,p2 such that A14: p1,p2 split P; A15: p2 in {p1,p2} by TARSKI:def 2; A16: p1 in {p1,p2} by TARSKI:def 2; consider f1,f2 being S-Sequence_in_R2 such that A17: p1 = f1/.1 and A18: p1 = f2/.1 and A19: p2 = f1/.len f1 and A20: p2 = f2/.len f2 and A21: L~f1 /\ L~f2 = {p1,p2} and A22: P = L~f1 \/ L~f2 by A14,Def1; take p1,p2, P1=L~f1, P2=L~f2; thus p1 <> p2 by A14,Def1; {p1,p2} c= P by A21,A22,XBOOLE_1:29; hence p1 in P & p2 in P by A16,A15; thus ex f st f is being_S-Seq & P1 = L~f & p1=f/.1 & p2=f/.len f by A17,A19 ; thus ex f st f is being_S-Seq & P2 = L~f & p1=f/.1 & p2=f/.len f by A18,A20 ; thus thesis by A21,A22; end; end; Lm17: for P being Subset of TOP-REAL 2 holds P is being_special_polygon implies ex p1,p2 st p1 <> p2 & p1 in P & p2 in P proof let P be Subset of TOP-REAL 2; assume P is being_special_polygon; then ex p1,p2 being Point of TOP-REAL 2, P1,P2 being Subset of TOP-REAL 2 st p1 <> p2 & p1 in P & p2 in P & P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 by TOPREAL4:def 2; hence thesis; end; definition let r1,r2,r19,r29; func [.r1,r2,r19,r29.] -> Subset of TOP-REAL 2 equals ( LSeg(|[r1,r19]|,|[r1 ,r29]|) \/ LSeg(|[r1,r29]|,|[r2,r29]|) ) \/ ( LSeg(|[r2,r29]|,|[r2,r19]|) \/ LSeg(|[r2,r19]|,|[r1,r19]|) ); coherence; end; registration let n be Element of NAT; let p1, p2 be Point of TOP-REAL n; cluster LSeg(p1,p2) -> compact; coherence; end; registration let r1,r2,r19,r29; cluster [.r1,r2,r19,r29.] -> non empty compact; coherence proof thus [.r1,r2,r19,r29.] is non empty; A1: LSeg(|[r2,r29]|,|[r2,r19]|) \/ LSeg(|[r2,r19]|,|[r1,r19]|) is compact by COMPTS_1:10; LSeg(|[r1,r19]|,|[r1,r29]|) \/ LSeg(|[r1,r29]|,|[r2,r29]|) is compact by COMPTS_1:10; hence thesis by A1,COMPTS_1:10; end; end; theorem r1<=r2 & r19<=r29 implies [.r1,r2,r19,r29.] = { p: p`1 = r1 & p`2 <= r29 & p`2 >= r19 or p`1 <= r2 & p`1 >= r1 & p`2 = r29 or p`1 <= r2 & p`1 >= r1 & p`2 = r19 or p`1 = r2 & p`2 <= r29 & p`2 >= r19} proof assume that A1: r1<=r2 and A2: r19<=r29; set p1 = |[r1,r19]|, p2 = |[r1,r29]| , p3 = |[r2,r29]|, p4 = |[r2,r19]|; set P4 = { p: p`2 = r19& r1 <= p`1 & p`1 <= r2 }; set P3 = { p: p`1 = r2 & r19<= p`2 & p`2 <= r29}; set P2 = { p: p`2 = r29& r1 <= p`1 & p`1 <= r2 }; set P1 = { p: p`1 = r1 & r19<= p`2 & p`2 <= r29}; set P = { p: p`1 = r1 & p`2 <= r29 & p`2 >= r19 or p`1 <= r2 & p`1 >= r1 & p `2 = r29 or p`1 <= r2 & p`1 >= r1 & p`2 = r19 or p`1 = r2 & p`2 <= r29 & p`2 >= r19}; A3: P = P1 \/ P2 \/ (P3 \/ P4) proof hereby let x be set; assume x in P; then ex p st x = p &( p`1 = r1 & p`2 <= r29 & p`2 >= r19 or p `1 <= r2 & p`1 >= r1 & p`2 = r29 or p`1 <= r2 & p`1 >= r1 & p`2 = r19 or p`1 = r2 & p`2 <= r29 & p`2 >= r19); then x in P1 or x in P2 or x in P3 or x in P4; then x in P1 \/ P2 or x in P3 \/ P4 by XBOOLE_0:def 3; hence x in P1 \/ P2 \/ (P3 \/ P4) by XBOOLE_0:def 3; end; let x be set; assume x in P1 \/ P2 \/ (P3 \/ P4); then A4: x in P1 \/ P2 or x in P3 \/ P4 by XBOOLE_0:def 3; per cases by A4,XBOOLE_0:def 3; suppose x in P1; then ex p st x = p & p`1 = r1 & r19<= p`2 & p`2 <= r29; hence thesis; end; suppose x in P2; then ex p st x = p & p`2 = r29& r1 <= p`1 & p`1 <= r2; hence thesis; end; suppose x in P3; then ex p st x = p & p`1 = r2 & r19<= p`2 & p`2 <= r29; hence thesis; end; suppose x in P4; then ex p st x = p & p`2 = r19& r1 <= p`1 & p`1 <= r2; hence thesis; end; end; thus [.r1,r2,r19,r29.] = P1 \/ LSeg(p2,p3) \/ (LSeg(p3,p4) \/ LSeg(p4,p1)) by A2,TOPREAL3:9 .= P1 \/ P2 \/ (LSeg(p3,p4) \/ LSeg(p4,p1)) by A1,TOPREAL3:10 .= P1 \/ P2 \/ (P3 \/ LSeg(p4,p1)) by A2,TOPREAL3:9 .= P by A1,A3,TOPREAL3:10; end; theorem Th55: r1<>r2 & r19<>r29 implies [.r1,r2,r19,r29.] is special_polygonal proof assume that A1: r1<>r2 and A2: r19<>r29; set p1 = |[r1,r19]|, p2 = |[r1,r29]| , p3 = |[r2,r29]|, p4 = |[r2,r19]|; A3: p3`1 = r2 by EUCLID:52; take p1,p3; thus p1 <> p3 by A1,FINSEQ_1:77; A4: p4`1 = r2 by EUCLID:52; A5: p3`2 = r29 by EUCLID:52; A6: p4`2 = r19 by EUCLID:52; set f1 = <* p1,p2,p3 *>, f2 = <* p1,p4,p3 *>; A7: p1`1 = r1 by EUCLID:52; A8: len f2 = 3 by FINSEQ_1:45; A9: len f1 = 3 by FINSEQ_1:45; A10: p1`2 = r19 by EUCLID:52; then reconsider f1,f2 as S-Sequence_in_R2 by A1,A2,A7,A3,A5,TOPREAL3:34,35; take f1,f2; thus p1 = f1/.1 & p1 = f2/.1 & p3 = f1/.len f1 & p3 = f2/.len f2 by A9,A8, FINSEQ_4:18; A11: L~f2 = LSeg(p3,p4) \/ LSeg(p4,p1) by TOPREAL3:16; L~f1 = LSeg(p1,p2) \/ LSeg(p2,p3) by TOPREAL3:16; hence L~f1 /\ L~f2 = ((LSeg(p1,p2) \/ LSeg(p2,p3)) /\ LSeg(p3,p4)) \/ ((LSeg( p1,p2) \/ LSeg(p2,p3)) /\ LSeg(p4,p1)) by A11,XBOOLE_1:23 .= ((LSeg(p2,p1) \/ LSeg(p3,p2)) /\ LSeg(p4,p3)) \/ {p1} by A2,A7,A10,A5,A6 ,TOPREAL3:27 .= {p3} \/ {p1} by A1,A7,A3,A5,A4,TOPREAL3:28 .= {p1,p3} by ENUMSET1:1; thus thesis by A11,TOPREAL3:16; end; theorem Th56: R^2-unit_square = [.0,1,0,1.]; registration cluster special_polygonal for Subset of TOP-REAL 2; existence proof take [.0,1,0,1.]; thus thesis by Th55; end; end; registration cluster R^2-unit_square -> special_polygonal; coherence by Th55,Th56; end; registration cluster special_polygonal for Subset of TOP-REAL 2; existence by Th56; cluster special_polygonal -> non empty for Subset of TOP-REAL 2; coherence proof let P be Subset of TOP-REAL 2; assume P is special_polygonal; then ex p1,p2 st p1 <> p2 & p1 in P & p2 in P by Lm17; hence thesis; end; cluster special_polygonal -> non trivial for Subset of TOP-REAL 2; coherence proof let P be Subset of TOP-REAL 2; assume P is special_polygonal; then ex p1,p2 st p1 <> p2 & p1 in P & p2 in P by Lm17; hence thesis by ZFMISC_1:def 10; end; end; definition mode Special_polygon_in_R2 is special_polygonal Subset of TOP-REAL 2; end; theorem Th57: P is being_S-P_arc implies P is compact proof A1: I[01] is compact by HEINE:4,TOPMETR:20; assume P is being_S-P_arc; then reconsider P as being_S-P_arc Subset of TOP-REAL 2; consider f being Function of I[01], (TOP-REAL 2)|P such that A2: f is being_homeomorphism by TOPREAL1:29; A3: rng f = [#]((TOP-REAL 2)|P) by A2,TOPS_2:def 5; f is continuous by A2,TOPS_2:def 5; then (TOP-REAL 2)|P is compact by A1,A3,COMPTS_1:14; hence thesis by COMPTS_1:3; end; registration cluster -> compact for Special_polygon_in_R2; coherence proof let G be Special_polygon_in_R2; consider p,q being Point of TOP-REAL 2, P1,P2 being Subset of TOP-REAL 2 such that p<>q and p in G and q in G and A1: P1 is_S-P_arc_joining p,q and A2: P2 is_S-P_arc_joining p,q and P1 /\ P2 = {p,q} and A3: G = P1 \/ P2 by TOPREAL4:def 2; reconsider P1,P2 as Subset of TOP-REAL 2; A4: P2 is compact by A2,Th57,TOPREAL4:1; P1 is compact by A1,Th57,TOPREAL4:1; hence thesis by A3,A4,COMPTS_1:10; end; end; theorem Th58: P is special_polygonal implies for p1,p2 st p1 <> p2 & p1 in P & p2 in P holds p1,p2 split P proof assume P is special_polygonal; then ex q1,q2 st q1,q2 split P by Def2; hence thesis by Th53; end; theorem P is special_polygonal implies for p1,p2 st p1 <> p2 & p1 in P & p2 in P ex P1,P2 being Subset of TOP-REAL 2 st P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 proof assume A1: P is special_polygonal; let p1,p2; assume that A2: p1 <> p2 and A3: p1 in P and A4: p2 in P; p1,p2 split P by A1,A2,A3,A4,Th58; then consider f1,f2 being S-Sequence_in_R2 such that A5: p1 = f1/.1 and A6: p1 = f2/.1 and A7: p2 = f1/.len f1 and A8: p2 = f2/.len f2 and A9: L~f1 /\ L~f2 = {p1,p2} and A10: P = L~f1 \/ L~f2 by Def1; take P1 = L~f1, P2 = L~f2; thus P1 is_S-P_arc_joining p1,p2 by A5,A7,TOPREAL4:def 1; thus P2 is_S-P_arc_joining p1,p2 by A6,A8,TOPREAL4:def 1; thus thesis by A9,A10; end;