:: SPPOL_2 semantic presentation begin theorem :: SPPOL_2:1 for r1, r2, r19, r29 being real number st |[r1,r2]| = |[r19,r29]| holds ( r1 = r19 & r2 = r29 ) by FINSEQ_1:77; theorem Th2: :: SPPOL_2:2 for f being FinSequence of (TOP-REAL 2) for i, j being Nat st i + j = len f holds LSeg (f,i) = LSeg ((Rev f),j) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for i, j being Nat st i + j = len f holds LSeg (f,i) = LSeg ((Rev f),j) let i, j be Nat; ::_thesis: ( i + j = len f implies LSeg (f,i) = LSeg ((Rev f),j) ) assume A1: i + j = len f ; ::_thesis: LSeg (f,i) = LSeg ((Rev f),j) percases ( ( 1 <= i & i + 1 <= len f ) or not 1 <= i or not i + 1 <= len f ) ; supposethat A2: 1 <= i and A3: i + 1 <= len f ; ::_thesis: LSeg (f,i) = LSeg ((Rev f),j) 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 ; ::_thesis: verum end; supposeA10: not 1 <= i ; ::_thesis: LSeg (f,i) = LSeg ((Rev f),j) 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 LSeg (f,i) = LSeg ((Rev f),j) by A11, TOPREAL1:def_3; ::_thesis: verum end; supposeA12: not i + 1 <= len f ; ::_thesis: LSeg (f,i) = LSeg ((Rev f),j) then A13: LSeg (f,i) = {} by TOPREAL1:def_3; j < 1 by A1, A12, XREAL_1:6; hence LSeg (f,i) = LSeg ((Rev f),j) by A13, TOPREAL1:def_3; ::_thesis: verum end; end; end; theorem Th3: :: SPPOL_2:3 for f being FinSequence of (TOP-REAL 2) for i, n being Nat st i + 1 <= len (f | n) holds LSeg ((f | n),i) = LSeg (f,i) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for i, n being Nat st i + 1 <= len (f | n) holds LSeg ((f | n),i) = LSeg (f,i) let i, n be Nat; ::_thesis: ( i + 1 <= len (f | n) implies LSeg ((f | n),i) = LSeg (f,i) ) assume A1: i + 1 <= len (f | n) ; ::_thesis: LSeg ((f | n),i) = LSeg (f,i) percases ( i <> 0 or i = 0 ) ; suppose i <> 0 ; ::_thesis: LSeg ((f | n),i) = LSeg (f,i) 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 ; ::_thesis: verum end; supposeA6: i = 0 ; ::_thesis: LSeg ((f | n),i) = LSeg (f,i) hence LSeg ((f | n),i) = {} by TOPREAL1:def_3 .= LSeg (f,i) by A6, TOPREAL1:def_3 ; ::_thesis: verum end; end; end; theorem Th4: :: SPPOL_2:4 for f being FinSequence of (TOP-REAL 2) for i, n being Nat st n <= len f & 1 <= i holds LSeg ((f /^ n),i) = LSeg (f,(n + i)) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for i, n being Nat st n <= len f & 1 <= i holds LSeg ((f /^ n),i) = LSeg (f,(n + i)) let i, n be Nat; ::_thesis: ( n <= len f & 1 <= i implies LSeg ((f /^ n),i) = LSeg (f,(n + i)) ) assume that A1: n <= len f and A2: 1 <= i ; ::_thesis: LSeg ((f /^ n),i) = LSeg (f,(n + i)) percases ( i + 1 <= (len f) - n or i + 1 > (len f) - n ) ; supposeA3: i + 1 <= (len f) - n ; ::_thesis: LSeg ((f /^ n),i) = LSeg (f,(n + i)) 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 ; ::_thesis: verum end; supposeA10: i + 1 > (len f) - n ; ::_thesis: LSeg ((f /^ n),i) = LSeg (f,(n + i)) 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 ; ::_thesis: verum end; end; end; theorem Th5: :: SPPOL_2:5 for f being FinSequence of (TOP-REAL 2) for i, n being Nat st 1 <= i & i + 1 <= (len f) - n holds LSeg ((f /^ n),i) = LSeg (f,(n + i)) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for i, n being Nat st 1 <= i & i + 1 <= (len f) - n holds LSeg ((f /^ n),i) = LSeg (f,(n + i)) let i, n be Nat; ::_thesis: ( 1 <= i & i + 1 <= (len f) - n implies LSeg ((f /^ n),i) = LSeg (f,(n + i)) ) assume A1: 1 <= i ; ::_thesis: ( not i + 1 <= (len f) - n or LSeg ((f /^ n),i) = LSeg (f,(n + i)) ) A2: n <= (i + 1) + n by NAT_1:11; assume i + 1 <= (len f) - n ; ::_thesis: LSeg ((f /^ n),i) = LSeg (f,(n + i)) then (i + 1) + n <= len f by XREAL_1:19; then n <= len f by A2, XXREAL_0:2; hence LSeg ((f /^ n),i) = LSeg (f,(n + i)) by A1, Th4; ::_thesis: verum end; theorem Th6: :: SPPOL_2:6 for f, g being FinSequence of (TOP-REAL 2) for i being Nat st i + 1 <= len f holds LSeg ((f ^ g),i) = LSeg (f,i) proof let f, g be FinSequence of (TOP-REAL 2); ::_thesis: for i being Nat st i + 1 <= len f holds LSeg ((f ^ g),i) = LSeg (f,i) let i be Nat; ::_thesis: ( i + 1 <= len f implies LSeg ((f ^ g),i) = LSeg (f,i) ) assume A1: i + 1 <= len f ; ::_thesis: LSeg ((f ^ g),i) = LSeg (f,i) percases ( i <> 0 or i = 0 ) ; suppose i <> 0 ; ::_thesis: LSeg ((f ^ g),i) = LSeg (f,i) 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 ; ::_thesis: verum end; supposeA6: i = 0 ; ::_thesis: LSeg ((f ^ g),i) = LSeg (f,i) hence LSeg ((f ^ g),i) = {} by TOPREAL1:def_3 .= LSeg (f,i) by A6, TOPREAL1:def_3 ; ::_thesis: verum end; end; end; theorem Th7: :: SPPOL_2:7 for f, g being FinSequence of (TOP-REAL 2) for i being Nat st 1 <= i holds LSeg ((f ^ g),((len f) + i)) = LSeg (g,i) proof let f, g be FinSequence of (TOP-REAL 2); ::_thesis: for i being Nat st 1 <= i holds LSeg ((f ^ g),((len f) + i)) = LSeg (g,i) let i be Nat; ::_thesis: ( 1 <= i implies LSeg ((f ^ g),((len f) + i)) = LSeg (g,i) ) assume A1: 1 <= i ; ::_thesis: LSeg ((f ^ g),((len f) + i)) = LSeg (g,i) percases ( i + 1 <= len g or i + 1 > len g ) ; supposeA2: i + 1 <= len g ; ::_thesis: LSeg ((f ^ g),((len f) + i)) = LSeg (g,i) (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 ; ::_thesis: verum end; supposeA7: i + 1 > len g ; ::_thesis: LSeg ((f ^ g),((len f) + i)) = LSeg (g,i) 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 ; ::_thesis: verum end; end; end; theorem Th8: :: SPPOL_2:8 for f, g being FinSequence of (TOP-REAL 2) st not f is empty & not g is empty holds LSeg ((f ^ g),(len f)) = LSeg ((f /. (len f)),(g /. 1)) proof let f, g be FinSequence of (TOP-REAL 2); ::_thesis: ( not f is empty & not g is empty implies LSeg ((f ^ g),(len f)) = LSeg ((f /. (len f)),(g /. 1)) ) assume that A1: not f is empty and A2: not g is empty ; ::_thesis: LSeg ((f ^ g),(len f)) = LSeg ((f /. (len f)),(g /. 1)) 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 ; ::_thesis: verum end; theorem Th9: :: SPPOL_2:9 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) for i being Nat st i + 1 <= len (f -: p) holds LSeg ((f -: p),i) = LSeg (f,i) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) for i being Nat st i + 1 <= len (f -: p) holds LSeg ((f -: p),i) = LSeg (f,i) let p be Point of (TOP-REAL 2); ::_thesis: for i being Nat st i + 1 <= len (f -: p) holds LSeg ((f -: p),i) = LSeg (f,i) let i be Nat; ::_thesis: ( i + 1 <= len (f -: p) implies LSeg ((f -: p),i) = LSeg (f,i) ) f -: p = f | (p .. f) by FINSEQ_5:def_1; hence ( i + 1 <= len (f -: p) implies LSeg ((f -: p),i) = LSeg (f,i) ) by Th3; ::_thesis: verum end; theorem Th10: :: SPPOL_2:10 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) for i being Nat st p in rng f holds LSeg ((f :- p),(i + 1)) = LSeg (f,(i + (p .. f))) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) for i being Nat st p in rng f holds LSeg ((f :- p),(i + 1)) = LSeg (f,(i + (p .. f))) let p be Point of (TOP-REAL 2); ::_thesis: for i being Nat st p in rng f holds LSeg ((f :- p),(i + 1)) = LSeg (f,(i + (p .. f))) let i be Nat; ::_thesis: ( p in rng f implies LSeg ((f :- p),(i + 1)) = LSeg (f,(i + (p .. f))) ) A1: 1 <= i + 1 by NAT_1:11; assume A2: p in rng f ; ::_thesis: LSeg ((f :- p),(i + 1)) = LSeg (f,(i + (p .. f))) then A3: len (f :- p) = ((len f) - (p .. f)) + 1 by FINSEQ_5:50; A4: i + (1 + 1) = (i + 1) + 1 ; percases ( i + 2 <= len (f :- p) or i + 2 > len (f :- p) ) ; supposeA5: i + 2 <= len (f :- p) ; ::_thesis: LSeg ((f :- p),(i + 1)) = LSeg (f,(i + (p .. f))) 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 ; ::_thesis: verum end; supposeA10: i + 2 > len (f :- p) ; ::_thesis: LSeg ((f :- p),(i + 1)) = LSeg (f,(i + (p .. f))) 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 ; ::_thesis: verum end; end; end; theorem Th11: :: SPPOL_2:11 L~ (<*> the carrier of (TOP-REAL 2)) = {} by TOPREAL1:22; theorem Th12: :: SPPOL_2:12 for p being Point of (TOP-REAL 2) holds L~ <*p*> = {} proof let p be Point of (TOP-REAL 2); ::_thesis: L~ <*p*> = {} len <*p*> = 1 by FINSEQ_1:39; hence L~ <*p*> = {} by TOPREAL1:22; ::_thesis: verum end; theorem Th13: :: SPPOL_2:13 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in L~ f holds ex i being Element of NAT st ( 1 <= i & i + 1 <= len f & p in LSeg (f,i) ) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st p in L~ f holds ex i being Element of NAT st ( 1 <= i & i + 1 <= len f & p in LSeg (f,i) ) let p be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f implies ex i being Element of NAT st ( 1 <= i & i + 1 <= len f & p in LSeg (f,i) ) ) set X = { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ; assume p in L~ f ; ::_thesis: ex i being Element of NAT st ( 1 <= i & i + 1 <= len f & p in LSeg (f,i) ) then consider Y being set such that A1: p in Y and A2: Y in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by TARSKI:def_4; ex i being Element of NAT st ( Y = LSeg (f,i) & 1 <= i & i + 1 <= len f ) by A2; hence ex i being Element of NAT st ( 1 <= i & i + 1 <= len f & p in LSeg (f,i) ) by A1; ::_thesis: verum end; theorem Th14: :: SPPOL_2:14 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in L~ f holds ex i being Element of NAT st ( 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) ) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st p in L~ f holds ex i being Element of NAT st ( 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) ) let p be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f implies ex i being Element of NAT st ( 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) ) ) assume p in L~ f ; ::_thesis: ex i being Element of NAT st ( 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) ) then consider i being Element of NAT such that A1: 1 <= i and A2: i + 1 <= len f and A3: p in LSeg (f,i) by Th13; take i ; ::_thesis: ( 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) ) thus ( 1 <= i & i + 1 <= len f ) by A1, A2; ::_thesis: p in LSeg ((f /. i),(f /. (i + 1))) thus p in LSeg ((f /. i),(f /. (i + 1))) by A1, A2, A3, TOPREAL1:def_3; ::_thesis: verum end; theorem Th15: :: SPPOL_2:15 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) for i being Element of NAT st 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) holds p in L~ f proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) for i being Element of NAT st 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) holds p in L~ f let p be Point of (TOP-REAL 2); ::_thesis: for i being Element of NAT st 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) holds p in L~ f let i be Element of NAT ; ::_thesis: ( 1 <= i & i + 1 <= len f & p in LSeg ((f /. i),(f /. (i + 1))) implies p in L~ f ) assume that A1: 1 <= i and A2: i + 1 <= len f and A3: p in LSeg ((f /. i),(f /. (i + 1))) ; ::_thesis: p in L~ f set X = { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ; A4: LSeg (f,i) in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A1, A2; LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A1, A2, TOPREAL1:def_3; hence p in L~ f by A3, A4, TARSKI:def_4; ::_thesis: verum end; theorem :: SPPOL_2:16 for f being FinSequence of (TOP-REAL 2) for i being Element of NAT st 1 <= i & i + 1 <= len f holds LSeg ((f /. i),(f /. (i + 1))) c= L~ f proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for i being Element of NAT st 1 <= i & i + 1 <= len f holds LSeg ((f /. i),(f /. (i + 1))) c= L~ f let i be Element of NAT ; ::_thesis: ( 1 <= i & i + 1 <= len f implies LSeg ((f /. i),(f /. (i + 1))) c= L~ f ) assume that A1: 1 <= i and A2: i + 1 <= len f ; ::_thesis: LSeg ((f /. i),(f /. (i + 1))) c= L~ f LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A1, A2, TOPREAL1:def_3; hence LSeg ((f /. i),(f /. (i + 1))) c= L~ f by TOPREAL3:19; ::_thesis: verum end; theorem :: SPPOL_2:17 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) for i being Element of NAT st p in LSeg (f,i) holds p in L~ f proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) for i being Element of NAT st p in LSeg (f,i) holds p in L~ f let p be Point of (TOP-REAL 2); ::_thesis: for i being Element of NAT st p in LSeg (f,i) holds p in L~ f let i be Element of NAT ; ::_thesis: ( p in LSeg (f,i) implies p in L~ f ) LSeg (f,i) c= L~ f by TOPREAL3:19; hence ( p in LSeg (f,i) implies p in L~ f ) ; ::_thesis: verum end; theorem Th18: :: SPPOL_2:18 for f being FinSequence of (TOP-REAL 2) st len f >= 2 holds rng f c= L~ f proof let f be FinSequence of (TOP-REAL 2); ::_thesis: ( len f >= 2 implies rng f c= L~ f ) assume A1: len f >= 2 ; ::_thesis: rng f c= L~ f let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in L~ f ) assume x in rng f ; ::_thesis: x in L~ f then consider i being Element of NAT 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; percases ( i = len f or i <> len f ) ; supposeA7: i = len f ; ::_thesis: x in L~ f then consider j being Nat such that A8: j + 1 = i by A1, NAT_1:6; reconsider j = 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 x in L~ f by A3, A7, A8, A9, Th15; ::_thesis: verum end; suppose i <> len f ; ::_thesis: x in L~ f then i < len f by A5, XXREAL_0:1; then i + 1 <= len f by NAT_1:13; hence x in L~ f by A3, A4, A6, Th15; ::_thesis: verum end; end; end; theorem Th19: :: SPPOL_2:19 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st not f is empty holds L~ (f ^ <*p*>) = (L~ f) \/ (LSeg ((f /. (len f)),p)) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st not f is empty holds L~ (f ^ <*p*>) = (L~ f) \/ (LSeg ((f /. (len f)),p)) let p be Point of (TOP-REAL 2); ::_thesis: ( not f is empty implies L~ (f ^ <*p*>) = (L~ f) \/ (LSeg ((f /. (len f)),p)) ) set fp = f ^ <*p*>; A1: (len f) + 1 <= len (f ^ <*p*>) by FINSEQ_2:16; 1 <= (len f) + 1 by NAT_1:11; then A2: (len f) + 1 in dom (f ^ <*p*>) by A1, FINSEQ_3:25; A3: (f ^ <*p*>) /. ((len f) + 1) = p by FINSEQ_4:67; len (f ^ <*p*>) = (len f) + 1 by FINSEQ_2:16; then A4: (f ^ <*p*>) | ((len f) + 1) = f ^ <*p*> by FINSEQ_1:58; A5: dom f c= dom (f ^ <*p*>) by FINSEQ_1:26; A6: (f ^ <*p*>) | (len f) = f by FINSEQ_5:23; assume not f is empty ; ::_thesis: L~ (f ^ <*p*>) = (L~ f) \/ (LSeg ((f /. (len f)),p)) then A7: len f in dom f by FINSEQ_5:6; then (f ^ <*p*>) /. (len f) = f /. (len f) by FINSEQ_4:68; hence L~ (f ^ <*p*>) = (L~ f) \/ (LSeg ((f /. (len f)),p)) by A2, A7, A3, A4, A5, A6, TOPREAL3:38; ::_thesis: verum end; theorem Th20: :: SPPOL_2:20 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st not f is empty holds L~ (<*p*> ^ f) = (LSeg (p,(f /. 1))) \/ (L~ f) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st not f is empty holds L~ (<*p*> ^ f) = (LSeg (p,(f /. 1))) \/ (L~ f) let p be Point of (TOP-REAL 2); ::_thesis: ( not f is empty implies L~ (<*p*> ^ f) = (LSeg (p,(f /. 1))) \/ (L~ f) ) 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 A3: not f is empty ; ::_thesis: L~ (<*p*> ^ f) = (LSeg (p,(f /. 1))) \/ (L~ f) hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: (LSeg (p,(f /. 1))) \/ (L~ f) c= L~ (<*p*> ^ f) let x be set ; ::_thesis: ( x in L~ (<*p*> ^ f) implies x in (LSeg (p,(f /. 1))) \/ (L~ f) ) assume A4: x in L~ (<*p*> ^ f) ; ::_thesis: x in (LSeg (p,(f /. 1))) \/ (L~ f) then reconsider r = x as Point of (TOP-REAL 2) ; consider i being Element of NAT 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__::_thesis:_(_(_i_=_1_&_r_in_LSeg_(p,(f_/._1))_)_or_(_i_>_1_&_r_in_L~_f_)_) percases ( i = 1 or i > 1 ) by A5, XXREAL_0:1; caseA8: i = 1 ; ::_thesis: r in LSeg (p,(f /. 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,(f /. 1)) by A1, A7, A8, A9, FINSEQ_4:69; ::_thesis: verum end; caseA10: i > 1 ; ::_thesis: r in L~ f then consider j being Nat such that A11: i = j + 1 by NAT_1:6; reconsider j = 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; ::_thesis: verum end; end; end; hence x in (LSeg (p,(f /. 1))) \/ (L~ f) by XBOOLE_0:def_3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (LSeg (p,(f /. 1))) \/ (L~ f) or x in L~ (<*p*> ^ f) ) assume A15: x in (LSeg (p,(f /. 1))) \/ (L~ f) ; ::_thesis: x in L~ (<*p*> ^ f) then reconsider r = x as Point of (TOP-REAL 2) ; percases ( r in LSeg (p,(f /. 1)) or r in L~ f ) by A15, XBOOLE_0:def_3; supposeA16: r in LSeg (p,(f /. 1)) ; ::_thesis: x in L~ (<*p*> ^ f) set i = 1; 1 <= len f by A3, NAT_1:14; then A17: 1 + 1 <= len (<*p*> ^ f) by A2, XREAL_1:6; 1 in dom f by A3, FINSEQ_5:6; then A18: f /. 1 = (<*p*> ^ f) /. (1 + 1) by A1, FINSEQ_4:69; p = (<*p*> ^ f) /. 1 by FINSEQ_5:15; hence x in L~ (<*p*> ^ f) by A16, A17, A18, Th15; ::_thesis: verum end; suppose r in L~ f ; ::_thesis: x in L~ (<*p*> ^ f) then consider j being Element of NAT 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) /. (j + 1) = f /. j by A1, FINSEQ_4:69; j + 1 in dom f by A19, A20, SEQ_4:134; then A23: (<*p*> ^ f) /. ((j + 1) + 1) = f /. (j + 1) by A1, FINSEQ_4:69; (j + 1) + 1 <= len (<*p*> ^ f) by A2, A20, XREAL_1:6; hence x in L~ (<*p*> ^ f) by A21, A22, A23, Th15, NAT_1:12; ::_thesis: verum end; end; end; theorem Th21: :: SPPOL_2:21 for p, q being Point of (TOP-REAL 2) holds L~ <*p,q*> = LSeg (p,q) proof let p, q be Point of (TOP-REAL 2); ::_thesis: L~ <*p,q*> = LSeg (p,q) set f = <*p*>; A1: len <*p*> = 1 by FINSEQ_1:39; thus L~ <*p,q*> = L~ (<*p*> ^ <*q*>) by FINSEQ_1:def_9 .= (L~ <*p*>) \/ (LSeg ((<*p*> /. (len <*p*>)),q)) by Th19 .= (L~ <*p*>) \/ (LSeg (p,q)) by A1, FINSEQ_4:16 .= {} \/ (LSeg (p,q)) by A1, TOPREAL1:22 .= LSeg (p,q) ; ::_thesis: verum end; theorem Th22: :: SPPOL_2:22 for f being FinSequence of (TOP-REAL 2) holds L~ f = L~ (Rev f) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: L~ f = L~ (Rev f) defpred S1[ FinSequence of (TOP-REAL 2)] means L~ $1 = L~ (Rev $1); A1: for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st S1[f] holds S1[f ^ <*p*>] proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st S1[f] holds S1[f ^ <*p*>] let p be Point of (TOP-REAL 2); ::_thesis: ( S1[f] implies S1[f ^ <*p*>] ) assume A2: S1[f] ; ::_thesis: S1[f ^ <*p*>] percases ( f is empty or not f is empty ) ; supposeA3: f is empty ; ::_thesis: S1[f ^ <*p*>] 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 ; ::_thesis: verum end; supposeA4: not f is empty ; ::_thesis: S1[f ^ <*p*>] set q9 = (Rev f) /. 1; set q = f /. (len f); len f = len (Rev f) by FINSEQ_5:def_3; then A5: not Rev f is empty by A4; f /. (len f) = (Rev f) /. 1 by A4, FINSEQ_5:65; hence L~ (f ^ <*p*>) = (LSeg (p,((Rev f) /. 1))) \/ (L~ (Rev f)) by A2, A4, Th19 .= L~ (<*p*> ^ (Rev f)) by A5, Th20 .= L~ (Rev (f ^ <*p*>)) by FINSEQ_5:63 ; ::_thesis: verum end; end; end; A6: S1[ <*> the carrier of (TOP-REAL 2)] ; for f being FinSequence of (TOP-REAL 2) holds S1[f] from FINSEQ_2:sch_2(A6, A1); hence L~ f = L~ (Rev f) ; ::_thesis: verum end; theorem Th23: :: SPPOL_2:23 for f1, f2 being FinSequence of (TOP-REAL 2) st not f1 is empty & not f2 is empty holds L~ (f1 ^ f2) = ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ f2) proof let f1, f2 be FinSequence of (TOP-REAL 2); ::_thesis: ( not f1 is empty & not f2 is empty implies L~ (f1 ^ f2) = ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ f2) ) set p = f1 /. (len f1); set q = f2 /. 1; defpred S1[ FinSequence of (TOP-REAL 2)] means L~ ((f1 ^ <*(f2 /. 1)*>) ^ $1) = ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ (<*(f2 /. 1)*> ^ $1)); assume A1: not f1 is empty ; ::_thesis: ( f2 is empty or L~ (f1 ^ f2) = ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ f2) ) A2: for f being FinSequence of (TOP-REAL 2) for o being Point of (TOP-REAL 2) st S1[f] holds S1[f ^ <*o*>] proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for o being Point of (TOP-REAL 2) st S1[f] holds S1[f ^ <*o*>] let o be Point of (TOP-REAL 2); ::_thesis: ( S1[f] implies S1[f ^ <*o*>] ) assume A3: S1[f] ; ::_thesis: S1[f ^ <*o*>] percases ( f is empty or not f is empty ) ; suppose f is empty ; ::_thesis: S1[f ^ <*o*>] then A4: f ^ <*o*> = <*o*> by FINSEQ_1:34; len (f1 ^ <*(f2 /. 1)*>) = (len f1) + 1 by FINSEQ_2:16; then (f1 ^ <*(f2 /. 1)*>) /. (len (f1 ^ <*(f2 /. 1)*>)) = f2 /. 1 by FINSEQ_4:67; hence L~ ((f1 ^ <*(f2 /. 1)*>) ^ (f ^ <*o*>)) = (L~ (f1 ^ <*(f2 /. 1)*>)) \/ (LSeg ((f2 /. 1),o)) by A4, Th19 .= ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (LSeg ((f2 /. 1),o)) by A1, Th19 .= ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ <*(f2 /. 1),o*>) by Th21 .= ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ (<*(f2 /. 1)*> ^ (f ^ <*o*>))) by A4, FINSEQ_1:def_9 ; ::_thesis: verum end; supposeA5: not f is empty ; ::_thesis: S1[f ^ <*o*>] set g = (f1 ^ <*(f2 /. 1)*>) ^ f; set h = <*(f2 /. 1)*> ^ 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: <*(f2 /. 1)*> ^ f = (<*(f2 /. 1)*> ^ f9) ^ <*d*> by A6, FINSEQ_1:32; then len (<*(f2 /. 1)*> ^ f) = (len (<*(f2 /. 1)*> ^ f9)) + 1 by FINSEQ_2:16; then A8: (<*(f2 /. 1)*> ^ f) /. (len (<*(f2 /. 1)*> ^ f)) = d by A7, FINSEQ_4:67; A9: (f1 ^ <*(f2 /. 1)*>) ^ f = ((f1 ^ <*(f2 /. 1)*>) ^ f9) ^ <*d*> by A6, FINSEQ_1:32; then len ((f1 ^ <*(f2 /. 1)*>) ^ f) = (len ((f1 ^ <*(f2 /. 1)*>) ^ f9)) + 1 by FINSEQ_2:16; then ((f1 ^ <*(f2 /. 1)*>) ^ f) /. (len ((f1 ^ <*(f2 /. 1)*>) ^ f)) = d by A9, FINSEQ_4:67; then A10: (L~ (<*(f2 /. 1)*> ^ f)) \/ (LSeg ((((f1 ^ <*(f2 /. 1)*>) ^ f) /. (len ((f1 ^ <*(f2 /. 1)*>) ^ f))),o)) = L~ ((<*(f2 /. 1)*> ^ f) ^ <*o*>) by A8, Th19 .= L~ (<*(f2 /. 1)*> ^ (f ^ <*o*>)) by FINSEQ_1:32 ; thus L~ ((f1 ^ <*(f2 /. 1)*>) ^ (f ^ <*o*>)) = L~ (((f1 ^ <*(f2 /. 1)*>) ^ f) ^ <*o*>) by FINSEQ_1:32 .= (L~ ((f1 ^ <*(f2 /. 1)*>) ^ f)) \/ (LSeg ((((f1 ^ <*(f2 /. 1)*>) ^ f) /. (len ((f1 ^ <*(f2 /. 1)*>) ^ f))),o)) by Th19 .= ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ (<*(f2 /. 1)*> ^ (f ^ <*o*>))) by A3, A10, XBOOLE_1:4 ; ::_thesis: verum end; end; end; assume not f2 is empty ; ::_thesis: L~ (f1 ^ f2) = ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ f2) then A11: f2 = <*(f2 /. 1)*> ^ (f2 /^ 1) by FINSEQ_5:29; A12: S1[ <*> the carrier of (TOP-REAL 2)] proof set O = <*> the carrier of (TOP-REAL 2); thus L~ ((f1 ^ <*(f2 /. 1)*>) ^ (<*> the carrier of (TOP-REAL 2))) = L~ (f1 ^ <*(f2 /. 1)*>) by FINSEQ_1:34 .= ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ {} by A1, Th19 .= ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ <*(f2 /. 1)*>) by Th12 .= ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ (<*(f2 /. 1)*> ^ (<*> the carrier of (TOP-REAL 2)))) by FINSEQ_1:34 ; ::_thesis: verum end; for f being FinSequence of (TOP-REAL 2) holds S1[f] from FINSEQ_2:sch_2(A12, A2); then L~ ((f1 ^ <*(f2 /. 1)*>) ^ (f2 /^ 1)) = ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ (<*(f2 /. 1)*> ^ (f2 /^ 1))) ; hence L~ (f1 ^ f2) = ((L~ f1) \/ (LSeg ((f1 /. (len f1)),(f2 /. 1)))) \/ (L~ f2) by A11, FINSEQ_1:32; ::_thesis: verum end; Lm1: for f being FinSequence of (TOP-REAL 2) for n being Element of NAT holds L~ (f | n) c= L~ f proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for n being Element of NAT holds L~ (f | n) c= L~ f let n be Element of NAT ; ::_thesis: L~ (f | n) c= L~ f now__::_thesis:_L~_(f_|_n)_c=_L~_f percases ( n = 0 or n <> 0 ) ; supposeA1: n = 0 ; ::_thesis: L~ (f | n) c= L~ f f | 0 is empty ; hence L~ (f | n) c= L~ f by A1, Th11, XBOOLE_1:2; ::_thesis: verum end; supposeA2: n <> 0 ; ::_thesis: L~ (f | n) c= L~ f now__::_thesis:_L~_(f_|_n)_c=_L~_f percases ( n < len f or n >= len f ) ; supposeA3: n < len f ; ::_thesis: L~ (f | n) c= L~ f then len (f /^ n) = (len f) - n by RFINSEQ:def_1; then len (f /^ n) <> 0 by A3; then A4: not f /^ n is empty ; len (f | n) = n by A3, FINSEQ_1:59; then A5: not f | n is 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 L~ (f | n) c= L~ f by XBOOLE_1:7; ::_thesis: verum end; suppose n >= len f ; ::_thesis: L~ (f | n) c= L~ f hence L~ (f | n) c= L~ f by FINSEQ_1:58; ::_thesis: verum end; end; end; hence L~ (f | n) c= L~ f ; ::_thesis: verum end; end; end; hence L~ (f | n) c= L~ f ; ::_thesis: verum end; theorem Th24: :: SPPOL_2:24 for f being FinSequence of (TOP-REAL 2) for q being Point of (TOP-REAL 2) st q in rng f holds L~ f = (L~ (f -: q)) \/ (L~ (f :- q)) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for q being Point of (TOP-REAL 2) st q in rng f holds L~ f = (L~ (f -: q)) \/ (L~ (f :- q)) let q be Point of (TOP-REAL 2); ::_thesis: ( q in rng f implies L~ f = (L~ (f -: q)) \/ (L~ (f :- q)) ) set n = q .. f; assume A1: q in rng f ; ::_thesis: L~ f = (L~ (f -: q)) \/ (L~ (f :- q)) then A2: q .. f <= len f by FINSEQ_4:21; percases ( q .. f < len f or q .. f = len f ) by A2, XXREAL_0:1; supposeA3: q .. f < len f ; ::_thesis: L~ f = (L~ (f -: q)) \/ (L~ (f :- q)) then len (f /^ (q .. f)) = (len f) - (q .. f) by RFINSEQ:def_1; then len (f /^ (q .. f)) <> 0 by A3; then A4: not f /^ (q .. f) is empty ; A5: len (f | (q .. f)) = q .. f by A3, FINSEQ_1:59; f | (q .. f) = f -: q by FINSEQ_5:def_1; then A6: (f | (q .. f)) /. (len (f | (q .. f))) = q by A1, A5, FINSEQ_5:45; A7: (f | (q .. f)) ^ (f /^ (q .. f)) = f by RFINSEQ:8; not f | (q .. f) is empty by A1, A5, FINSEQ_4:21; hence L~ f = ((L~ (f | (q .. f))) \/ (LSeg (((f | (q .. f)) /. (len (f | (q .. f)))),((f /^ (q .. f)) /. 1)))) \/ (L~ (f /^ (q .. f))) by A4, A7, Th23 .= (L~ (f | (q .. f))) \/ ((LSeg (((f | (q .. f)) /. (len (f | (q .. f)))),((f /^ (q .. f)) /. 1))) \/ (L~ (f /^ (q .. f)))) by XBOOLE_1:4 .= (L~ (f | (q .. f))) \/ (L~ (<*((f | (q .. f)) /. (len (f | (q .. f))))*> ^ (f /^ (q .. f)))) by A4, Th20 .= (L~ (f | (q .. f))) \/ (L~ (f :- q)) by A6, FINSEQ_5:def_2 .= (L~ (f -: q)) \/ (L~ (f :- q)) by FINSEQ_5:def_1 ; ::_thesis: verum end; supposeA8: q .. f = len f ; ::_thesis: L~ f = (L~ (f -: q)) \/ (L~ (f :- q)) then len (f /^ (q .. f)) = (len f) - (q .. f) by RFINSEQ:def_1 .= 0 by A8 ; then A9: f /^ (q .. f) is empty ; f :- q = <*q*> ^ (f /^ (q .. f)) by FINSEQ_5:def_2 .= <*q*> by A9, FINSEQ_1:34 ; then A10: L~ (f :- q) is empty by Th12; L~ f = L~ (f | (q .. f)) by A8, FINSEQ_1:58 .= L~ (f -: q) by FINSEQ_5:def_1 ; hence L~ f = (L~ (f -: q)) \/ (L~ (f :- q)) by A10; ::_thesis: verum end; end; end; theorem Th25: :: SPPOL_2:25 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) for n being Element of NAT st p in LSeg (f,n) holds L~ f = L~ (Ins (f,n,p)) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) for n being Element of NAT st p in LSeg (f,n) holds L~ f = L~ (Ins (f,n,p)) let p be Point of (TOP-REAL 2); ::_thesis: for n being Element of NAT st p in LSeg (f,n) holds L~ f = L~ (Ins (f,n,p)) let n be Element of NAT ; ::_thesis: ( p in LSeg (f,n) implies L~ f = L~ (Ins (f,n,p)) ) set f1 = f | n; set g1 = (f | n) ^ <*p*>; set f2 = f /^ n; A1: ((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>)) = ((f | n) ^ <*p*>) /. ((len (f | n)) + 1) by FINSEQ_2:16 .= p by FINSEQ_4:67 ; assume A2: p in LSeg (f,n) ; ::_thesis: L~ f = L~ (Ins (f,n,p)) 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 (f | n) = n by A3, FINSEQ_1:59, XXREAL_0:2; then A7: not f | n is empty by A2, TOPREAL1:def_3; A8: 1 <= n by A2, TOPREAL1:def_3; then A9: n in dom (f | n) by A6, FINSEQ_3:25; n <= len f by A3, A5, XXREAL_0:2; then 1 <= len (f /^ n) by A4, RFINSEQ:def_1; then A10: 1 in dom (f /^ n) by FINSEQ_3:25; A11: LSeg (f,n) = LSeg ((f /. n),(f /. (n + 1))) by A8, A3, TOPREAL1:def_3 .= LSeg (((f | n) /. (len (f | n))),(f /. (n + 1))) by A6, A9, FINSEQ_4:70 .= LSeg (((f | n) /. (len (f | n))),((f /^ n) /. 1)) by A10, FINSEQ_5:27 ; thus L~ (Ins (f,n,p)) = L~ (((f | n) ^ <*p*>) ^ (f /^ n)) by FINSEQ_5:def_4 .= ((L~ ((f | n) ^ <*p*>)) \/ (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1)))) \/ (L~ (f /^ n)) by A10, Th23, RELAT_1:38 .= (((L~ (f | n)) \/ (LSeg (((f | n) /. (len (f | n))),p))) \/ (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1)))) \/ (L~ (f /^ n)) by A9, Th19, RELAT_1:38 .= ((L~ (f | n)) \/ ((LSeg (((f | n) /. (len (f | n))),p)) \/ (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))))) \/ (L~ (f /^ n)) by XBOOLE_1:4 .= ((L~ (f | n)) \/ (LSeg (((f | n) /. (len (f | n))),((f /^ n) /. 1)))) \/ (L~ (f /^ n)) by A2, A1, A11, TOPREAL1:5 .= L~ ((f | n) ^ (f /^ n)) by A7, A10, Th23, RELAT_1:38 .= L~ f by RFINSEQ:8 ; ::_thesis: verum end; begin registration clusterV15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like V32() FinSequence-like FinSubsequence-like being_S-Seq for FinSequence of the carrier of (TOP-REAL 2); existence ex b1 being FinSequence of (TOP-REAL 2) st b1 is being_S-Seq proof set p = |[0,0]|; set q = |[1,1]|; A1: |[0,0]| `2 = 0 by EUCLID:52; A2: |[1,1]| `1 = 1 by EUCLID:52; A3: |[1,1]| `2 = 1 by EUCLID:52; |[0,0]| `1 = 0 by EUCLID:52; then <*|[0,0]|,|[(|[0,0]| `1),(|[1,1]| `2)]|,|[1,1]|*> is being_S-Seq by A1, A2, A3, TOPREAL3:34; hence ex b1 being FinSequence of (TOP-REAL 2) st b1 is being_S-Seq ; ::_thesis: verum end; cluster being_S-Seq -> non trivial one-to-one special unfolded s.n.c. for FinSequence of the carrier of (TOP-REAL 2); coherence for b1 being FinSequence of (TOP-REAL 2) st b1 is being_S-Seq holds ( b1 is one-to-one & b1 is unfolded & b1 is s.n.c. & b1 is special & not b1 is trivial ) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is being_S-Seq implies ( f is one-to-one & f is unfolded & f is s.n.c. & f is special & not f is trivial ) ) assume A4: f is being_S-Seq ; ::_thesis: ( f is one-to-one & f is unfolded & f is s.n.c. & f is special & not f is trivial ) then len f >= 2 by TOPREAL1:def_8; hence ( f is one-to-one & f is unfolded & f is s.n.c. & f is special & not f is trivial ) by A4, NAT_D:60, TOPREAL1:def_8; ::_thesis: verum end; cluster non trivial one-to-one special unfolded s.n.c. -> being_S-Seq for FinSequence of the carrier of (TOP-REAL 2); coherence for b1 being FinSequence of (TOP-REAL 2) st b1 is one-to-one & b1 is unfolded & b1 is s.n.c. & b1 is special & not b1 is trivial holds b1 is being_S-Seq proof let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is one-to-one & f is unfolded & f is s.n.c. & f is special & not f is trivial implies f is being_S-Seq ) assume A5: ( f is one-to-one & f is unfolded & f is s.n.c. & f is special ) ; ::_thesis: ( f is trivial or f is being_S-Seq ) assume not f is trivial ; ::_thesis: f is being_S-Seq then len f >= 2 by NAT_D:60; hence f is being_S-Seq by A5, TOPREAL1:def_8; ::_thesis: verum end; cluster being_S-Seq -> non empty for FinSequence of the carrier of (TOP-REAL 2); coherence for b1 being FinSequence of (TOP-REAL 2) st b1 is being_S-Seq holds not b1 is empty by CARD_1:27, TOPREAL1:def_8; end; registration cluster non trivial V15() V18( NAT ) V19( the carrier of (TOP-REAL 2)) Function-like one-to-one V32() FinSequence-like FinSubsequence-like special unfolded s.n.c. for FinSequence of the carrier of (TOP-REAL 2); existence ex b1 being FinSequence of (TOP-REAL 2) st ( b1 is one-to-one & b1 is unfolded & b1 is s.n.c. & b1 is special & not b1 is trivial ) proof set f = the being_S-Seq FinSequence of (TOP-REAL 2); ( the being_S-Seq FinSequence of (TOP-REAL 2) is one-to-one & the being_S-Seq FinSequence of (TOP-REAL 2) is unfolded & the being_S-Seq FinSequence of (TOP-REAL 2) is s.n.c. & the being_S-Seq FinSequence of (TOP-REAL 2) is special & not the being_S-Seq FinSequence of (TOP-REAL 2) is trivial ) ; hence ex b1 being FinSequence of (TOP-REAL 2) st ( b1 is one-to-one & b1 is unfolded & b1 is s.n.c. & b1 is special & not b1 is trivial ) ; ::_thesis: verum end; end; theorem Th26: :: SPPOL_2:26 for f being FinSequence of (TOP-REAL 2) st len f <= 2 holds f is unfolded proof let f be FinSequence of (TOP-REAL 2); ::_thesis: ( len f <= 2 implies f is unfolded ) assume A1: len f <= 2 ; ::_thesis: f is unfolded let i be Nat; :: according to TOPREAL1:def_6 ::_thesis: ( not 1 <= i or not i + 2 <= len f or (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} ) assume A2: 1 <= i ; ::_thesis: ( not i + 2 <= len f or (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} ) assume i + 2 <= len f ; ::_thesis: (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} then i + 2 <= 2 by A1, XXREAL_0:2; then i <= 2 - 2 by XREAL_1:19; hence (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} by A2, XXREAL_0:2; ::_thesis: verum end; Lm2: for p, q being Point of (TOP-REAL 2) holds <*p,q*> is unfolded proof let p, q be Point of (TOP-REAL 2); ::_thesis: <*p,q*> is unfolded len <*p,q*> = 2 by FINSEQ_1:44; hence <*p,q*> is unfolded by Th26; ::_thesis: verum end; Lm3: for f being FinSequence of (TOP-REAL 2) for n being Element of NAT st f is unfolded holds f | n is unfolded proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for n being Element of NAT st f is unfolded holds f | n is unfolded let n be Element of NAT ; ::_thesis: ( f is unfolded implies f | n is unfolded ) assume A1: f is unfolded ; ::_thesis: f | n is unfolded set h = f | n; let i be Nat; :: according to TOPREAL1:def_6 ::_thesis: ( not 1 <= i or not i + 2 <= len (f | n) or (LSeg ((f | n),i)) /\ (LSeg ((f | n),(i + 1))) = {((f | n) /. (i + 1))} ) assume that A2: 1 <= i and A3: i + 2 <= len (f | n) ; ::_thesis: (LSeg ((f | n),i)) /\ (LSeg ((f | n),(i + 1))) = {((f | n) /. (i + 1))} A4: i + 1 in dom (f | n) by A2, A3, SEQ_4:135; len (f | n) <= 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 ((f | n),i)) /\ (LSeg ((f | n),(i + 1))) = (LSeg (f,i)) /\ (LSeg ((f | n),(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 .= {((f | n) /. (i + 1))} by A4, FINSEQ_4:70 ; ::_thesis: verum end; Lm4: for f being FinSequence of (TOP-REAL 2) for n being Element of NAT st f is unfolded holds f /^ n is unfolded proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for n being Element of NAT st f is unfolded holds f /^ n is unfolded let n be Element of NAT ; ::_thesis: ( f is unfolded implies f /^ n is unfolded ) assume A1: f is unfolded ; ::_thesis: f /^ n is unfolded percases ( n <= len f or n > len f ) ; supposeA2: n <= len f ; ::_thesis: f /^ n is unfolded set h = f /^ n; let i be Nat; :: according to TOPREAL1:def_6 ::_thesis: ( not 1 <= i or not i + 2 <= len (f /^ n) or (LSeg ((f /^ n),i)) /\ (LSeg ((f /^ n),(i + 1))) = {((f /^ n) /. (i + 1))} ) assume that A3: 1 <= i and A4: i + 2 <= len (f /^ n) ; ::_thesis: (LSeg ((f /^ n),i)) /\ (LSeg ((f /^ n),(i + 1))) = {((f /^ n) /. (i + 1))} A5: i + 1 in dom (f /^ n) by A3, A4, SEQ_4:135; A6: len (f /^ n) = (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 (f /^ n) by A4, XXREAL_0:2; hence (LSeg ((f /^ n),i)) /\ (LSeg ((f /^ n),(i + 1))) = (LSeg (f,(n + i))) /\ (LSeg ((f /^ n),(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)))} .= {((f /^ n) /. (i + 1))} by A5, FINSEQ_5:27 ; ::_thesis: verum end; suppose n > len f ; ::_thesis: f /^ n is unfolded then f /^ n = <*> the carrier of (TOP-REAL 2) by RFINSEQ:def_1; then len (f /^ n) = 0 ; hence f /^ n is unfolded by Th26; ::_thesis: verum end; end; end; registration let f be unfolded FinSequence of (TOP-REAL 2); let n be Element of NAT ; clusterf | n -> unfolded for FinSequence of (TOP-REAL 2); coherence for b1 being FinSequence of (TOP-REAL 2) st b1 = f | n holds b1 is unfolded by Lm3; clusterf /^ n -> unfolded for FinSequence of (TOP-REAL 2); coherence for b1 being FinSequence of (TOP-REAL 2) st b1 = f /^ n holds b1 is unfolded by Lm4; end; theorem Th27: :: SPPOL_2:27 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in rng f & f is unfolded holds f :- p is unfolded proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st p in rng f & f is unfolded holds f :- p is unfolded let p be Point of (TOP-REAL 2); ::_thesis: ( p in rng f & f is unfolded implies f :- p is unfolded ) assume p in rng f ; ::_thesis: ( not f is unfolded or f :- p is unfolded ) then ex i being Element of NAT st ( i + 1 = p .. f & f :- p = f /^ i ) by FINSEQ_5:49; hence ( not f is unfolded or f :- p is unfolded ) ; ::_thesis: verum end; Lm5: for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st f is unfolded holds f -: p is unfolded proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st f is unfolded holds f -: p is unfolded let p be Point of (TOP-REAL 2); ::_thesis: ( f is unfolded implies f -: p is unfolded ) f -: p = f | (p .. f) by FINSEQ_5:def_1; hence ( f is unfolded implies f -: p is unfolded ) ; ::_thesis: verum end; registration let f be unfolded FinSequence of (TOP-REAL 2); let p be Point of (TOP-REAL 2); clusterf -: p -> unfolded ; coherence f -: p is unfolded by Lm5; end; theorem Th28: :: SPPOL_2:28 for f being FinSequence of (TOP-REAL 2) st f is unfolded holds Rev f is unfolded proof let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is unfolded implies Rev f is unfolded ) assume A1: f is unfolded ; ::_thesis: Rev f is unfolded A2: dom f = Seg (len f) by FINSEQ_1:def_3; let i be Nat; :: according to TOPREAL1:def_6 ::_thesis: ( not 1 <= i or not i + 2 <= len (Rev f) or (LSeg ((Rev f),i)) /\ (LSeg ((Rev f),(i + 1))) = {((Rev f) /. (i + 1))} ) assume that A3: 1 <= i and A4: i + 2 <= len (Rev f) ; ::_thesis: (LSeg ((Rev f),i)) /\ (LSeg ((Rev f),(i + 1))) = {((Rev f) /. (i + 1))} 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, FINSEQ_5:66 ; ::_thesis: verum end; theorem Th29: :: SPPOL_2:29 for g being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st g is unfolded & (LSeg (p,(g /. 1))) /\ (LSeg (g,1)) = {(g /. 1)} holds <*p*> ^ g is unfolded proof let g be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st g is unfolded & (LSeg (p,(g /. 1))) /\ (LSeg (g,1)) = {(g /. 1)} holds <*p*> ^ g is unfolded let p be Point of (TOP-REAL 2); ::_thesis: ( g is unfolded & (LSeg (p,(g /. 1))) /\ (LSeg (g,1)) = {(g /. 1)} implies <*p*> ^ g is unfolded ) set f = <*p*>; A1: len <*p*> = 1 by FINSEQ_1:39; A2: <*p*> /. 1 = p by FINSEQ_4:16; A3: len (<*p*> ^ g) = (len <*p*>) + (len g) by FINSEQ_1:22; assume that A4: g is unfolded and A5: (LSeg (p,(g /. 1))) /\ (LSeg (g,1)) = {(g /. 1)} ; ::_thesis: <*p*> ^ g is unfolded let i be Nat; :: according to TOPREAL1:def_6 ::_thesis: ( not 1 <= i or not i + 2 <= len (<*p*> ^ g) or (LSeg ((<*p*> ^ g),i)) /\ (LSeg ((<*p*> ^ g),(i + 1))) = {((<*p*> ^ g) /. (i + 1))} ) assume that A6: 1 <= i and A7: i + 2 <= len (<*p*> ^ g) ; ::_thesis: (LSeg ((<*p*> ^ g),i)) /\ (LSeg ((<*p*> ^ g),(i + 1))) = {((<*p*> ^ g) /. (i + 1))} A8: i + (1 + 1) = (i + 1) + 1 ; percases ( i = len <*p*> or i <> len <*p*> ) ; supposeA9: i = len <*p*> ; ::_thesis: (LSeg ((<*p*> ^ g),i)) /\ (LSeg ((<*p*> ^ g),(i + 1))) = {((<*p*> ^ g) /. (i + 1))} then A10: LSeg ((<*p*> ^ g),(i + 1)) = LSeg (g,1) by Th7; now__::_thesis:_not_len_g_=_0 i <= i + 1 by NAT_1:11; then A11: i < i + (1 + 1) by A8, NAT_1:13; assume len g = 0 ; ::_thesis: contradiction hence contradiction by A1, A6, A7, A3, A11, XXREAL_0:2; ::_thesis: verum end; then 1 <= len g by NAT_1:14; then A12: 1 in dom g by FINSEQ_3:25; then LSeg ((<*p*> ^ g),i) = LSeg ((<*p*> /. (len <*p*>)),(g /. 1)) by A9, Th8, RELAT_1:38; hence (LSeg ((<*p*> ^ g),i)) /\ (LSeg ((<*p*> ^ g),(i + 1))) = {((<*p*> ^ g) /. (i + 1))} by A1, A5, A2, A9, A12, A10, FINSEQ_4:69; ::_thesis: verum end; supposeA13: i <> len <*p*> ; ::_thesis: (LSeg ((<*p*> ^ g),i)) /\ (LSeg ((<*p*> ^ g),(i + 1))) = {((<*p*> ^ g) /. (i + 1))} reconsider j = i - (len <*p*>) as Element of NAT by A1, A6, INT_1:5; i > len <*p*> by A1, A6, A13, XXREAL_0:1; then (len <*p*>) + 1 <= i by NAT_1:13; then A14: 1 <= j by XREAL_1:19; A15: (i + 2) - (len <*p*>) <= 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 <*p*>) + (j + 1) = i + 1 ; (len <*p*>) + j = i ; hence (LSeg ((<*p*> ^ g),i)) /\ (LSeg ((<*p*> ^ g),(i + 1))) = (LSeg (g,j)) /\ (LSeg ((<*p*> ^ 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 .= {((<*p*> ^ g) /. (i + 1))} by A18, A17, FINSEQ_4:69 ; ::_thesis: verum end; end; end; theorem Th30: :: SPPOL_2:30 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) for k being Element of NAT st f is unfolded & k + 1 = len f & (LSeg (f,k)) /\ (LSeg ((f /. (len f)),p)) = {(f /. (len f))} holds f ^ <*p*> is unfolded proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) for k being Element of NAT st f is unfolded & k + 1 = len f & (LSeg (f,k)) /\ (LSeg ((f /. (len f)),p)) = {(f /. (len f))} holds f ^ <*p*> is unfolded let p be Point of (TOP-REAL 2); ::_thesis: for k being Element of NAT st f is unfolded & k + 1 = len f & (LSeg (f,k)) /\ (LSeg ((f /. (len f)),p)) = {(f /. (len f))} holds f ^ <*p*> is unfolded let k be Element of NAT ; ::_thesis: ( f is unfolded & k + 1 = len f & (LSeg (f,k)) /\ (LSeg ((f /. (len f)),p)) = {(f /. (len f))} implies f ^ <*p*> is unfolded ) 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))} ; ::_thesis: f ^ <*p*> is unfolded A4: len <*p*> = 1 by FINSEQ_1:39; A5: <*p*> /. 1 = p by FINSEQ_4:16; A6: len (f ^ <*p*>) = (len f) + (len <*p*>) by FINSEQ_1:22; let i be Nat; :: according to TOPREAL1:def_6 ::_thesis: ( not 1 <= i or not i + 2 <= len (f ^ <*p*>) or (LSeg ((f ^ <*p*>),i)) /\ (LSeg ((f ^ <*p*>),(i + 1))) = {((f ^ <*p*>) /. (i + 1))} ) assume that A7: 1 <= i and A8: i + 2 <= len (f ^ <*p*>) ; ::_thesis: (LSeg ((f ^ <*p*>),i)) /\ (LSeg ((f ^ <*p*>),(i + 1))) = {((f ^ <*p*>) /. (i + 1))} A9: i + (1 + 1) = (i + 1) + 1 ; percases ( i + 2 <= len f or i + 2 > len f ) ; supposeA10: i + 2 <= len f ; ::_thesis: (LSeg ((f ^ <*p*>),i)) /\ (LSeg ((f ^ <*p*>),(i + 1))) = {((f ^ <*p*>) /. (i + 1))} then A11: i + 1 in dom f by A7, SEQ_4:135; i + 1 <= (i + 1) + 1 by NAT_1:11; hence (LSeg ((f ^ <*p*>),i)) /\ (LSeg ((f ^ <*p*>),(i + 1))) = (LSeg (f,i)) /\ (LSeg ((f ^ <*p*>),(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 ^ <*p*>) /. (i + 1))} by A11, FINSEQ_4:68 ; ::_thesis: verum end; suppose i + 2 > len f ; ::_thesis: (LSeg ((f ^ <*p*>),i)) /\ (LSeg ((f ^ <*p*>),(i + 1))) = {((f ^ <*p*>) /. (i + 1))} then A12: len f <= i + 1 by A9, NAT_1:13; A13: not f is 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 ^ <*p*>),(i + 1)) = LSeg ((f /. (len f)),(<*p*> /. 1)) by A13, Th8; LSeg ((f ^ <*p*>),i) = LSeg (f,k) by A2, A15, Th6; hence (LSeg ((f ^ <*p*>),i)) /\ (LSeg ((f ^ <*p*>),(i + 1))) = {((f ^ <*p*>) /. (i + 1))} by A3, A5, A15, A16, A14, FINSEQ_4:68; ::_thesis: verum end; end; end; theorem Th31: :: SPPOL_2:31 for f, g being FinSequence of (TOP-REAL 2) for k being Element of NAT st 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)} holds f ^ g is unfolded proof let f, g be FinSequence of (TOP-REAL 2); ::_thesis: for k being Element of NAT st 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)} holds f ^ g is unfolded let k be Element of NAT ; ::_thesis: ( 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 ) 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)} ; ::_thesis: f ^ g is unfolded let i be Nat; :: according to TOPREAL1:def_6 ::_thesis: ( not 1 <= i or not i + 2 <= len (f ^ g) or (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),(i + 1))) = {((f ^ g) /. (i + 1))} ) assume that A6: 1 <= i and A7: i + 2 <= len (f ^ g) ; ::_thesis: (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),(i + 1))) = {((f ^ g) /. (i + 1))} A8: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22; percases ( i + 2 <= len f or i + 2 > len f ) ; supposeA9: i + 2 <= len f ; ::_thesis: (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),(i + 1))) = {((f ^ g) /. (i + 1))} 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 ; ::_thesis: verum end; supposeA12: i + 2 > len f ; ::_thesis: (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),(i + 1))) = {((f ^ g) /. (i + 1))} A13: i + (1 + 1) = (i + 1) + 1 ; now__::_thesis:_(LSeg_((f_^_g),i))_/\_(LSeg_((f_^_g),(i_+_1)))_=_{((f_^_g)_/._(i_+_1))} percases ( i <= len f or i > len f ) ; supposeA14: i <= len f ; ::_thesis: (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),(i + 1))) = {((f ^ g) /. (i + 1))} 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: not f is empty by A6, A14; now__::_thesis:_(LSeg_((f_^_g),i))_/\_(LSeg_((f_^_g),(i_+_1)))_=_{((f_^_g)_/._(i_+_1))} percases ( i = len f or i <> len f ) ; supposeA17: i = len f ; ::_thesis: (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),(i + 1))) = {((f ^ g) /. (i + 1))} 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 (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),(i + 1))) = {((f ^ g) /. (i + 1))} by A5, A15, A17, A18, FINSEQ_4:69; ::_thesis: verum end; suppose i <> len f ; ::_thesis: (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),(i + 1))) = {((f ^ g) /. (i + 1))} 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 (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),(i + 1))) = {((f ^ g) /. (i + 1))} by A4, A20, A21, A22, FINSEQ_4:68; ::_thesis: verum end; end; end; hence (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),(i + 1))) = {((f ^ g) /. (i + 1))} ; ::_thesis: verum end; supposeA23: i > len f ; ::_thesis: (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),(i + 1))) = {((f ^ g) /. (i + 1))} 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 ; ::_thesis: verum end; end; end; hence (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),(i + 1))) = {((f ^ g) /. (i + 1))} ; ::_thesis: verum end; end; end; theorem Th32: :: SPPOL_2:32 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) for n being Element of NAT st f is unfolded & p in LSeg (f,n) holds Ins (f,n,p) is unfolded proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) for n being Element of NAT st f is unfolded & p in LSeg (f,n) holds Ins (f,n,p) is unfolded let p be Point of (TOP-REAL 2); ::_thesis: for n being Element of NAT st f is unfolded & p in LSeg (f,n) holds Ins (f,n,p) is unfolded let n be Element of NAT ; ::_thesis: ( f is unfolded & p in LSeg (f,n) implies Ins (f,n,p) is unfolded ) assume that A1: f is unfolded and A2: p in LSeg (f,n) ; ::_thesis: Ins (f,n,p) is unfolded set f1 = f | n; set g1 = (f | n) ^ <*p*>; set f2 = f /^ n; A3: n + 1 <= len f by A2, TOPREAL1:def_3; A4: n <= n + 1 by NAT_1:11; then A5: len (f | n) = n by A3, FINSEQ_1:59, XXREAL_0:2; then A6: n + 1 = len ((f | n) ^ <*p*>) 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 (f /^ n) by A7, RFINSEQ:def_1; then 1 in dom (f /^ n) by FINSEQ_3:25; then A9: f /. (n + 1) = (f /^ n) /. 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 (f | n) by A10, A5, FINSEQ_3:25; then A13: f /. n = (f | n) /. (len (f | n)) by A5, FINSEQ_4:70; A14: ((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>)) = ((f | n) ^ <*p*>) /. ((len (f | n)) + 1) by FINSEQ_2:16 .= p by FINSEQ_4:67 ; then A15: (LSeg (((f | n) /. (len (f | n))),p)) \/ (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))) = LSeg (((f | n) /. (len (f | n))),((f /^ n) /. 1)) by A2, A11, A13, A9, TOPREAL1:5; A16: now__::_thesis:_(f_|_n)_^_<*p*>_is_unfolded len (f | n) <> 0 by A2, A5, TOPREAL1:def_3; then consider k being Nat such that A17: k + 1 = len (f | n) by NAT_1:6; reconsider k = k as Element of NAT by ORDINAL1:def_12; A18: k + (1 + 1) <= len f by A3, A5, A17; percases ( k <> 0 or k = 0 ) ; suppose k <> 0 ; ::_thesis: (f | n) ^ <*p*> is unfolded then A19: 1 <= k by NAT_1:14; LSeg ((f | n),k) = LSeg (f,k) by A17, Th3; then A20: (LSeg ((f | n),k)) /\ (LSeg (f,n)) = {(f /. n)} by A1, A5, A17, A18, A19, TOPREAL1:def_6; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_(LSeg_((f_|_n),k))_/\_(LSeg_(((f_|_n)_/._(len_(f_|_n))),p))_implies_x_=_f_/._n_)_&_(_x_=_f_/._n_implies_x_in_(LSeg_((f_|_n),k))_/\_(LSeg_(((f_|_n)_/._(len_(f_|_n))),p))_)_) let x be set ; ::_thesis: ( ( x in (LSeg ((f | n),k)) /\ (LSeg (((f | n) /. (len (f | n))),p)) implies x = f /. n ) & ( x = f /. n implies x in (LSeg ((f | n),k)) /\ (LSeg (((f | n) /. (len (f | n))),p)) ) ) hereby ::_thesis: ( x = f /. n implies x in (LSeg ((f | n),k)) /\ (LSeg (((f | n) /. (len (f | n))),p)) ) assume A21: x in (LSeg ((f | n),k)) /\ (LSeg (((f | n) /. (len (f | n))),p)) ; ::_thesis: x = f /. n then x in LSeg (((f | n) /. (len (f | n))),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 ((f | n),k) by A21, XBOOLE_0:def_4; then x in (LSeg ((f | n),k)) /\ (LSeg (f,n)) by A22, XBOOLE_0:def_4; hence x = f /. n by A20, TARSKI:def_1; ::_thesis: verum end; assume A23: x = f /. n ; ::_thesis: x in (LSeg ((f | n),k)) /\ (LSeg (((f | n) /. (len (f | n))),p)) then x in (LSeg ((f | n),k)) /\ (LSeg (f,n)) by A20, TARSKI:def_1; then A24: x in LSeg ((f | n),k) by XBOOLE_0:def_4; x in LSeg (((f | n) /. (len (f | n))),p) by A13, A23, RLTOPSP1:68; hence x in (LSeg ((f | n),k)) /\ (LSeg (((f | n) /. (len (f | n))),p)) by A24, XBOOLE_0:def_4; ::_thesis: verum end; then (LSeg ((f | n),k)) /\ (LSeg (((f | n) /. (len (f | n))),p)) = {((f | n) /. (len (f | n)))} by A13, TARSKI:def_1; hence (f | n) ^ <*p*> is unfolded by A1, A17, Th30; ::_thesis: verum end; suppose k = 0 ; ::_thesis: (f | n) ^ <*p*> is unfolded then len ((f | n) ^ <*p*>) = 1 + 1 by A17, FINSEQ_2:16; hence (f | n) ^ <*p*> is unfolded by Th26; ::_thesis: verum end; end; end; (f | n) /. (len (f | n)) = ((f | n) ^ <*p*>) /. n by A5, A12, FINSEQ_4:68; then LSeg (((f | n) ^ <*p*>),n) = LSeg (((f | n) /. (len (f | n))),(((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>)))) by A10, A6, TOPREAL1:def_3; then A25: (LSeg (((f | n) ^ <*p*>),n)) /\ (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))) = {(((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>)))} by A2, A14, A11, A13, A9, TOPREAL1:8; now__::_thesis:_((f_|_n)_^_<*p*>)_^_(f_/^_n)_is_unfolded percases ( len (f /^ n) = 1 or len (f /^ n) <> 1 ) ; suppose len (f /^ n) = 1 ; ::_thesis: ((f | n) ^ <*p*>) ^ (f /^ n) is unfolded then f /^ n = <*((f /^ n) /. 1)*> by FINSEQ_5:14; hence ((f | n) ^ <*p*>) ^ (f /^ n) is unfolded by A16, A6, A25, Th30; ::_thesis: verum end; suppose len (f /^ n) <> 1 ; ::_thesis: ((f | n) ^ <*p*>) ^ (f /^ n) is unfolded then len (f /^ n) > 1 by A8, XXREAL_0:1; then A26: 1 + 1 <= len (f /^ n) by NAT_1:13; then LSeg ((f /^ n),1) = LSeg (((f /^ n) /. 1),((f /^ n) /. (1 + 1))) by TOPREAL1:def_3; then A27: (f /^ n) /. 1 in LSeg ((f /^ n),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 ((f /^ n),1)) by A28, Th5 ; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_(LSeg_((((f_|_n)_^_<*p*>)_/._(len_((f_|_n)_^_<*p*>))),((f_/^_n)_/._1)))_/\_(LSeg_((f_/^_n),1))_implies_x_=_(f_/^_n)_/._1_)_&_(_x_=_(f_/^_n)_/._1_implies_x_in_(LSeg_((((f_|_n)_^_<*p*>)_/._(len_((f_|_n)_^_<*p*>))),((f_/^_n)_/._1)))_/\_(LSeg_((f_/^_n),1))_)_) let x be set ; ::_thesis: ( ( x in (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))) /\ (LSeg ((f /^ n),1)) implies x = (f /^ n) /. 1 ) & ( x = (f /^ n) /. 1 implies x in (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))) /\ (LSeg ((f /^ n),1)) ) ) hereby ::_thesis: ( x = (f /^ n) /. 1 implies x in (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))) /\ (LSeg ((f /^ n),1)) ) assume A30: x in (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))) /\ (LSeg ((f /^ n),1)) ; ::_thesis: x = (f /^ n) /. 1 then x in LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 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 ((f /^ n),1) by A30, XBOOLE_0:def_4; then x in (LSeg (f,n)) /\ (LSeg ((f /^ n),1)) by A31, XBOOLE_0:def_4; hence x = (f /^ n) /. 1 by A9, A29, TARSKI:def_1; ::_thesis: verum end; assume A32: x = (f /^ n) /. 1 ; ::_thesis: x in (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))) /\ (LSeg ((f /^ n),1)) then x in LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1)) by RLTOPSP1:68; hence x in (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))) /\ (LSeg ((f /^ n),1)) by A27, A32, XBOOLE_0:def_4; ::_thesis: verum end; then (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))) /\ (LSeg ((f /^ n),1)) = {((f /^ n) /. 1)} by TARSKI:def_1; hence ((f | n) ^ <*p*>) ^ (f /^ n) is unfolded by A1, A16, A6, A25, Th31; ::_thesis: verum end; end; end; hence Ins (f,n,p) is unfolded by FINSEQ_5:def_4; ::_thesis: verum end; theorem Th33: :: SPPOL_2:33 for f being FinSequence of (TOP-REAL 2) st len f <= 2 holds f is s.n.c. proof let f be FinSequence of (TOP-REAL 2); ::_thesis: ( len f <= 2 implies f is s.n.c. ) assume A1: len f <= 2 ; ::_thesis: f is s.n.c. let i, j be Nat; :: according to TOPREAL1:def_7 ::_thesis: ( j <= i + 1 or LSeg (f,i) misses LSeg (f,j) ) assume A2: i + 1 < j ; ::_thesis: LSeg (f,i) misses LSeg (f,j) now__::_thesis:_(_1_<=_i_&_i_+_1_<=_len_f_&_1_<=_j_implies_not_j_+_1_<=_len_f_) assume that A3: 1 <= i and A4: i + 1 <= len f and A5: 1 <= j and A6: j + 1 <= len f ; ::_thesis: contradiction 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; ::_thesis: verum end; then ( LSeg (f,i) = {} or LSeg (f,j) = {} ) by TOPREAL1:def_3; hence (LSeg (f,i)) /\ (LSeg (f,j)) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: verum end; Lm6: for p, q being Point of (TOP-REAL 2) holds <*p,q*> is s.n.c. proof let p, q be Point of (TOP-REAL 2); ::_thesis: <*p,q*> is s.n.c. len <*p,q*> = 2 by FINSEQ_1:44; hence <*p,q*> is s.n.c. by Th33; ::_thesis: verum end; Lm7: for f being FinSequence of (TOP-REAL 2) for n being Element of NAT st f is s.n.c. holds f | n is s.n.c. proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for n being Element of NAT st f is s.n.c. holds f | n is s.n.c. let n be Element of NAT ; ::_thesis: ( f is s.n.c. implies f | n is s.n.c. ) assume A1: f is s.n.c. ; ::_thesis: f | n is s.n.c. let i, j be Nat; :: according to TOPREAL1:def_7 ::_thesis: ( j <= i + 1 or LSeg ((f | n),i) misses LSeg ((f | n),j) ) assume A2: i + 1 < j ; ::_thesis: LSeg ((f | n),i) misses LSeg ((f | n),j) percases ( i = 0 or j + 1 > len (f | n) or ( i <> 0 & j + 1 <= len (f | n) ) ) ; supposeA3: ( i = 0 or j + 1 > len (f | n) ) ; ::_thesis: LSeg ((f | n),i) misses LSeg ((f | n),j) now__::_thesis:_(_(_i_=_0_&_LSeg_((f_|_n),i)_=_{}_)_or_(_j_+_1_>_len_(f_|_n)_&_LSeg_((f_|_n),j)_=_{}_)_) percases ( i = 0 or j + 1 > len (f | n) ) by A3; case i = 0 ; ::_thesis: LSeg ((f | n),i) = {} hence LSeg ((f | n),i) = {} by TOPREAL1:def_3; ::_thesis: verum end; case j + 1 > len (f | n) ; ::_thesis: LSeg ((f | n),j) = {} hence LSeg ((f | n),j) = {} by TOPREAL1:def_3; ::_thesis: verum end; end; end; then (LSeg ((f | n),i)) /\ (LSeg ((f | n),j)) = {} ; hence LSeg ((f | n),i) misses LSeg ((f | n),j) by XBOOLE_0:def_7; ::_thesis: verum end; supposethat i <> 0 and A4: j + 1 <= len (f | n) ; ::_thesis: LSeg ((f | n),i) misses LSeg ((f | n),j) 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 LSeg ((f | n),i) misses LSeg ((f | n),j) by XBOOLE_0:def_7; ::_thesis: verum end; end; end; Lm8: for f being FinSequence of (TOP-REAL 2) for n being Element of NAT st f is s.n.c. holds f /^ n is s.n.c. proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for n being Element of NAT st f is s.n.c. holds f /^ n is s.n.c. let n be Element of NAT ; ::_thesis: ( f is s.n.c. implies f /^ n is s.n.c. ) assume A1: f is s.n.c. ; ::_thesis: f /^ n is s.n.c. percases ( n <= len f or n > len f ) ; supposeA2: n <= len f ; ::_thesis: f /^ n is s.n.c. let i, j be Nat; :: according to TOPREAL1:def_7 ::_thesis: ( j <= i + 1 or LSeg ((f /^ n),i) misses LSeg ((f /^ n),j) ) assume A3: i + 1 < j ; ::_thesis: LSeg ((f /^ n),i) misses LSeg ((f /^ n),j) now__::_thesis:_LSeg_((f_/^_n),i)_misses_LSeg_((f_/^_n),j) percases ( i = 0 or j + 1 > len (f /^ n) or ( i <> 0 & j + 1 <= len (f /^ n) ) ) ; supposeA4: ( i = 0 or j + 1 > len (f /^ n) ) ; ::_thesis: LSeg ((f /^ n),i) misses LSeg ((f /^ n),j) now__::_thesis:_(_(_i_=_0_&_LSeg_((f_/^_n),i)_=_{}_)_or_(_j_+_1_>_len_(f_/^_n)_&_LSeg_((f_/^_n),j)_=_{}_)_) percases ( i = 0 or j + 1 > len (f /^ n) ) by A4; case i = 0 ; ::_thesis: LSeg ((f /^ n),i) = {} hence LSeg ((f /^ n),i) = {} by TOPREAL1:def_3; ::_thesis: verum end; case j + 1 > len (f /^ n) ; ::_thesis: LSeg ((f /^ n),j) = {} hence LSeg ((f /^ n),j) = {} by TOPREAL1:def_3; ::_thesis: verum end; end; end; then (LSeg ((f /^ n),i)) /\ (LSeg ((f /^ n),j)) = {} ; hence LSeg ((f /^ n),i) misses LSeg ((f /^ n),j) by XBOOLE_0:def_7; ::_thesis: verum end; supposethat A5: i <> 0 and A6: j + 1 <= len (f /^ n) ; ::_thesis: LSeg ((f /^ n),i) misses LSeg ((f /^ n),j) 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 LSeg ((f /^ n),i) misses LSeg ((f /^ n),j) by XBOOLE_0:def_7; ::_thesis: verum end; end; end; hence LSeg ((f /^ n),i) misses LSeg ((f /^ n),j) ; ::_thesis: verum end; suppose n > len f ; ::_thesis: f /^ n is s.n.c. then f /^ n = <*> the carrier of (TOP-REAL 2) by RFINSEQ:def_1; then len (f /^ n) = 0 ; hence f /^ n is s.n.c. by Th33; ::_thesis: verum end; end; end; registration let f be s.n.c. FinSequence of (TOP-REAL 2); let n be Element of NAT ; clusterf | n -> s.n.c. for FinSequence of (TOP-REAL 2); coherence for b1 being FinSequence of (TOP-REAL 2) st b1 = f | n holds b1 is s.n.c. by Lm7; clusterf /^ n -> s.n.c. for FinSequence of (TOP-REAL 2); coherence for b1 being FinSequence of (TOP-REAL 2) st b1 = f /^ n holds b1 is s.n.c. by Lm8; end; Lm9: for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st f is s.n.c. holds f -: p is s.n.c. proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st f is s.n.c. holds f -: p is s.n.c. let p be Point of (TOP-REAL 2); ::_thesis: ( f is s.n.c. implies f -: p is s.n.c. ) f -: p = f | (p .. f) by FINSEQ_5:def_1; hence ( f is s.n.c. implies f -: p is s.n.c. ) ; ::_thesis: verum end; registration let f be s.n.c. FinSequence of (TOP-REAL 2); let p be Point of (TOP-REAL 2); clusterf -: p -> s.n.c. ; coherence f -: p is s.n.c. by Lm9; end; theorem Th34: :: SPPOL_2:34 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in rng f & f is s.n.c. holds f :- p is s.n.c. proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st p in rng f & f is s.n.c. holds f :- p is s.n.c. let p be Point of (TOP-REAL 2); ::_thesis: ( p in rng f & f is s.n.c. implies f :- p is s.n.c. ) assume p in rng f ; ::_thesis: ( not f is s.n.c. or f :- p is s.n.c. ) then ex i being Element of NAT st ( i + 1 = p .. f & f :- p = f /^ i ) by FINSEQ_5:49; hence ( not f is s.n.c. or f :- p is s.n.c. ) ; ::_thesis: verum end; theorem Th35: :: SPPOL_2:35 for f being FinSequence of (TOP-REAL 2) st f is s.n.c. holds Rev f is s.n.c. proof let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is s.n.c. implies Rev f is s.n.c. ) assume A1: f is s.n.c. ; ::_thesis: Rev f is s.n.c. let i, j be Nat; :: according to TOPREAL1:def_7 ::_thesis: ( j <= i + 1 or LSeg ((Rev f),i) misses LSeg ((Rev f),j) ) assume A2: i + 1 < j ; ::_thesis: LSeg ((Rev f),i) misses LSeg ((Rev f),j) percases ( i = 0 or j + 1 > len (Rev f) or ( i <> 0 & j + 1 <= len (Rev f) ) ) ; supposeA3: ( i = 0 or j + 1 > len (Rev f) ) ; ::_thesis: LSeg ((Rev f),i) misses LSeg ((Rev f),j) now__::_thesis:_(_(_i_=_0_&_LSeg_((Rev_f),i)_=_{}_)_or_(_j_+_1_>_len_(Rev_f)_&_LSeg_((Rev_f),j)_=_{}_)_) percases ( i = 0 or j + 1 > len (Rev f) ) by A3; case i = 0 ; ::_thesis: LSeg ((Rev f),i) = {} hence LSeg ((Rev f),i) = {} by TOPREAL1:def_3; ::_thesis: verum end; case j + 1 > len (Rev f) ; ::_thesis: LSeg ((Rev f),j) = {} hence LSeg ((Rev f),j) = {} by TOPREAL1:def_3; ::_thesis: verum end; end; end; then (LSeg ((Rev f),i)) /\ (LSeg ((Rev f),j)) = {} ; hence LSeg ((Rev f),i) misses LSeg ((Rev f),j) by XBOOLE_0:def_7; ::_thesis: verum end; supposethat i <> 0 and A4: j + 1 <= len (Rev f) ; ::_thesis: LSeg ((Rev f),i) misses LSeg ((Rev f),j) 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 ; :: according to XBOOLE_0:def_7 ::_thesis: verum end; end; end; theorem Th36: :: SPPOL_2:36 for f, g being FinSequence of (TOP-REAL 2) st f is s.n.c. & g is s.n.c. & L~ f misses L~ g & ( for i being Element of NAT st 1 <= i & i + 2 <= len f holds LSeg (f,i) misses LSeg ((f /. (len f)),(g /. 1)) ) & ( for i being Element of NAT st 2 <= i & i + 1 <= len g holds LSeg (g,i) misses LSeg ((f /. (len f)),(g /. 1)) ) holds f ^ g is s.n.c. proof let f, g be FinSequence of (TOP-REAL 2); ::_thesis: ( f is s.n.c. & g is s.n.c. & L~ f misses L~ g & ( for i being Element of NAT st 1 <= i & i + 2 <= len f holds LSeg (f,i) misses LSeg ((f /. (len f)),(g /. 1)) ) & ( for i being Element of NAT 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. ) 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 being Element of NAT st 1 <= i & i + 2 <= len f holds LSeg (f,i) misses LSeg ((f /. (len f)),(g /. 1)) and A5: for i being Element of NAT st 2 <= i & i + 1 <= len g holds LSeg (g,i) misses LSeg ((f /. (len f)),(g /. 1)) ; :: according to XBOOLE_0:def_7 ::_thesis: f ^ g is s.n.c. let i, j be Nat; :: according to TOPREAL1:def_7 ::_thesis: ( j <= i + 1 or LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) ) assume A6: i + 1 < j ; ::_thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) percases ( i = 0 or j + 1 > len (f ^ g) or ( i <> 0 & j + 1 <= len (f ^ g) ) ) ; supposeA7: ( i = 0 or j + 1 > len (f ^ g) ) ; ::_thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) now__::_thesis:_(_(_i_=_0_&_LSeg_((f_^_g),i)_=_{}_)_or_(_j_+_1_>_len_(f_^_g)_&_LSeg_((f_^_g),j)_=_{}_)_) percases ( i = 0 or j + 1 > len (f ^ g) ) by A7; case i = 0 ; ::_thesis: LSeg ((f ^ g),i) = {} hence LSeg ((f ^ g),i) = {} by TOPREAL1:def_3; ::_thesis: verum end; case j + 1 > len (f ^ g) ; ::_thesis: LSeg ((f ^ g),j) = {} hence LSeg ((f ^ g),j) = {} by TOPREAL1:def_3; ::_thesis: verum end; end; end; then (LSeg ((f ^ g),i)) /\ (LSeg ((f ^ g),j)) = {} ; hence LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) by XBOOLE_0:def_7; ::_thesis: verum end; supposethat A8: i <> 0 and A9: j + 1 <= len (f ^ g) ; ::_thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) 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__::_thesis:_LSeg_((f_^_g),i)_misses_LSeg_((f_^_g),j) percases ( j + 1 <= len f or j + 1 > len f ) ; supposeA13: j + 1 <= len f ; ::_thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) 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 LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) by A1, A6, A14, TOPREAL1:def_7; ::_thesis: verum end; suppose j + 1 > len f ; ::_thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) 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__::_thesis:_LSeg_((f_^_g),i)_misses_LSeg_((f_^_g),j) percases ( i <= len f or i > len f ) ; supposeA18: i <= len f ; ::_thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) then A19: not f is empty by A12; now__::_thesis:_LSeg_((f_^_g),i)_misses_LSeg_((f_^_g),j) percases ( i = len f or i <> len f ) ; supposeA20: i = len f ; ::_thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) not g is 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 LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) by A5, A16, A22, A21; ::_thesis: verum end; suppose i <> len f ; ::_thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) 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__::_thesis:_LSeg_((f_^_g),i)_misses_LSeg_((f_^_g),j) percases ( j = len f or j <> len f ) ; supposeA24: j = len f ; ::_thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) then (i + 1) + 1 <= len f by A6, NAT_1:13; then A25: i + (1 + 1) <= len f ; not g is 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 LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) by A4, A8, A23, A25, A26, NAT_1:14; ::_thesis: verum end; suppose j <> len f ; ::_thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) 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, XBOOLE_1:27; hence LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) by XBOOLE_0:def_7; ::_thesis: verum end; end; end; hence LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) ; ::_thesis: verum end; end; end; hence LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) ; ::_thesis: verum end; supposeA28: i > len f ; ::_thesis: LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) 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 LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) by A2, A30, A29, TOPREAL1:def_7; ::_thesis: verum end; end; end; hence LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) ; ::_thesis: verum end; end; end; hence LSeg ((f ^ g),i) misses LSeg ((f ^ g),j) ; ::_thesis: verum end; end; end; theorem Th37: :: SPPOL_2:37 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) for n being Element of NAT st f is unfolded & f is s.n.c. & p in LSeg (f,n) & not p in rng f holds Ins (f,n,p) is s.n.c. proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) for n being Element of NAT st f is unfolded & f is s.n.c. & p in LSeg (f,n) & not p in rng f holds Ins (f,n,p) is s.n.c. let p be Point of (TOP-REAL 2); ::_thesis: for n being Element of NAT st f is unfolded & f is s.n.c. & p in LSeg (f,n) & not p in rng f holds Ins (f,n,p) is s.n.c. let n be Element of NAT ; ::_thesis: ( f is unfolded & f is s.n.c. & p in LSeg (f,n) & not p in rng f implies Ins (f,n,p) is s.n.c. ) 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 ; ::_thesis: Ins (f,n,p) is s.n.c. set fp = Ins (f,n,p); let i, j be Nat; :: according to TOPREAL1:def_7 ::_thesis: ( j <= i + 1 or LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) ) assume A5: i + 1 < j ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) percases ( i = 0 or j + 1 > len (Ins (f,n,p)) or ( i <> 0 & j + 1 <= len (Ins (f,n,p)) ) ) ; supposeA6: ( i = 0 or j + 1 > len (Ins (f,n,p)) ) ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) now__::_thesis:_(_(_i_=_0_&_LSeg_((Ins_(f,n,p)),i)_=_{}_)_or_(_j_+_1_>_len_(Ins_(f,n,p))_&_LSeg_((Ins_(f,n,p)),j)_=_{}_)_) percases ( i = 0 or j + 1 > len (Ins (f,n,p)) ) by A6; case i = 0 ; ::_thesis: LSeg ((Ins (f,n,p)),i) = {} hence LSeg ((Ins (f,n,p)),i) = {} by TOPREAL1:def_3; ::_thesis: verum end; case j + 1 > len (Ins (f,n,p)) ; ::_thesis: LSeg ((Ins (f,n,p)),j) = {} hence LSeg ((Ins (f,n,p)),j) = {} by TOPREAL1:def_3; ::_thesis: verum end; end; end; then (LSeg ((Ins (f,n,p)),i)) /\ (LSeg ((Ins (f,n,p)),j)) = {} ; hence LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) by XBOOLE_0:def_7; ::_thesis: verum end; supposethat A7: i <> 0 and A8: j + 1 <= len (Ins (f,n,p)) ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) A9: 1 <= i by A7, NAT_1:14; set f1 = f | n; set g1 = (f | n) ^ <*p*>; set f2 = f /^ n; A10: Ins (f,n,p) = ((f | n) ^ <*p*>) ^ (f /^ n) 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 (Ins (f,n,p)) = (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 ((f | n) ^ <*p*>) = (len (f | n)) + 1 by FINSEQ_2:16; then A17: ((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>)) = 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 (f | n) = 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__::_thesis:_LSeg_((Ins_(f,n,p)),i)_misses_LSeg_((Ins_(f,n,p)),j) percases ( j + 1 <= n or j + 1 > n ) ; supposeA23: j + 1 <= n ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) then A24: LSeg ((Ins (f,n,p)),j) = LSeg (((f | n) ^ <*p*>),j) by A10, A16, A18, A20, Th6, XXREAL_0:2 .= LSeg ((f | n),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 ((Ins (f,n,p)),i) = LSeg (((f | n) ^ <*p*>),i) by A10, A16, A18, A20, Th6, XXREAL_0:2 .= LSeg ((f | n),i) by A20, A25, Th6 .= LSeg (f,i) by A20, A25, Th3 ; hence LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) by A2, A5, A24, TOPREAL1:def_7; ::_thesis: verum end; suppose j + 1 > n ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) then A26: n <= j by NAT_1:13; now__::_thesis:_LSeg_((Ins_(f,n,p)),i)_misses_LSeg_((Ins_(f,n,p)),j) percases ( i <= n + 1 or i > n + 1 ) ; supposeA27: i <= n + 1 ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) A28: 1 <= n + 1 by NAT_1:11; 1 <= (len f) - n by A15, XREAL_1:19; then 1 <= len (f /^ n) by A19, RFINSEQ:def_1; then 1 in dom (f /^ n) by FINSEQ_3:25; then A29: f /. (n + 1) = (f /^ n) /. 1 by FINSEQ_5:27; len ((f | n) ^ <*p*>) in dom ((f | n) ^ <*p*>) by FINSEQ_5:6; then A30: (Ins (f,n,p)) /. (n + 1) = ((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>)) by A10, A16, A20, FINSEQ_4:68; A31: (Ins (f,n,p)) /. ((n + 1) + 1) = f /. (n + 1) by A15, FINSEQ_5:74; A32: n in dom (f | n) by A14, A20, FINSEQ_3:25; then A33: f /. n = (f | n) /. (len (f | n)) by A20, FINSEQ_4:70; (n + 1) + 1 <= len (Ins (f,n,p)) by A13, A15, XREAL_1:6; then A34: LSeg ((Ins (f,n,p)),(n + 1)) = LSeg (p,((f /^ n) /. 1)) by A17, A29, A31, A28, A30, TOPREAL1:def_3; A35: (f | n) /. (len (f | n)) = ((f | n) ^ <*p*>) /. (len (f | n)) by A20, A32, FINSEQ_4:68; A36: LSeg ((Ins (f,n,p)),n) = LSeg (((f | n) ^ <*p*>),n) by A10, A16, A20, Th6 .= LSeg (((f | n) /. (len (f | n))),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 (((f | n) /. (len (f | n))),p)) \/ (LSeg ((((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))),((f /^ n) /. 1))) = LSeg (((f | n) /. (len (f | n))),((f /^ n) /. 1)) by A3, A17, A33, A29, TOPREAL1:5; A39: (LSeg (((f | n) /. (len (f | n))),p)) /\ (LSeg (p,((f /^ n) /. 1))) = {p} by A3, A37, A33, A29, TOPREAL1:8; now__::_thesis:_LSeg_((Ins_(f,n,p)),i)_misses_LSeg_((Ins_(f,n,p)),j) percases ( i < n or i = n or i > n ) by XXREAL_0:1; suppose i < n ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) then A40: i + 1 <= n by NAT_1:13; then A41: LSeg ((Ins (f,n,p)),i) = LSeg (((f | n) ^ <*p*>),i) by A10, A16, A18, A20, Th6, XXREAL_0:2 .= LSeg ((f | n),i) by A20, A40, Th6 .= LSeg (f,i) by A20, A40, Th3 ; now__::_thesis:_LSeg_((Ins_(f,n,p)),i)_misses_LSeg_((Ins_(f,n,p)),j) percases ( j = n or j <> n ) ; supposeA42: j = n ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) then A43: LSeg (f,i) misses LSeg (f,n) by A2, A5, TOPREAL1:def_7; (LSeg ((Ins (f,n,p)),i)) /\ (LSeg ((Ins (f,n,p)),j)) c= (LSeg (f,i)) /\ (LSeg (f,n)) by A37, A33, A29, A38, A36, A41, A42, XBOOLE_1:7, XBOOLE_1:26; then (LSeg ((Ins (f,n,p)),i)) /\ (LSeg ((Ins (f,n,p)),j)) c= {} by A43, XBOOLE_0:def_7; then (LSeg ((Ins (f,n,p)),i)) /\ (LSeg ((Ins (f,n,p)),j)) = {} by XBOOLE_1:3; hence LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) by XBOOLE_0:def_7; ::_thesis: verum end; suppose j <> n ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) then n < j by A26, XXREAL_0:1; then A44: n + 1 <= j by NAT_1:13; now__::_thesis:_LSeg_((Ins_(f,n,p)),i)_misses_LSeg_((Ins_(f,n,p)),j) percases ( j = n + 1 or j <> n + 1 ) ; supposeA45: j = n + 1 ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) now__::_thesis:_LSeg_((Ins_(f,n,p)),i)_misses_LSeg_((Ins_(f,n,p)),j) percases ( i + 1 = n or i + 1 <> n ) ; supposeA46: i + 1 = n ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) A47: i + (1 + 1) <= len f by A21, XREAL_1:6; LSeg ((Ins (f,n,p)),i) = LSeg (((f | n) ^ <*p*>),i) by A10, A16, A20, A46, Th6, NAT_1:11 .= LSeg ((f | n),i) by A20, A46, Th6 .= LSeg (f,i) by A20, A46, Th3 ; then A48: (LSeg ((Ins (f,n,p)),i)) /\ (LSeg (f,n)) = {(f /. n)} by A1, A9, A46, A47, TOPREAL1:def_6; assume not LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) ; ::_thesis: contradiction then consider x being set such that A49: x in (LSeg ((Ins (f,n,p)),i)) /\ (LSeg ((Ins (f,n,p)),j)) by XBOOLE_0:4; A50: x in LSeg ((Ins (f,n,p)),i) by A49, XBOOLE_0:def_4; A51: x in LSeg ((Ins (f,n,p)),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 ((Ins (f,n,p)),n) by A33, A36, RLTOPSP1:68; then x in (LSeg ((Ins (f,n,p)),n)) /\ (LSeg ((Ins (f,n,p)),(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; ::_thesis: verum end; suppose i + 1 <> n ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) then i + 1 < n by A40, XXREAL_0:1; then A54: LSeg (f,i) misses LSeg (f,n) by A2, TOPREAL1:def_7; (LSeg ((Ins (f,n,p)),i)) /\ (LSeg ((Ins (f,n,p)),j)) c= (LSeg (f,i)) /\ (LSeg (f,n)) by A17, A37, A33, A29, A38, A34, A41, A45, XBOOLE_1:7, XBOOLE_1:26; then (LSeg ((Ins (f,n,p)),i)) /\ (LSeg ((Ins (f,n,p)),j)) c= {} by A54, XBOOLE_0:def_7; then (LSeg ((Ins (f,n,p)),i)) /\ (LSeg ((Ins (f,n,p)),j)) = {} by XBOOLE_1:3; hence LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) by XBOOLE_0:def_7; ::_thesis: verum end; end; end; hence LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) ; ::_thesis: verum end; supposeA55: j <> n + 1 ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) 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 ((Ins (f,n,p)),j) = LSeg ((f /^ n),nj) by A10, A16, A20, A57, Th7 .= LSeg (f,j9) by A19, A57, A58, Th4 ; hence LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) by A2, A41, A59, TOPREAL1:def_7; ::_thesis: verum end; end; end; hence LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) ; ::_thesis: verum end; end; end; hence LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) ; ::_thesis: verum end; supposeA60: i = n ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) 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 ((Ins (f,n,p)),j) = LSeg ((f /^ n),nj) by A10, A16, A20, A62, Th7 .= LSeg (f,j9) by A19, A62, A63, Th4 ; now__::_thesis:_LSeg_((Ins_(f,n,p)),i)_misses_LSeg_((Ins_(f,n,p)),j) percases ( j <> (n + 1) + 1 or j = (n + 1) + 1 ) ; suppose j <> (n + 1) + 1 ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) 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 ((Ins (f,n,p)),i)) /\ (LSeg ((Ins (f,n,p)),j)) c= (LSeg (f,i)) /\ (LSeg (f,j9)) by A37, A33, A29, A38, A36, A60, A64, XBOOLE_1:7, XBOOLE_1:26; then (LSeg ((Ins (f,n,p)),i)) /\ (LSeg ((Ins (f,n,p)),j)) c= {} by A65, XBOOLE_0:def_7; then (LSeg ((Ins (f,n,p)),i)) /\ (LSeg ((Ins (f,n,p)),j)) = {} by XBOOLE_1:3; hence LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) by XBOOLE_0:def_7; ::_thesis: verum end; supposeA66: j = (n + 1) + 1 ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) 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 LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) ; ::_thesis: contradiction then consider x being set such that A68: x in (LSeg ((Ins (f,n,p)),i)) /\ (LSeg ((Ins (f,n,p)),j)) by XBOOLE_0:4; A69: x in LSeg ((Ins (f,n,p)),j) by A68, XBOOLE_0:def_4; A70: x in LSeg ((Ins (f,n,p)),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 ((Ins (f,n,p)),(n + 1)) by A29, A34, RLTOPSP1:68; then x in (LSeg ((Ins (f,n,p)),n)) /\ (LSeg ((Ins (f,n,p)),(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; ::_thesis: verum end; end; end; hence LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) ; ::_thesis: verum end; supposeA73: i > n ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) 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 ((Ins (f,n,p)),j) = LSeg ((f /^ n),nj) by A10, A16, A20, A76, Th7 .= LSeg (f,j9) by A19, A76, A77, Th4 ; then (LSeg ((Ins (f,n,p)),(n + 1))) /\ (LSeg ((Ins (f,n,p)),j)) c= (LSeg (f,n)) /\ (LSeg (f,j9)) by A17, A37, A33, A29, A38, A34, XBOOLE_1:7, XBOOLE_1:26; then (LSeg ((Ins (f,n,p)),(n + 1))) /\ (LSeg ((Ins (f,n,p)),j)) c= {} by A75, XBOOLE_0:def_7; then (LSeg ((Ins (f,n,p)),(n + 1))) /\ (LSeg ((Ins (f,n,p)),j)) = {} by XBOOLE_1:3; hence LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) by A74, XBOOLE_0:def_7; ::_thesis: verum end; end; end; hence LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) ; ::_thesis: verum end; supposeA78: i > n + 1 ; ::_thesis: LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) 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 ((Ins (f,n,p)),j) = LSeg ((f /^ n),nj) by A10, A16, A20, A79, Th7 .= LSeg (f,j9) by A19, A79, A84, Th4 ; i = ni + (n + 1) ; then LSeg ((Ins (f,n,p)),i) = LSeg ((f /^ n),ni) by A10, A16, A20, A80, Th7 .= LSeg (f,i9) by A80, A81, A82, Th5 ; hence LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) by A2, A83, A85, TOPREAL1:def_7; ::_thesis: verum end; end; end; hence LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) ; ::_thesis: verum end; end; end; hence LSeg ((Ins (f,n,p)),i) misses LSeg ((Ins (f,n,p)),j) ; ::_thesis: verum end; end; end; registration cluster <*> the carrier of (TOP-REAL 2) -> special ; coherence <*> the carrier of (TOP-REAL 2) is special proof set f = <*> the carrier of (TOP-REAL 2); let i be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( not 1 <= i or not i + 1 <= len (<*> the carrier of (TOP-REAL 2)) or ((<*> the carrier of (TOP-REAL 2)) /. i) `1 = ((<*> the carrier of (TOP-REAL 2)) /. (i + 1)) `1 or ((<*> the carrier of (TOP-REAL 2)) /. i) `2 = ((<*> the carrier of (TOP-REAL 2)) /. (i + 1)) `2 ) assume that 1 <= i and A1: i + 1 <= len (<*> the carrier of (TOP-REAL 2)) ; ::_thesis: ( ((<*> the carrier of (TOP-REAL 2)) /. i) `1 = ((<*> the carrier of (TOP-REAL 2)) /. (i + 1)) `1 or ((<*> the carrier of (TOP-REAL 2)) /. i) `2 = ((<*> the carrier of (TOP-REAL 2)) /. (i + 1)) `2 ) thus ( ((<*> the carrier of (TOP-REAL 2)) /. i) `1 = ((<*> the carrier of (TOP-REAL 2)) /. (i + 1)) `1 or ((<*> the carrier of (TOP-REAL 2)) /. i) `2 = ((<*> the carrier of (TOP-REAL 2)) /. (i + 1)) `2 ) by A1; ::_thesis: verum end; end; registration let p be Point of (TOP-REAL 2); cluster<*p*> -> special for FinSequence of (TOP-REAL 2); coherence for b1 being FinSequence of (TOP-REAL 2) st b1 = <*p*> holds b1 is special proof set f = <*p*>; <*p*> is special proof let i be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( not 1 <= i or not i + 1 <= len <*p*> or (<*p*> /. i) `1 = (<*p*> /. (i + 1)) `1 or (<*p*> /. i) `2 = (<*p*> /. (i + 1)) `2 ) assume that A1: 1 <= i and A2: i + 1 <= len <*p*> ; ::_thesis: ( (<*p*> /. i) `1 = (<*p*> /. (i + 1)) `1 or (<*p*> /. i) `2 = (<*p*> /. (i + 1)) `2 ) len <*p*> = 0 + 1 by FINSEQ_1:39; hence ( (<*p*> /. i) `1 = (<*p*> /. (i + 1)) `1 or (<*p*> /. i) `2 = (<*p*> /. (i + 1)) `2 ) by A1, A2, XREAL_1:6; ::_thesis: verum end; hence for b1 being FinSequence of (TOP-REAL 2) st b1 = <*p*> holds b1 is special ; ::_thesis: verum end; end; theorem Th38: :: SPPOL_2:38 for p, q being Point of (TOP-REAL 2) st ( p `1 = q `1 or p `2 = q `2 ) holds <*p,q*> is special proof let p, q be Point of (TOP-REAL 2); ::_thesis: ( ( p `1 = q `1 or p `2 = q `2 ) implies <*p,q*> is special ) assume A1: ( p `1 = q `1 or p `2 = q `2 ) ; ::_thesis: <*p,q*> is special set f = <*p,q*>; let i be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( not 1 <= i or not i + 1 <= len <*p,q*> or (<*p,q*> /. i) `1 = (<*p,q*> /. (i + 1)) `1 or (<*p,q*> /. i) `2 = (<*p,q*> /. (i + 1)) `2 ) assume that A2: 1 <= i and A3: i + 1 <= len <*p,q*> ; ::_thesis: ( (<*p,q*> /. i) `1 = (<*p,q*> /. (i + 1)) `1 or (<*p,q*> /. i) `2 = (<*p,q*> /. (i + 1)) `2 ) len <*p,q*> = 1 + 1 by FINSEQ_1:44; then i <= 1 by A3, XREAL_1:6; then A4: i = 1 by A2, XXREAL_0:1; then <*p,q*> /. i = p by FINSEQ_4:17; hence ( (<*p,q*> /. i) `1 = (<*p,q*> /. (i + 1)) `1 or (<*p,q*> /. i) `2 = (<*p,q*> /. (i + 1)) `2 ) by A1, A4, FINSEQ_4:17; ::_thesis: verum end; Lm10: for f being FinSequence of (TOP-REAL 2) for n being Element of NAT st f is special holds f | n is special proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for n being Element of NAT st f is special holds f | n is special let n be Element of NAT ; ::_thesis: ( f is special implies f | n is special ) assume A1: f is special ; ::_thesis: f | n is special let i be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( not 1 <= i or not i + 1 <= len (f | n) or ((f | n) /. i) `1 = ((f | n) /. (i + 1)) `1 or ((f | n) /. i) `2 = ((f | n) /. (i + 1)) `2 ) assume that A2: 1 <= i and A3: i + 1 <= len (f | n) ; ::_thesis: ( ((f | n) /. i) `1 = ((f | n) /. (i + 1)) `1 or ((f | n) /. i) `2 = ((f | n) /. (i + 1)) `2 ) 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 ( ((f | n) /. i) `1 = ((f | n) /. (i + 1)) `1 or ((f | n) /. i) `2 = ((f | n) /. (i + 1)) `2 ) by A1, A2, A4, A5, TOPREAL1:def_5; ::_thesis: verum end; Lm11: for f being FinSequence of (TOP-REAL 2) for n being Element of NAT st f is special holds f /^ n is special proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for n being Element of NAT st f is special holds f /^ n is special let n be Element of NAT ; ::_thesis: ( f is special implies f /^ n is special ) assume A1: f is special ; ::_thesis: f /^ n is special percases ( n <= len f or n > len f ) ; supposeA2: n <= len f ; ::_thesis: f /^ n is special let i be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( not 1 <= i or not i + 1 <= len (f /^ n) or ((f /^ n) /. i) `1 = ((f /^ n) /. (i + 1)) `1 or ((f /^ n) /. i) `2 = ((f /^ n) /. (i + 1)) `2 ) assume that A3: 1 <= i and A4: i + 1 <= len (f /^ n) ; ::_thesis: ( ((f /^ n) /. i) `1 = ((f /^ n) /. (i + 1)) `1 or ((f /^ n) /. i) `2 = ((f /^ n) /. (i + 1)) `2 ) 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 ( ((f /^ n) /. i) `1 = ((f /^ n) /. (i + 1)) `1 or ((f /^ n) /. i) `2 = ((f /^ n) /. (i + 1)) `2 ) by A1, A5, A7, A6, TOPREAL1:def_5; ::_thesis: verum end; suppose n > len f ; ::_thesis: f /^ n is special then f /^ n = <*> the carrier of (TOP-REAL 2) by RFINSEQ:def_1; hence f /^ n is special ; ::_thesis: verum end; end; end; registration let f be special FinSequence of (TOP-REAL 2); let n be Element of NAT ; clusterf | n -> special for FinSequence of (TOP-REAL 2); coherence for b1 being FinSequence of (TOP-REAL 2) st b1 = f | n holds b1 is special by Lm10; clusterf /^ n -> special for FinSequence of (TOP-REAL 2); coherence for b1 being FinSequence of (TOP-REAL 2) st b1 = f /^ n holds b1 is special by Lm11; end; theorem Th39: :: SPPOL_2:39 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in rng f & f is special holds f :- p is special proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st p in rng f & f is special holds f :- p is special let p be Point of (TOP-REAL 2); ::_thesis: ( p in rng f & f is special implies f :- p is special ) assume p in rng f ; ::_thesis: ( not f is special or f :- p is special ) then ex i being Element of NAT st ( i + 1 = p .. f & f :- p = f /^ i ) by FINSEQ_5:49; hence ( not f is special or f :- p is special ) ; ::_thesis: verum end; Lm12: for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st f is special holds f -: p is special proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st f is special holds f -: p is special let p be Point of (TOP-REAL 2); ::_thesis: ( f is special implies f -: p is special ) f -: p = f | (p .. f) by FINSEQ_5:def_1; hence ( f is special implies f -: p is special ) ; ::_thesis: verum end; registration let f be special FinSequence of (TOP-REAL 2); let p be Point of (TOP-REAL 2); clusterf -: p -> special ; coherence f -: p is special by Lm12; end; theorem Th40: :: SPPOL_2:40 for f being FinSequence of (TOP-REAL 2) st f is special holds Rev f is special proof let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is special implies Rev f is special ) assume A1: f is special ; ::_thesis: Rev f is special A2: len (Rev f) = len f by FINSEQ_5:def_3; let i be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( not 1 <= i or not i + 1 <= len (Rev f) or ((Rev f) /. i) `1 = ((Rev f) /. (i + 1)) `1 or ((Rev f) /. i) `2 = ((Rev f) /. (i + 1)) `2 ) assume that A3: 1 <= i and A4: i + 1 <= len (Rev f) ; ::_thesis: ( ((Rev f) /. i) `1 = ((Rev f) /. (i + 1)) `1 or ((Rev f) /. i) `2 = ((Rev f) /. (i + 1)) `2 ) 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 ( ((Rev f) /. i) `1 = ((Rev f) /. (i + 1)) `1 or ((Rev f) /. i) `2 = ((Rev f) /. (i + 1)) `2 ) by A1, A5, A7, A8, TOPREAL1:def_5; ::_thesis: verum end; Lm13: for f, g being FinSequence of (TOP-REAL 2) st f is special & g is special & ( (f /. (len f)) `1 = (g /. 1) `1 or (f /. (len f)) `2 = (g /. 1) `2 ) holds f ^ g is special proof let f, g be FinSequence of (TOP-REAL 2); ::_thesis: ( 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 ) 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 ) ; ::_thesis: f ^ g is special let i be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( not 1 <= i or not i + 1 <= len (f ^ g) or ((f ^ g) /. i) `1 = ((f ^ g) /. (i + 1)) `1 or ((f ^ g) /. i) `2 = ((f ^ g) /. (i + 1)) `2 ) assume that A4: 1 <= i and A5: i + 1 <= len (f ^ g) ; ::_thesis: ( ((f ^ g) /. i) `1 = ((f ^ g) /. (i + 1)) `1 or ((f ^ g) /. i) `2 = ((f ^ g) /. (i + 1)) `2 ) A6: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22; percases ( i < len f or i = len f or i > len f ) by XXREAL_0:1; suppose i < len f ; ::_thesis: ( ((f ^ g) /. i) `1 = ((f ^ g) /. (i + 1)) `1 or ((f ^ g) /. i) `2 = ((f ^ g) /. (i + 1)) `2 ) 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 ( ((f ^ g) /. i) `1 = ((f ^ g) /. (i + 1)) `1 or ((f ^ g) /. i) `2 = ((f ^ g) /. (i + 1)) `2 ) by A1, A4, A7, A8, TOPREAL1:def_5; ::_thesis: verum end; supposeA9: i = len f ; ::_thesis: ( ((f ^ g) /. i) `1 = ((f ^ g) /. (i + 1)) `1 or ((f ^ g) /. i) `2 = ((f ^ g) /. (i + 1)) `2 ) 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 ( ((f ^ g) /. i) `1 = ((f ^ g) /. (i + 1)) `1 or ((f ^ g) /. i) `2 = ((f ^ g) /. (i + 1)) `2 ) by A3, A9, A10, FINSEQ_4:69; ::_thesis: verum end; supposeA11: i > len f ; ::_thesis: ( ((f ^ g) /. i) `1 = ((f ^ g) /. (i + 1)) `1 or ((f ^ g) /. i) `2 = ((f ^ g) /. (i + 1)) `2 ) 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 ( ((f ^ g) /. i) `1 = ((f ^ g) /. (i + 1)) `1 or ((f ^ g) /. i) `2 = ((f ^ g) /. (i + 1)) `2 ) by A2, A12, A14, A15, TOPREAL1:def_5; ::_thesis: verum end; end; end; theorem Th41: :: SPPOL_2:41 for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) for n being Element of NAT st f is special & p in LSeg (f,n) holds Ins (f,n,p) is special proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) for n being Element of NAT st f is special & p in LSeg (f,n) holds Ins (f,n,p) is special let p be Point of (TOP-REAL 2); ::_thesis: for n being Element of NAT st f is special & p in LSeg (f,n) holds Ins (f,n,p) is special let n be Element of NAT ; ::_thesis: ( f is special & p in LSeg (f,n) implies Ins (f,n,p) is special ) assume that A1: f is special and A2: p in LSeg (f,n) ; ::_thesis: Ins (f,n,p) is special 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; set g1 = (f | n) ^ <*p*>; set f2 = f /^ n; set p1 = (f | n) /. (len (f | n)); set p2 = (f /^ n) /. 1; A7: (f | n) /. (len (f | n)) = |[(((f | n) /. (len (f | n))) `1),(((f | n) /. (len (f | n))) `2)]| by EUCLID:53; A8: n <= n + 1 by NAT_1:11; then n <= len f by A3, XXREAL_0:2; then 1 <= len (f /^ n) by A4, RFINSEQ:def_1; then 1 in dom (f /^ n) by FINSEQ_3:25; then A9: f /. (n + 1) = (f /^ n) /. 1 by FINSEQ_5:27; A10: len (f | n) = n by A3, A8, FINSEQ_1:59, XXREAL_0:2; then n in dom (f | n) by A5, FINSEQ_3:25; then A11: f /. n = (f | n) /. (len (f | n)) by A10, FINSEQ_4:70; then A12: ( ((f | n) /. (len (f | n))) `1 = ((f /^ n) /. 1) `1 or ((f | n) /. (len (f | n))) `2 = ((f /^ n) /. 1) `2 ) by A1, A5, A3, A9, TOPREAL1:def_5; set q1 = ((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>)); A13: (f /^ n) /. 1 = |[(((f /^ n) /. 1) `1),(((f /^ n) /. 1) `2)]| by EUCLID:53; <*p*> /. 1 = p by FINSEQ_4:16; then ( ((f | n) /. (len (f | n))) `1 = (<*p*> /. 1) `1 or ((f | n) /. (len (f | n))) `2 = (<*p*> /. 1) `2 ) by A2, A6, A11, A9, A12, A7, A13, TOPREAL3:11, TOPREAL3:12; then A14: (f | n) ^ <*p*> is special by A1, Lm13; ((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>)) = ((f | n) ^ <*p*>) /. ((len (f | n)) + 1) by FINSEQ_2:16 .= p by FINSEQ_4:67 ; then ( (((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))) `1 = ((f /^ n) /. 1) `1 or (((f | n) ^ <*p*>) /. (len ((f | n) ^ <*p*>))) `2 = ((f /^ n) /. 1) `2 ) by A2, A6, A11, A9, A12, A7, A13, TOPREAL3:11, TOPREAL3:12; then ((f | n) ^ <*p*>) ^ (f /^ n) is special by A1, A14, Lm13; hence Ins (f,n,p) is special by FINSEQ_5:def_4; ::_thesis: verum end; theorem Th42: :: SPPOL_2:42 for f being FinSequence of (TOP-REAL 2) for q being Point of (TOP-REAL 2) st q in rng f & 1 <> q .. f & q .. f <> len f & f is unfolded & f is s.n.c. holds (L~ (f -: q)) /\ (L~ (f :- q)) = {q} proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for q being Point of (TOP-REAL 2) st q in rng f & 1 <> q .. f & q .. f <> len f & f is unfolded & f is s.n.c. holds (L~ (f -: q)) /\ (L~ (f :- q)) = {q} let q be Point of (TOP-REAL 2); ::_thesis: ( q in rng f & 1 <> q .. f & q .. f <> len f & f is unfolded & f is s.n.c. implies (L~ (f -: q)) /\ (L~ (f :- q)) = {q} ) 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. ; ::_thesis: (L~ (f -: q)) /\ (L~ (f :- q)) = {q} 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; not f -: q is 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} :: according to XBOOLE_0:def_10 ::_thesis: {q} c= (L~ (f -: q)) /\ (L~ (f :- q)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (L~ (f -: q)) /\ (L~ (f :- q)) or x in {q} ) assume A12: x in (L~ (f -: q)) /\ (L~ (f :- q)) ; ::_thesis: x in {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 being Element of NAT 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 being Element of NAT 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 = j9 as Element of NAT by ORDINAL1:def_12; A20: LSeg ((f :- q),j) = LSeg (f,(j9 + (q .. f))) by A1, A19, Th10; percases ( ( i + 1 = len (f -: q) & j9 = 0 ) or ( i + 1 = len (f -: q) & j9 <> 0 ) or i + 1 <> len (f -: q) ) ; supposethat A21: i + 1 = len (f -: q) and A22: j9 = 0 ; ::_thesis: x in {q} 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 x in {q} by A15, A18, XBOOLE_0:def_4; ::_thesis: verum end; supposethat A23: i + 1 = len (f -: q) and A24: j9 <> 0 ; ::_thesis: x in {q} 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 x in {q} by A15, A18, XBOOLE_0:def_4; ::_thesis: verum end; supposeA25: i + 1 <> len (f -: q) ; ::_thesis: x in {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 x in {q} by A15, A18, XBOOLE_0:def_4; ::_thesis: verum end; 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 {q} c= (L~ (f -: q)) /\ (L~ (f :- q)) by ZFMISC_1:31; ::_thesis: verum end; theorem Th43: :: SPPOL_2:43 for p, q being Point of (TOP-REAL 2) st p <> q & ( p `1 = q `1 or p `2 = q `2 ) holds <*p,q*> is being_S-Seq proof let p, q be Point of (TOP-REAL 2); ::_thesis: ( p <> q & ( p `1 = q `1 or p `2 = q `2 ) implies <*p,q*> is being_S-Seq ) assume that A1: p <> q and A2: ( p `1 = q `1 or p `2 = q `2 ) ; ::_thesis: <*p,q*> is being_S-Seq set f = <*p,q*>; thus <*p,q*> is one-to-one by A1, FINSEQ_3:94; :: according to TOPREAL1:def_8 ::_thesis: ( 2 <= len <*p,q*> & <*p,q*> is unfolded & <*p,q*> is s.n.c. & <*p,q*> is special ) thus len <*p,q*> >= 2 by FINSEQ_1:44; ::_thesis: ( <*p,q*> is unfolded & <*p,q*> is s.n.c. & <*p,q*> is special ) thus ( <*p,q*> is unfolded & <*p,q*> is s.n.c. & <*p,q*> is special ) by A2, Lm2, Lm6, Th38; ::_thesis: verum 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 for b1 being FinSequence of (TOP-REAL 2) st b1 = Rev f holds b1 is being_S-Seq proof set g = Rev f; Rev f is being_S-Seq proof thus Rev f is one-to-one ; :: according to TOPREAL1:def_8 ::_thesis: ( 2 <= len (Rev f) & Rev f is unfolded & Rev f is s.n.c. & Rev f is special ) len (Rev f) = len f by FINSEQ_5:def_3; hence len (Rev f) >= 2 by TOPREAL1:def_8; ::_thesis: ( Rev f is unfolded & Rev f is s.n.c. & Rev f is special ) thus ( Rev f is unfolded & Rev f is s.n.c. & Rev f is special ) by Th28, Th35, Th40; ::_thesis: verum end; hence for b1 being FinSequence of (TOP-REAL 2) st b1 = Rev f holds b1 is being_S-Seq ; ::_thesis: verum end; end; theorem :: SPPOL_2:44 for i being Element of NAT for f being S-Sequence_in_R2 st i in dom f holds f /. i in L~ f proof let i be Element of NAT ; ::_thesis: for f being S-Sequence_in_R2 st i in dom f holds f /. i in L~ f let f be S-Sequence_in_R2; ::_thesis: ( i in dom f implies f /. i in L~ f ) len f >= 2 by TOPREAL1:def_8; hence ( i in dom f implies f /. i in L~ f ) by GOBOARD1:1; ::_thesis: verum end; theorem :: SPPOL_2:45 for p, q being Point of (TOP-REAL 2) st p <> q & ( p `1 = q `1 or p `2 = q `2 ) holds LSeg (p,q) is being_S-P_arc proof let p, q be Point of (TOP-REAL 2); ::_thesis: ( p <> q & ( p `1 = q `1 or p `2 = q `2 ) implies LSeg (p,q) is being_S-P_arc ) assume that A1: p <> q and A2: ( p `1 = q `1 or p `2 = q `2 ) ; ::_thesis: LSeg (p,q) is being_S-P_arc take f = <*p,q*>; :: according to TOPREAL1:def_9 ::_thesis: ( f is being_S-Seq & LSeg (p,q) = L~ f ) thus f is being_S-Seq by A1, A2, Th43; ::_thesis: LSeg (p,q) = L~ f thus LSeg (p,q) = L~ f by Th21; ::_thesis: verum end; Lm14: for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in rng f holds L~ (f -: p) c= L~ f proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st p in rng f holds L~ (f -: p) c= L~ f let p be Point of (TOP-REAL 2); ::_thesis: ( p in rng f implies L~ (f -: p) c= L~ f ) assume p in rng f ; ::_thesis: L~ (f -: p) c= L~ f then L~ f = (L~ (f -: p)) \/ (L~ (f :- p)) by Th24; hence L~ (f -: p) c= L~ f by XBOOLE_1:7; ::_thesis: verum end; Lm15: for f being FinSequence of (TOP-REAL 2) for p being Point of (TOP-REAL 2) st p in rng f holds L~ (f :- p) c= L~ f proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st p in rng f holds L~ (f :- p) c= L~ f let p be Point of (TOP-REAL 2); ::_thesis: ( p in rng f implies L~ (f :- p) c= L~ f ) assume p in rng f ; ::_thesis: L~ (f :- p) c= L~ f then L~ f = (L~ (f -: p)) \/ (L~ (f :- p)) by Th24; hence L~ (f :- p) c= L~ f by XBOOLE_1:7; ::_thesis: verum end; theorem Th46: :: SPPOL_2:46 for p being Point of (TOP-REAL 2) for f being S-Sequence_in_R2 st p in rng f & p .. f <> 1 holds f -: p is being_S-Seq proof let p be Point of (TOP-REAL 2); ::_thesis: for f being S-Sequence_in_R2 st p in rng f & p .. f <> 1 holds f -: p is being_S-Seq let f be S-Sequence_in_R2; ::_thesis: ( p in rng f & p .. f <> 1 implies f -: p is being_S-Seq ) assume that A1: p in rng f and A2: p .. f <> 1 ; ::_thesis: f -: p is being_S-Seq thus f -: p is one-to-one ; :: according to TOPREAL1:def_8 ::_thesis: ( 2 <= len (f -: p) & f -: p is unfolded & f -: p is s.n.c. & f -: p is special ) 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; ::_thesis: ( f -: p is unfolded & f -: p is s.n.c. & f -: p is special ) thus ( f -: p is unfolded & f -: p is s.n.c. & f -: p is special ) ; ::_thesis: verum end; theorem :: SPPOL_2:47 for p being Point of (TOP-REAL 2) 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 p be Point of (TOP-REAL 2); ::_thesis: for f being S-Sequence_in_R2 st p in rng f & p .. f <> len f holds f :- p is being_S-Seq let f be S-Sequence_in_R2; ::_thesis: ( p in rng f & p .. f <> len f implies f :- p is being_S-Seq ) assume that A1: p in rng f and A2: p .. f <> len f ; ::_thesis: f :- p is being_S-Seq thus f :- p is one-to-one by A1, FINSEQ_5:56; :: according to TOPREAL1:def_8 ::_thesis: ( 2 <= len (f :- p) & f :- p is unfolded & f :- p is s.n.c. & f :- p is special ) hereby ::_thesis: ( f :- p is unfolded & f :- p is s.n.c. & f :- p is special ) 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 ; ::_thesis: contradiction then ((len f) - (p .. f)) + 1 < 1 + 1 by A1, FINSEQ_5:50; hence contradiction by A3, XREAL_1:6; ::_thesis: verum end; thus ( f :- p is unfolded & f :- p is s.n.c. & f :- p is special ) by A1, Th27, Th34, Th39; ::_thesis: verum end; theorem Th48: :: SPPOL_2:48 for p being Point of (TOP-REAL 2) for i being Element of NAT 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 p be Point of (TOP-REAL 2); ::_thesis: for i being Element of NAT 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 let i be Element of NAT ; ::_thesis: 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 let f be S-Sequence_in_R2; ::_thesis: ( p in LSeg (f,i) & not p in rng f implies Ins (f,i,p) is being_S-Seq ) assume that A1: p in LSeg (f,i) and A2: not p in rng f ; ::_thesis: Ins (f,i,p) is being_S-Seq set g = Ins (f,i,p); thus Ins (f,i,p) is one-to-one by A2, FINSEQ_5:76; :: according to TOPREAL1:def_8 ::_thesis: ( 2 <= len (Ins (f,i,p)) & Ins (f,i,p) is unfolded & Ins (f,i,p) is s.n.c. & Ins (f,i,p) is special ) len (Ins (f,i,p)) = (len f) + 1 by FINSEQ_5:69; then A3: len (Ins (f,i,p)) >= len f by NAT_1:11; len f >= 2 by TOPREAL1:def_8; hence len (Ins (f,i,p)) >= 2 by A3, XXREAL_0:2; ::_thesis: ( Ins (f,i,p) is unfolded & Ins (f,i,p) is s.n.c. & Ins (f,i,p) is special ) thus Ins (f,i,p) is unfolded by A1, Th32; ::_thesis: ( Ins (f,i,p) is s.n.c. & Ins (f,i,p) is special ) thus Ins (f,i,p) is s.n.c. by A1, A2, Th37; ::_thesis: Ins (f,i,p) is special thus Ins (f,i,p) is special by A1, Th41; ::_thesis: verum end; begin registration cluster being_S-P_arc for Element of bool the carrier of (TOP-REAL 2); existence ex b1 being Subset of (TOP-REAL 2) st b1 is being_S-P_arc proof set p = |[0,0]|; set q = |[1,1]|; set f = <*|[0,0]|,|[(|[0,0]| `1),(|[1,1]| `2)]|,|[1,1]|*>; A1: |[0,0]| `2 = 0 by EUCLID:52; A2: |[1,1]| `1 = 1 by EUCLID:52; A3: |[1,1]| `2 = 1 by EUCLID:52; |[0,0]| `1 = 0 by EUCLID:52; then <*|[0,0]|,|[(|[0,0]| `1),(|[1,1]| `2)]|,|[1,1]|*> is being_S-Seq by A1, A2, A3, TOPREAL3:34; then L~ <*|[0,0]|,|[(|[0,0]| `1),(|[1,1]| `2)]|,|[1,1]|*> is being_S-P_arc by TOPREAL1:def_9; hence ex b1 being Subset of (TOP-REAL 2) st b1 is being_S-P_arc ; ::_thesis: verum end; end; theorem :: SPPOL_2:49 for P being Subset of (TOP-REAL 2) for p1, p2 being Point of (TOP-REAL 2) st P is_S-P_arc_joining p1,p2 holds P is_S-P_arc_joining p2,p1 proof let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st P is_S-P_arc_joining p1,p2 holds P is_S-P_arc_joining p2,p1 let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( P is_S-P_arc_joining p1,p2 implies P is_S-P_arc_joining p2,p1 ) given f being FinSequence of (TOP-REAL 2) such that A1: f is being_S-Seq and A2: P = L~ f and A3: p1 = f /. 1 and A4: p2 = f /. (len f) ; :: according to TOPREAL4:def_1 ::_thesis: P is_S-P_arc_joining p2,p1 take g = Rev f; :: according to TOPREAL4:def_1 ::_thesis: ( g is being_S-Seq & P = L~ g & p2 = g /. 1 & p1 = g /. (len g) ) thus ( g is being_S-Seq & P = L~ g ) by A1, A2, Th22; ::_thesis: ( p2 = g /. 1 & p1 = g /. (len g) ) len g = len f by FINSEQ_5:def_3; hence ( p2 = g /. 1 & p1 = g /. (len g) ) by A1, A3, A4, FINSEQ_5:65; ::_thesis: verum end; definition let p1, p2 be Point of (TOP-REAL 2); let P be Subset of (TOP-REAL 2); predp1,p2 split P means :Def1: :: SPPOL_2:def 1 ( 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; :: deftheorem Def1 defines split SPPOL_2:def_1_:_ for p1, p2 being Point of (TOP-REAL 2) for P being Subset of (TOP-REAL 2) holds ( p1,p2 split P iff ( 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) ) ) ); theorem Th50: :: SPPOL_2:50 for P being Subset of (TOP-REAL 2) for p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P holds p2,p1 split P proof let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P holds p2,p1 split P let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( p1,p2 split P implies p2,p1 split P ) assume A1: p1 <> p2 ; :: according to SPPOL_2:def_1 ::_thesis: ( for f1, f2 being S-Sequence_in_R2 holds ( not p1 = f1 /. 1 or not p1 = f2 /. 1 or not p2 = f1 /. (len f1) or not p2 = f2 /. (len f2) or not (L~ f1) /\ (L~ f2) = {p1,p2} or not P = (L~ f1) \/ (L~ f2) ) or p2,p1 split P ) 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) ; ::_thesis: p2,p1 split P thus p2 <> p1 by A1; :: according to SPPOL_2:def_1 ::_thesis: ex f1, f2 being S-Sequence_in_R2 st ( p2 = f1 /. 1 & p2 = f2 /. 1 & p1 = f1 /. (len f1) & p1 = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p2,p1} & P = (L~ f1) \/ (L~ f2) ) reconsider g1 = Rev f1, g2 = Rev f2 as S-Sequence_in_R2 ; take g1 ; ::_thesis: ex f2 being S-Sequence_in_R2 st ( p2 = g1 /. 1 & p2 = f2 /. 1 & p1 = g1 /. (len g1) & p1 = f2 /. (len f2) & (L~ g1) /\ (L~ f2) = {p2,p1} & P = (L~ g1) \/ (L~ f2) ) take g2 ; ::_thesis: ( p2 = g1 /. 1 & p2 = g2 /. 1 & p1 = g1 /. (len g1) & p1 = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p2,p1} & P = (L~ g1) \/ (L~ 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; ::_thesis: ( (L~ g1) /\ (L~ g2) = {p2,p1} & P = (L~ g1) \/ (L~ g2) ) L~ g1 = L~ f1 by Th22; hence ( (L~ g1) /\ (L~ g2) = {p2,p1} & P = (L~ g1) \/ (L~ g2) ) by A6, A7, Th22; ::_thesis: verum end; Lm16: for P being Subset of (TOP-REAL 2) for p1, p2, q being Point of (TOP-REAL 2) 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 holds 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 P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q being Point of (TOP-REAL 2) 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 holds 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) ) let p1, p2, q be Point of (TOP-REAL 2); ::_thesis: 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 holds 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) ) let f1, f2 be S-Sequence_in_R2; ::_thesis: ( 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 implies 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) ) ) assume 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 ; ::_thesis: 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) ) set f19 = Rev (f1 :- q); A9: 1 <= q .. f1 by A8, FINSEQ_4:21; A10: now__::_thesis:_not_1_=_q_.._f1 assume A11: 1 = q .. f1 ; ::_thesis: contradiction 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; ::_thesis: verum 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 (Rev (f1 :- q)) = rng (f1 :- q) by FINSEQ_5:57; then A15: rng (Rev (f1 :- q)) 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 = (f2 | l) ^ (Rev (f1 :- q)); A18: dom (f2 | l) = Seg (len (f2 | l)) by FINSEQ_1:def_3; len (f1 :- q) >= 1 by NAT_1:14; then A19: len (Rev (f1 :- q)) >= 1 by FINSEQ_5:def_3; then A20: len (Rev (f1 :- q)) in dom (Rev (f1 :- q)) by FINSEQ_3:25; A21: l < len f2 by XREAL_1:44; then A22: len (f2 | l) = 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 (f2 | l) by A22, FINSEQ_3:25; then A25: (f2 | l) /. (len (f2 | l)) = f2 /. l by A22, FINSEQ_4:70; A26: (Rev (f1 :- q)) /. 1 = (f1 :- q) /. (len (f1 :- q)) by FINSEQ_5:65 .= f2 /. (len f2) by A3, A4, A8, FINSEQ_5:54 ; then A27: LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)) = LSeg (f2,l) by A23, A14, A25, TOPREAL1:def_3; A28: now__::_thesis:_for_i_being_Element_of_NAT_st_1_<=_i_&_i_+_2_<=_len_(f2_|_l)_holds_ LSeg_((f2_|_l),i)_misses_LSeg_(((f2_|_l)_/._(len_(f2_|_l))),((Rev_(f1_:-_q))_/._1)) let i be Element of NAT ; ::_thesis: ( 1 <= i & i + 2 <= len (f2 | l) implies LSeg ((f2 | l),i) misses LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)) ) assume that 1 <= i and A29: i + 2 <= len (f2 | l) ; ::_thesis: LSeg ((f2 | l),i) misses LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)) (i + 1) + 1 <= len (f2 | l) by A29; then A30: i + 1 < len (f2 | l) by NAT_1:13; then LSeg ((f2 | l),i) = LSeg (f2,i) by Th3; hence LSeg ((f2 | l),i) misses LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)) by A22, A27, A30, TOPREAL1:def_7; ::_thesis: verum end; A31: 1 in dom f1 by FINSEQ_5:6; A32: now__::_thesis:_not_p1_in_L~_(Rev_(f1_:-_q)) 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~ (Rev (f1 :- q)) ; ::_thesis: contradiction then A35: p1 in L~ (f1 :- q) by Th22; then consider i being Element of NAT such that A36: 1 <= i and i + 1 <= len (f1 :- q) and A37: p1 in LSeg ((f1 :- q),i) by Th13; consider j being Nat such that A38: i = j + 1 by A36, NAT_1:6; A39: 1 < q .. f1 by A10, A9, XXREAL_0:1; reconsider j = 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; percases ( j = 0 or j <> 0 ) ; supposeA42: j = 0 ; ::_thesis: contradiction A43: 1 + 1 <= q .. f1 by A39, NAT_1:13; now__::_thesis:_contradiction percases ( q .. f1 = 2 or q .. f1 > 2 ) by A43, XXREAL_0:1; supposeA44: q .. f1 = 2 ; ::_thesis: contradiction A45: q .. f1 <= len f1 by A8, FINSEQ_4:21; now__::_thesis:_contradiction percases ( len f1 = 2 or len f1 > 2 ) by A44, A45, XXREAL_0:1; suppose len f1 = 2 ; ::_thesis: contradiction then len (f1 :- q) = ((len f1) - (len f1)) + 1 by A8, A44, FINSEQ_5:50; hence contradiction by A35, TOPREAL1:22; ::_thesis: verum end; suppose len f1 > 2 ; ::_thesis: contradiction 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; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; suppose q .. f1 > 2 ; ::_thesis: contradiction then 1 + 1 < j + (q .. f1) by A42; hence contradiction by A41, TOPREAL1:def_7; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; suppose j <> 0 ; ::_thesis: contradiction then 1 + 1 < j + (q .. f1) by A39, NAT_1:14, XREAL_1:8; hence contradiction by A41, TOPREAL1:def_7; ::_thesis: verum end; end; end; A47: now__::_thesis:_for_i_being_Element_of_NAT_st_2_<=_i_&_i_+_1_<=_len_(Rev_(f1_:-_q))_holds_ LSeg_((Rev_(f1_:-_q)),i)_misses_LSeg_(((f2_|_l)_/._(len_(f2_|_l))),((Rev_(f1_:-_q))_/._1)) let i be Element of NAT ; ::_thesis: ( 2 <= i & i + 1 <= len (Rev (f1 :- q)) implies LSeg ((Rev (f1 :- q)),i) misses LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)) ) assume that A48: 2 <= i and A49: i + 1 <= len (Rev (f1 :- q)) ; ::_thesis: LSeg ((Rev (f1 :- q)),i) misses LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)) reconsider m = (len (Rev (f1 :- q))) - (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 ((Rev (f1 :- q)),i) = LSeg ((f1 :- q),(m + 1)) by Th2 .= LSeg (f1,(m + (q .. f1))) by A8, Th10 ; then A51: LSeg ((Rev (f1 :- q)),i) c= L~ f1 by TOPREAL3:19; A52: now__::_thesis:_not_p2_in_LSeg_((Rev_(f1_:-_q)),i) 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 (Rev (f1 :- q)) = len (f1 :- q) by FINSEQ_5:def_3; A58: (len f1) - i = (((((len f1) - (q .. f1)) + 1) - 1) + (q .. f1)) - i .= (((len (Rev (f1 :- q))) - 1) + (q .. f1)) - i by A8, A57, FINSEQ_5:50 .= m + (q .. f1) ; percases ( i = 1 + 1 or i <> 2 ) ; supposeA59: i = 1 + 1 ; ::_thesis: not p2 in LSeg ((Rev (f1 :- q)),i) 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 ((Rev (f1 :- q)),i) ; ::_thesis: contradiction 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 ; ::_thesis: verum end; suppose i <> 2 ; ::_thesis: not p2 in LSeg ((Rev (f1 :- q)),i) 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 ((Rev (f1 :- q)),i) by A50, A56, XBOOLE_0:def_4; ::_thesis: verum end; end; end; LSeg ((Rev (f1 :- q)),i) c= L~ (Rev (f1 :- q)) by TOPREAL3:19; then A69: not p1 in LSeg ((Rev (f1 :- q)),i) by A32; LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)) c= L~ f2 by A27, TOPREAL3:19; then A70: (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),i)) c= {p1,p2} by A5, A51, XBOOLE_1:27; now__::_thesis:_for_x_being_set_holds_not_x_in_(LSeg_(((f2_|_l)_/._(len_(f2_|_l))),((Rev_(f1_:-_q))_/._1)))_/\_(LSeg_((Rev_(f1_:-_q)),i)) given x being set such that A71: x in (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),i)) ; ::_thesis: contradiction ( x = p1 or x = p2 ) by A70, A71, TARSKI:def_2; hence contradiction by A69, A52, A71, XBOOLE_0:def_4; ::_thesis: verum end; then (LSeg ((Rev (f1 :- q)),i)) /\ (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) = {} by XBOOLE_0:def_1; hence LSeg ((Rev (f1 :- q)),i) misses LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)) by XBOOLE_0:def_7; ::_thesis: verum end; A72: now__::_thesis:_(_len_(Rev_(f1_:-_q))_<>_1_implies_(LSeg_(((f2_|_l)_/._(len_(f2_|_l))),((Rev_(f1_:-_q))_/._1)))_/\_(LSeg_((Rev_(f1_:-_q)),1))_=_{((Rev_(f1_:-_q))_/._1)}_) assume len (Rev (f1 :- q)) <> 1 ; ::_thesis: (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) = {((Rev (f1 :- q)) /. 1)} then 1 < len (Rev (f1 :- q)) by A19, XXREAL_0:1; then A73: 1 + 1 <= len (Rev (f1 :- q)) by NAT_1:13; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_(LSeg_(((f2_|_l)_/._(len_(f2_|_l))),((Rev_(f1_:-_q))_/._1)))_/\_(LSeg_((Rev_(f1_:-_q)),1))_implies_x_=_(Rev_(f1_:-_q))_/._1_)_&_(_x_=_(Rev_(f1_:-_q))_/._1_implies_x_in_(LSeg_(((f2_|_l)_/._(len_(f2_|_l))),((Rev_(f1_:-_q))_/._1)))_/\_(LSeg_((Rev_(f1_:-_q)),1))_)_) let x be set ; ::_thesis: ( ( x in (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) implies x = (Rev (f1 :- q)) /. 1 ) & ( x = (Rev (f1 :- q)) /. 1 implies x in (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) ) ) hereby ::_thesis: ( x = (Rev (f1 :- q)) /. 1 implies x in (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) ) reconsider m = (len (Rev (f1 :- q))) - 2 as Element of NAT by A73, INT_1:5; LSeg ((Rev (f1 :- q)),1) c= L~ (Rev (f1 :- q)) by TOPREAL3:19; then not p1 in LSeg ((Rev (f1 :- q)),1) by A32; then A74: not p1 in (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) by XBOOLE_0:def_4; (m + 1) + 1 = len (f1 :- q) by FINSEQ_5:def_3; then LSeg ((Rev (f1 :- q)),1) = LSeg ((f1 :- q),(m + 1)) by Th2 .= LSeg (f1,(m + (q .. f1))) by A8, Th10 ; then A75: LSeg ((Rev (f1 :- q)),1) c= L~ f1 by TOPREAL3:19; LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)) c= L~ f2 by A27, TOPREAL3:19; then A76: (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) c= {p1,p2} by A5, A75, XBOOLE_1:27; assume x in (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) ; ::_thesis: x = (Rev (f1 :- q)) /. 1 hence x = (Rev (f1 :- q)) /. 1 by A4, A26, A76, A74, TARSKI:def_2; ::_thesis: verum end; assume A77: x = (Rev (f1 :- q)) /. 1 ; ::_thesis: x in (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) then x in LSeg (((Rev (f1 :- q)) /. 1),((Rev (f1 :- q)) /. (1 + 1))) by RLTOPSP1:68; then A78: x in LSeg ((Rev (f1 :- q)),1) by A73, TOPREAL1:def_3; x in LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)) by A77, RLTOPSP1:68; hence x in (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) by A78, XBOOLE_0:def_4; ::_thesis: verum end; hence (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) /\ (LSeg ((Rev (f1 :- q)),1)) = {((Rev (f1 :- q)) /. 1)} by TARSKI:def_1; ::_thesis: verum end; A79: len (f2 | l) >= 1 by A21, A23, FINSEQ_1:59; then A80: not f2 | l is empty ; f1 :- q is unfolded by A8, Th27; then A81: Rev (f1 :- q) is unfolded by Th28; A82: now__::_thesis:_(f2_|_l)_^_(Rev_(f1_:-_q))_is_unfolded percases ( ( len (f2 | l) = 1 & len (Rev (f1 :- q)) = 1 ) or ( len (f2 | l) <> 1 & len (Rev (f1 :- q)) = 1 ) or ( len (f2 | l) = 1 & len (Rev (f1 :- q)) <> 1 ) or ( len (f2 | l) <> 1 & len (Rev (f1 :- q)) <> 1 ) ) ; suppose ( len (f2 | l) = 1 & len (Rev (f1 :- q)) = 1 ) ; ::_thesis: (f2 | l) ^ (Rev (f1 :- q)) is unfolded then len ((f2 | l) ^ (Rev (f1 :- q))) = 1 + 1 by FINSEQ_1:22; hence (f2 | l) ^ (Rev (f1 :- q)) is unfolded by Th26; ::_thesis: verum end; supposethat A83: len (f2 | l) <> 1 and A84: len (Rev (f1 :- q)) = 1 ; ::_thesis: (f2 | l) ^ (Rev (f1 :- q)) is unfolded consider k being Nat such that A85: k + 1 = len (f2 | l) by A79, NAT_1:6; reconsider k = k as Element of NAT by ORDINAL1:def_12; A86: LSeg ((f2 | l),k) = LSeg (f2,k) by A85, Th3; len (f2 | l) > 1 by A22, A23, A83, XXREAL_0:1; then A87: 1 <= k by A85, NAT_1:13; A88: Rev (f1 :- q) = <*((Rev (f1 :- q)) /. 1)*> by A84, FINSEQ_5:14; k + (1 + 1) <= len f2 by A22, A85; then (LSeg ((f2 | l),k)) /\ (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) = {((f2 | l) /. (len (f2 | l)))} by A22, A25, A27, A85, A87, A86, TOPREAL1:def_6; hence (f2 | l) ^ (Rev (f1 :- q)) is unfolded by A85, A88, Th30; ::_thesis: verum end; supposethat A89: len (f2 | l) = 1 and A90: len (Rev (f1 :- q)) <> 1 ; ::_thesis: (f2 | l) ^ (Rev (f1 :- q)) is unfolded f2 | l = <*((f2 | l) /. (len (f2 | l)))*> by A89, FINSEQ_5:14; hence (f2 | l) ^ (Rev (f1 :- q)) is unfolded by A81, A72, A90, Th29; ::_thesis: verum end; supposethat A91: len (f2 | l) <> 1 and A92: len (Rev (f1 :- q)) <> 1 ; ::_thesis: (f2 | l) ^ (Rev (f1 :- q)) is unfolded consider k being Nat such that A93: k + 1 = len (f2 | l) by A79, NAT_1:6; reconsider k = k as Element of NAT by ORDINAL1:def_12; A94: k + (1 + 1) <= len f2 by A22, A93; A95: LSeg ((f2 | l),k) = LSeg (f2,k) by A93, Th3; len (f2 | l) > 1 by A22, A23, A91, XXREAL_0:1; then 1 <= k by A93, NAT_1:13; then (LSeg ((f2 | l),k)) /\ (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1))) = {((f2 | l) /. (len (f2 | l)))} by A22, A25, A27, A93, A94, A95, TOPREAL1:def_6; hence (f2 | l) ^ (Rev (f1 :- q)) is unfolded by A81, A72, A92, A93, Th31; ::_thesis: verum end; end; end; len g1 >= 2 by TOPREAL1:def_8; then A96: rng g1 c= L~ g1 by Th18; set Z = (rng (f2 | l)) /\ (rng (Rev (f1 :- q))); A97: 1 in dom (f2 | l) 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__::_thesis:_not_p2_in_rng_(f2_|_l) assume A100: p2 in rng (f2 | l) ; ::_thesis: contradiction then p2 .. (f2 | l) = p2 .. f2 by FINSEQ_5:40; hence contradiction by A22, A99, A100, FINSEQ_4:21, XREAL_1:44; ::_thesis: verum end; then A101: not p2 in (rng (f2 | l)) /\ (rng (Rev (f1 :- q))) by XBOOLE_0:def_4; then A102: (rng (f2 | l)) /\ (rng (Rev (f1 :- q))) <> {p1,p2} by TARSKI:def_2; dom f2 = Seg (len f2) by FINSEQ_1:def_3; then A103: len (f2 | l) in dom f2 by A22, A14, A24, A18, FINSEQ_2:8; now__::_thesis:_not_p2_in_L~_(f2_|_l) p2 in LSeg ((f2 /. (len (f2 | l))),p2) by RLTOPSP1:68; then A104: p2 in LSeg (f2,(len (f2 | l))) by A4, A22, A23, A14, TOPREAL1:def_3; assume p2 in L~ (f2 | l) ; ::_thesis: contradiction then consider i being Element of NAT such that A105: 1 <= i and A106: i + 1 <= len (f2 | l) and A107: p2 in LSeg ((f2 | l),i) by Th13; LSeg ((f2 | l),i) = LSeg (f2,i) by A106, Th3; then A108: p2 in (LSeg (f2,i)) /\ (LSeg (f2,(len (f2 | l)))) by A107, A104, XBOOLE_0:def_4; then A109: LSeg (f2,i) meets LSeg (f2,(len (f2 | l))) by XBOOLE_0:4; A110: len f2 <> len (f2 | l) by A21, FINSEQ_1:59; percases ( i + 1 = len (f2 | l) or i + 1 <> len (f2 | l) ) ; supposeA111: i + 1 = len (f2 | l) ; ::_thesis: contradiction then i + (1 + 1) = len f2 by A22; then (LSeg (f2,i)) /\ (LSeg (f2,(len (f2 | l)))) = {(f2 /. (len (f2 | l)))} by A105, A111, TOPREAL1:def_6; then p2 = f2 /. (len (f2 | l)) by A108, TARSKI:def_1; hence contradiction by A4, A98, A103, A110, PARTFUN2:10; ::_thesis: verum end; suppose i + 1 <> len (f2 | l) ; ::_thesis: contradiction then i + 1 < len (f2 | l) by A106, XXREAL_0:1; hence contradiction by A109, TOPREAL1:def_7; ::_thesis: verum end; end; end; then A112: not p2 in (L~ (f2 | l)) /\ (L~ (Rev (f1 :- q))) by XBOOLE_0:def_4; L~ (f1 :- q) c= L~ f1 by A8, Lm15; then A113: L~ (Rev (f1 :- q)) c= L~ f1 by Th22; L~ (f2 | l) c= L~ f2 by Lm1; then (L~ (f2 | l)) /\ (L~ (Rev (f1 :- q))) c= {p1,p2} by A5, A113, XBOOLE_1:27; then A114: ( (L~ (f2 | l)) /\ (L~ (Rev (f1 :- q))) = {} or (L~ (f2 | l)) /\ (L~ (Rev (f1 :- q))) = {p1} or (L~ (f2 | l)) /\ (L~ (Rev (f1 :- q))) = {p2} or (L~ (f2 | l)) /\ (L~ (Rev (f1 :- q))) = {p1,p2} ) by ZFMISC_1:36; f1 :- q is special by A8, Th39; then A115: Rev (f1 :- q) is special by Th40; A116: 1 in dom (f1 :- q) by FINSEQ_5:6; now__::_thesis:_not_p1_in_rng_(f1_:-_q) set l = p1 .. (f1 :- q); assume A117: p1 in rng (f1 :- q) ; ::_thesis: contradiction then A118: (f1 :- q) . (p1 .. (f1 :- q)) = p1 by FINSEQ_4:19; p1 .. (f1 :- q) <> 0 by A117, FINSEQ_4:21; then consider j being Nat such that A119: p1 .. (f1 :- q) = j + 1 by NAT_1:6; reconsider j = j as Element of NAT by ORDINAL1:def_12; A120: p1 .. (f1 :- q) 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) /. (p1 .. (f1 :- q)) = 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; ::_thesis: verum end; then not p1 in rng (Rev (f1 :- q)) by FINSEQ_5:57; then not p1 in (rng (f2 | l)) /\ (rng (Rev (f1 :- q))) by XBOOLE_0:def_4; then A123: (rng (f2 | l)) /\ (rng (Rev (f1 :- q))) <> {p1} by TARSKI:def_1; rng (f2 | l) c= rng f2 by FINSEQ_5:19; then (rng (f2 | l)) /\ (rng (Rev (f1 :- q))) c= (rng f2) /\ (rng f1) by A15, XBOOLE_1:27; then A124: (rng (f2 | l)) /\ (rng (Rev (f1 :- q))) 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: Rev (f1 :- q) is s.n.c. by Th35; ( ((f2 | l) /. (len (f2 | l))) `1 = ((Rev (f1 :- q)) /. 1) `1 or ((f2 | l) /. (len (f2 | l))) `2 = ((Rev (f1 :- q)) /. 1) `2 ) by A23, A14, A25, A26, TOPREAL1:def_5; then A127: (f2 | l) ^ (Rev (f1 :- q)) is special by A115, Lm13; (len (f2 | l)) + (len (Rev (f1 :- q))) >= 1 + 1 by A22, A19, A23, XREAL_1:7; then A128: len ((f2 | l) ^ (Rev (f1 :- q))) >= 2 by FINSEQ_1:22; (rng (f2 | l)) /\ (rng (Rev (f1 :- q))) <> {p2} by A101, TARSKI:def_1; then (rng (f2 | l)) /\ (rng (Rev (f1 :- q))) = {} by A123, A102, A124, ZFMISC_1:36; then rng (f2 | l) misses rng (Rev (f1 :- q)) by XBOOLE_0:def_7; then A129: (f2 | l) ^ (Rev (f1 :- q)) is one-to-one by A125, FINSEQ_3:91; not p1 in (L~ (f2 | l)) /\ (L~ (Rev (f1 :- q))) by A32, XBOOLE_0:def_4; then L~ (f2 | l) misses L~ (Rev (f1 :- q)) by A114, A112, TARSKI:def_1, TARSKI:def_2, XBOOLE_0:def_7; then (f2 | l) ^ (Rev (f1 :- q)) is s.n.c. by A126, A28, A47, Th36; then reconsider g2 = (f2 | l) ^ (Rev (f1 :- q)) as S-Sequence_in_R2 by A129, A128, A82, A127, TOPREAL1:def_8; A130: (L~ f2) \/ (L~ (Rev (f1 :- q))) = (L~ ((f2 | l) ^ <*p2*>)) \/ (L~ (Rev (f1 :- q))) by A4, A14, FINSEQ_5:21 .= ((L~ (f2 | l)) \/ (LSeg (((f2 | l) /. (len (f2 | l))),((Rev (f1 :- q)) /. 1)))) \/ (L~ (Rev (f1 :- q))) by A4, A97, A26, Th19, RELAT_1:38 .= L~ g2 by A20, A80, Th23, RELAT_1:38 ; take g1 ; ::_thesis: ex 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) ) take g2 ; ::_thesis: ( 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) ) thus A131: p1 = g1 /. 1 by A1, A8, FINSEQ_5:44; ::_thesis: ( p1 = g2 /. 1 & q = g1 /. (len g1) & q = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) ) A132: 1 in dom g2 by FINSEQ_5:6; hence A133: g2 /. 1 = g2 . 1 by PARTFUN1:def_6 .= (f2 | l) . 1 by A97, FINSEQ_1:def_7 .= (f2 | l) /. 1 by A97, PARTFUN1:def_6 .= p1 by A2, A97, FINSEQ_4:70 ; ::_thesis: ( q = g1 /. (len g1) & q = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) ) thus A134: q = g1 /. (q .. f1) by A8, FINSEQ_5:45 .= g1 /. (len g1) by A8, FINSEQ_5:42 ; ::_thesis: ( q = g2 /. (len g2) & (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) ) A135: len g2 in dom g2 by FINSEQ_5:6; hence A136: g2 /. (len g2) = g2 . (len g2) by PARTFUN1:def_6 .= g2 . ((len (f2 | l)) + (len (Rev (f1 :- q)))) by FINSEQ_1:22 .= (Rev (f1 :- q)) . (len (Rev (f1 :- q))) by A20, FINSEQ_1:def_7 .= (Rev (f1 :- q)) . (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 ; ::_thesis: ( (L~ g1) /\ (L~ g2) = {p1,q} & P = (L~ g1) \/ (L~ g2) ) 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) ::_thesis: P = (L~ g1) \/ (L~ g2) proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: (L~ g1) /\ (L~ g2) c= {p1,q} let x be set ; ::_thesis: ( x in {p1,q} implies b1 in (L~ g1) /\ (L~ g2) ) assume A139: x in {p1,q} ; ::_thesis: b1 in (L~ g1) /\ (L~ g2) percases ( x = p1 or x = q ) by A139, TARSKI:def_2; supposeA140: x = p1 ; ::_thesis: b1 in (L~ g1) /\ (L~ g2) 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; ::_thesis: verum end; supposeA142: x = q ; ::_thesis: b1 in (L~ g1) /\ (L~ g2) 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; ::_thesis: verum end; end; end; A144: len f1 in dom f1 by FINSEQ_5:6; A145: (L~ g1) /\ (L~ g2) = ((L~ g1) /\ (L~ f2)) \/ ((L~ g1) /\ (L~ (Rev (f1 :- q)))) 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; percases ( q <> p2 or q = p2 ) ; supposeA149: q <> p2 ; ::_thesis: (L~ g1) /\ (L~ g2) c= {p1,q} now__::_thesis:_not_p2_in_L~_g1 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 ; ::_thesis: contradiction then consider i being Element of NAT 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; percases ( i + 1 = j or i + 1 <> j ) ; supposeA160: i + 1 = j ; ::_thesis: contradiction 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; ::_thesis: verum end; suppose i + 1 <> j ; ::_thesis: contradiction 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; ::_thesis: verum end; 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, TARSKI:def_2, ZFMISC_1:33; (L~ g1) /\ (L~ (Rev (f1 :- q))) = (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 (L~ g1) /\ (L~ g2) c= {p1,q} by ENUMSET1:1; ::_thesis: verum end; supposeA163: q = p2 ; ::_thesis: (L~ g1) /\ (L~ g2) c= {p1,q} 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~ (Rev (f1 :- q))) = (L~ g1) /\ (L~ (f1 :- q)) by Th22 .= (L~ g1) /\ {} by A164, TOPREAL1:22 .= {} ; hence (L~ g1) /\ (L~ g2) c= {p1,q} by A5, A8, A145, A163, Lm14, XBOOLE_1:26; ::_thesis: verum end; 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 ; ::_thesis: verum end; theorem Th51: :: SPPOL_2:51 for P being Subset of (TOP-REAL 2) for p1, p2, q being Point of (TOP-REAL 2) st p1,p2 split P & q in P & q <> p1 holds p1,q split P proof let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q being Point of (TOP-REAL 2) st p1,p2 split P & q in P & q <> p1 holds p1,q split P let p1, p2, q be Point of (TOP-REAL 2); ::_thesis: ( p1,p2 split P & q in P & q <> p1 implies p1,q split P ) assume p1 <> p2 ; :: according to SPPOL_2:def_1 ::_thesis: ( for f1, f2 being S-Sequence_in_R2 holds ( not p1 = f1 /. 1 or not p1 = f2 /. 1 or not p2 = f1 /. (len f1) or not p2 = f2 /. (len f2) or not (L~ f1) /\ (L~ f2) = {p1,p2} or not P = (L~ f1) \/ (L~ f2) ) or not q in P or not q <> p1 or p1,q split P ) 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) ; ::_thesis: ( not q in P or not q <> p1 or p1,q split P ) assume A7: q in P ; ::_thesis: ( not q <> p1 or p1,q split P ) assume A8: q <> p1 ; ::_thesis: p1,q split P hence p1 <> q ; :: according to SPPOL_2:def_1 ::_thesis: ex f1, f2 being S-Sequence_in_R2 st ( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) ) percases ( q in L~ f1 or q in L~ f2 ) by A6, A7, XBOOLE_0:def_3; supposeA9: q in L~ f1 ; ::_thesis: ex f1, f2 being S-Sequence_in_R2 st ( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) ) now__::_thesis:_ex_f1,_f2_being_S-Sequence_in_R2_st_ (_p1_=_f1_/._1_&_p1_=_f2_/._1_&_q_=_f1_/._(len_f1)_&_q_=_f2_/._(len_f2)_&_(L~_f1)_/\_(L~_f2)_=_{p1,q}_&_P_=_(L~_f1)_\/_(L~_f2)_) percases ( q in rng f1 or not q in rng f1 ) ; suppose q in rng f1 ; ::_thesis: ex f1, f2 being S-Sequence_in_R2 st ( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) ) hence ex f1, f2 being S-Sequence_in_R2 st ( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) ) by A1, A2, A3, A4, A5, A6, A8, Lm16; ::_thesis: verum end; supposeA10: not q in rng f1 ; ::_thesis: ex f1, f2 being S-Sequence_in_R2 st ( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) ) consider i being Element of NAT 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 ex f1, f2 being S-Sequence_in_R2 st ( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) ) by A2, A4, A5, A6, A8, A16, A15, A14, Lm16; ::_thesis: verum end; end; end; hence ex f1, f2 being S-Sequence_in_R2 st ( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) ) ; ::_thesis: verum end; supposeA17: q in L~ f2 ; ::_thesis: ex f1, f2 being S-Sequence_in_R2 st ( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) ) now__::_thesis:_ex_f1,_f2_being_S-Sequence_in_R2_st_ (_p1_=_f1_/._1_&_p1_=_f2_/._1_&_q_=_f1_/._(len_f1)_&_q_=_f2_/._(len_f2)_&_(L~_f1)_/\_(L~_f2)_=_{p1,q}_&_P_=_(L~_f1)_\/_(L~_f2)_) percases ( q in rng f2 or not q in rng f2 ) ; suppose q in rng f2 ; ::_thesis: ex f1, f2 being S-Sequence_in_R2 st ( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) ) hence ex f1, f2 being S-Sequence_in_R2 st ( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) ) by A1, A2, A3, A4, A5, A6, A8, Lm16; ::_thesis: verum end; supposeA18: not q in rng f2 ; ::_thesis: ex f1, f2 being S-Sequence_in_R2 st ( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) ) consider i being Element of NAT 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 ex f1, f2 being S-Sequence_in_R2 st ( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) ) by A1, A3, A5, A6, A8, A24, A23, A22, Lm16; ::_thesis: verum end; end; end; hence ex f1, f2 being S-Sequence_in_R2 st ( p1 = f1 /. 1 & p1 = f2 /. 1 & q = f1 /. (len f1) & q = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {p1,q} & P = (L~ f1) \/ (L~ f2) ) ; ::_thesis: verum end; end; end; theorem Th52: :: SPPOL_2:52 for P being Subset of (TOP-REAL 2) for p1, p2, q being Point of (TOP-REAL 2) st p1,p2 split P & q in P & q <> p2 holds q,p2 split P proof let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q being Point of (TOP-REAL 2) st p1,p2 split P & q in P & q <> p2 holds q,p2 split P let p1, p2, q be Point of (TOP-REAL 2); ::_thesis: ( p1,p2 split P & q in P & q <> p2 implies q,p2 split P ) assume that A1: p1,p2 split P and A2: q in P and A3: q <> p2 ; ::_thesis: q,p2 split P p2,p1 split P by A1, Th50; then p2,q split P by A2, A3, Th51; hence q,p2 split P by Th50; ::_thesis: verum end; theorem Th53: :: SPPOL_2:53 for P being Subset of (TOP-REAL 2) for p1, p2, q1, q2 being Point of (TOP-REAL 2) st p1,p2 split P & q1 in P & q2 in P & q1 <> q2 holds q1,q2 split P proof let P be Subset of (TOP-REAL 2); ::_thesis: for p1, p2, q1, q2 being Point of (TOP-REAL 2) st p1,p2 split P & q1 in P & q2 in P & q1 <> q2 holds q1,q2 split P let p1, p2, q1, q2 be Point of (TOP-REAL 2); ::_thesis: ( p1,p2 split P & q1 in P & q2 in P & q1 <> q2 implies q1,q2 split P ) assume that A1: p1,p2 split P and A2: q1 in P and A3: q2 in P and A4: q1 <> q2 ; ::_thesis: q1,q2 split P A5: p2,p1 split P by A1, Th50; percases ( p1 = q1 or p1 = q2 or p1 <> q1 or p2 <> q1 ) ; suppose p1 = q1 ; ::_thesis: q1,q2 split P hence q1,q2 split P by A1, A3, A4, Th51; ::_thesis: verum end; suppose p1 = q2 ; ::_thesis: q1,q2 split P hence q1,q2 split P by A2, A4, A5, Th52; ::_thesis: verum end; suppose p1 <> q1 ; ::_thesis: q1,q2 split P then p1,q1 split P by A1, A2, Th51; then q2,q1 split P by A3, A4, Th52; hence q1,q2 split P by Th50; ::_thesis: verum end; suppose p2 <> q1 ; ::_thesis: q1,q2 split P then q1,p2 split P by A1, A2, Th52; hence q1,q2 split P by A3, A4, Th51; ::_thesis: verum end; end; end; notation let P be Subset of (TOP-REAL 2); synonym special_polygonal P for being_special_polygon ; end; definition let P be Subset of (TOP-REAL 2); redefine attr P is being_special_polygon means :Def2: :: SPPOL_2:def 2 ex p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P; compatibility ( P is special_polygonal iff ex p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P ) proof thus ( P is being_special_polygon implies ex p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P ) ::_thesis: ( ex p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P implies P is special_polygonal ) 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 ; :: according to TOPREAL4:def_2 ::_thesis: ex p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P take p1 ; ::_thesis: ex p2 being Point of (TOP-REAL 2) st p1,p2 split P take p2 ; ::_thesis: p1,p2 split P thus p1 <> p2 by A1; :: according to SPPOL_2:def_1 ::_thesis: 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) ) consider f1 being FinSequence of (TOP-REAL 2) 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 being FinSequence of (TOP-REAL 2) 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 = f1, f2 = f2 as S-Sequence_in_R2 by A6, A10; take f1 ; ::_thesis: ex 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) ) take f2 ; ::_thesis: ( 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) ) thus ( 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) ) by A4, A5, A7, A8, A9, A11, A12, A13; ::_thesis: verum end; given p1, p2 being Point of (TOP-REAL 2) such that A14: p1,p2 split P ; ::_thesis: P is special_polygonal 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 ; :: according to TOPREAL4:def_2 ::_thesis: ex b1 being Element of the carrier of (TOP-REAL 2) ex b2, b3 being Element of bool the carrier of (TOP-REAL 2) st ( not p1 = b1 & p1 in P & b1 in P & b2 is_S-P_arc_joining p1,b1 & b3 is_S-P_arc_joining p1,b1 & b2 /\ b3 = {p1,b1} & P = b2 \/ b3 ) take p2 ; ::_thesis: ex b1, b2 being Element of bool the carrier of (TOP-REAL 2) st ( not p1 = p2 & p1 in P & p2 in P & b1 is_S-P_arc_joining p1,p2 & b2 is_S-P_arc_joining p1,p2 & b1 /\ b2 = {p1,p2} & P = b1 \/ b2 ) take P1 = L~ f1; ::_thesis: ex b1 being Element of bool the carrier of (TOP-REAL 2) st ( not p1 = p2 & p1 in P & p2 in P & P1 is_S-P_arc_joining p1,p2 & b1 is_S-P_arc_joining p1,p2 & P1 /\ b1 = {p1,p2} & P = P1 \/ b1 ) take P2 = L~ f2; ::_thesis: ( not 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 ) thus p1 <> p2 by A14, Def1; ::_thesis: ( 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 ) {p1,p2} c= P by A21, A22, XBOOLE_1:29; hence ( p1 in P & p2 in P ) by A16, A15; ::_thesis: ( P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 ) thus ex f being FinSequence of (TOP-REAL 2) st ( f is being_S-Seq & P1 = L~ f & p1 = f /. 1 & p2 = f /. (len f) ) by A17, A19; :: according to TOPREAL4:def_1 ::_thesis: ( P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 ) thus ex f being FinSequence of (TOP-REAL 2) st ( f is being_S-Seq & P2 = L~ f & p1 = f /. 1 & p2 = f /. (len f) ) by A18, A20; :: according to TOPREAL4:def_1 ::_thesis: ( P1 /\ P2 = {p1,p2} & P = P1 \/ P2 ) thus ( P1 /\ P2 = {p1,p2} & P = P1 \/ P2 ) by A21, A22; ::_thesis: verum end; end; :: deftheorem Def2 defines special_polygonal SPPOL_2:def_2_:_ for P being Subset of (TOP-REAL 2) holds ( P is special_polygonal iff ex p1, p2 being Point of (TOP-REAL 2) st p1,p2 split P ); Lm17: for P being Subset of (TOP-REAL 2) st P is being_special_polygon holds ex p1, p2 being Point of (TOP-REAL 2) st ( p1 <> p2 & p1 in P & p2 in P ) proof let P be Subset of (TOP-REAL 2); ::_thesis: ( P is being_special_polygon implies ex p1, p2 being Point of (TOP-REAL 2) st ( p1 <> p2 & p1 in P & p2 in P ) ) assume P is being_special_polygon ; ::_thesis: ex p1, p2 being Point of (TOP-REAL 2) st ( p1 <> p2 & p1 in P & p2 in P ) then ex p1, p2 being Point of (TOP-REAL 2) ex 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 ex p1, p2 being Point of (TOP-REAL 2) st ( p1 <> p2 & p1 in P & p2 in P ) ; ::_thesis: verum end; definition let r1, r2, r19, r29 be real number ; func[.r1,r2,r19,r29.] -> Subset of (TOP-REAL 2) equals :: SPPOL_2:def 3 ((LSeg (|[r1,r19]|,|[r1,r29]|)) \/ (LSeg (|[r1,r29]|,|[r2,r29]|))) \/ ((LSeg (|[r2,r29]|,|[r2,r19]|)) \/ (LSeg (|[r2,r19]|,|[r1,r19]|))); coherence ((LSeg (|[r1,r19]|,|[r1,r29]|)) \/ (LSeg (|[r1,r29]|,|[r2,r29]|))) \/ ((LSeg (|[r2,r29]|,|[r2,r19]|)) \/ (LSeg (|[r2,r19]|,|[r1,r19]|))) is Subset of (TOP-REAL 2) ; end; :: deftheorem defines [. SPPOL_2:def_3_:_ for r1, r2, r19, r29 being real number holds [.r1,r2,r19,r29.] = ((LSeg (|[r1,r19]|,|[r1,r29]|)) \/ (LSeg (|[r1,r29]|,|[r2,r29]|))) \/ ((LSeg (|[r2,r29]|,|[r2,r19]|)) \/ (LSeg (|[r2,r19]|,|[r1,r19]|))); registration let n be Element of NAT ; let p1, p2 be Point of (TOP-REAL n); cluster LSeg (p1,p2) -> compact ; coherence LSeg (p1,p2) is compact ; end; registration let r1, r2, r19, r29 be real number ; cluster[.r1,r2,r19,r29.] -> non empty compact ; coherence ( not [.r1,r2,r19,r29.] is empty & [.r1,r2,r19,r29.] is compact ) proof thus not [.r1,r2,r19,r29.] is empty ; ::_thesis: [.r1,r2,r19,r29.] is compact 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 [.r1,r2,r19,r29.] is compact by A1, COMPTS_1:10; ::_thesis: verum end; end; theorem :: SPPOL_2:54 for r1, r2, r19, r29 being real number st r1 <= r2 & r19 <= r29 holds [.r1,r2,r19,r29.] = { p where p is Point of (TOP-REAL 2) : ( ( 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 let r1, r2, r19, r29 be real number ; ::_thesis: ( r1 <= r2 & r19 <= r29 implies [.r1,r2,r19,r29.] = { p where p is Point of (TOP-REAL 2) : ( ( 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 ) ) } ) assume that A1: r1 <= r2 and A2: r19 <= r29 ; ::_thesis: [.r1,r2,r19,r29.] = { p where p is Point of (TOP-REAL 2) : ( ( 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 ) ) } set p1 = |[r1,r19]|; set p2 = |[r1,r29]|; set p3 = |[r2,r29]|; set p4 = |[r2,r19]|; set P4 = { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ; set P3 = { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } ; set P2 = { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } ; set P1 = { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } ; set P = { p where p is Point of (TOP-REAL 2) : ( ( 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 where p is Point of (TOP-REAL 2) : ( ( 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 ) ) } = ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ) proof hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ) c= { p where p is Point of (TOP-REAL 2) : ( ( 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 ) ) } let x be set ; ::_thesis: ( x in { p where p is Point of (TOP-REAL 2) : ( ( 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 ) ) } implies x in ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ) ) assume x in { p where p is Point of (TOP-REAL 2) : ( ( 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 ) ) } ; ::_thesis: x in ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ) then ex p being Point of (TOP-REAL 2) 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 { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } or x in { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } or x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } or x in { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ) ; then ( x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } or x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ) by XBOOLE_0:def_3; hence x in ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ) by XBOOLE_0:def_3; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ) or x in { p where p is Point of (TOP-REAL 2) : ( ( 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 ) ) } ) assume x in ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ) ; ::_thesis: x in { p where p is Point of (TOP-REAL 2) : ( ( 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 A4: ( x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } or x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ) by XBOOLE_0:def_3; percases ( x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } or x in { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } or x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } or x in { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ) by A4, XBOOLE_0:def_3; suppose x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } ; ::_thesis: x in { p where p is Point of (TOP-REAL 2) : ( ( 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 ex p being Point of (TOP-REAL 2) st ( x = p & p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) ; hence x in { p where p is Point of (TOP-REAL 2) : ( ( 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 ) ) } ; ::_thesis: verum end; suppose x in { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } ; ::_thesis: x in { p where p is Point of (TOP-REAL 2) : ( ( 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 ex p being Point of (TOP-REAL 2) st ( x = p & p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) ; hence x in { p where p is Point of (TOP-REAL 2) : ( ( 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 ) ) } ; ::_thesis: verum end; suppose x in { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } ; ::_thesis: x in { p where p is Point of (TOP-REAL 2) : ( ( 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 ex p being Point of (TOP-REAL 2) st ( x = p & p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) ; hence x in { p where p is Point of (TOP-REAL 2) : ( ( 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 ) ) } ; ::_thesis: verum end; suppose x in { p where p is Point of (TOP-REAL 2) : ( p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) } ; ::_thesis: x in { p where p is Point of (TOP-REAL 2) : ( ( 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 ex p being Point of (TOP-REAL 2) st ( x = p & p `2 = r19 & r1 <= p `1 & p `1 <= r2 ) ; hence x in { p where p is Point of (TOP-REAL 2) : ( ( 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 ) ) } ; ::_thesis: verum end; end; end; thus [.r1,r2,r19,r29.] = ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ (LSeg (|[r1,r29]|,|[r2,r29]|))) \/ ((LSeg (|[r2,r29]|,|[r2,r19]|)) \/ (LSeg (|[r2,r19]|,|[r1,r19]|))) by A2, TOPREAL3:9 .= ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } ) \/ ((LSeg (|[r2,r29]|,|[r2,r19]|)) \/ (LSeg (|[r2,r19]|,|[r1,r19]|))) by A1, TOPREAL3:10 .= ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r1 & r19 <= p `2 & p `2 <= r29 ) } \/ { p where p is Point of (TOP-REAL 2) : ( p `2 = r29 & r1 <= p `1 & p `1 <= r2 ) } ) \/ ( { p where p is Point of (TOP-REAL 2) : ( p `1 = r2 & r19 <= p `2 & p `2 <= r29 ) } \/ (LSeg (|[r2,r19]|,|[r1,r19]|))) by A2, TOPREAL3:9 .= { p where p is Point of (TOP-REAL 2) : ( ( 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 ) ) } by A1, A3, TOPREAL3:10 ; ::_thesis: verum end; theorem Th55: :: SPPOL_2:55 for r1, r2, r19, r29 being real number st r1 <> r2 & r19 <> r29 holds [.r1,r2,r19,r29.] is special_polygonal proof let r1, r2, r19, r29 be real number ; ::_thesis: ( r1 <> r2 & r19 <> r29 implies [.r1,r2,r19,r29.] is special_polygonal ) assume that A1: r1 <> r2 and A2: r19 <> r29 ; ::_thesis: [.r1,r2,r19,r29.] is special_polygonal set p1 = |[r1,r19]|; set p2 = |[r1,r29]|; set p3 = |[r2,r29]|; set p4 = |[r2,r19]|; A3: |[r2,r29]| `1 = r2 by EUCLID:52; take |[r1,r19]| ; :: according to SPPOL_2:def_2 ::_thesis: ex p2 being Point of (TOP-REAL 2) st |[r1,r19]|,p2 split [.r1,r2,r19,r29.] take |[r2,r29]| ; ::_thesis: |[r1,r19]|,|[r2,r29]| split [.r1,r2,r19,r29.] thus |[r1,r19]| <> |[r2,r29]| by A1, FINSEQ_1:77; :: according to SPPOL_2:def_1 ::_thesis: ex f1, f2 being S-Sequence_in_R2 st ( |[r1,r19]| = f1 /. 1 & |[r1,r19]| = f2 /. 1 & |[r2,r29]| = f1 /. (len f1) & |[r2,r29]| = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {|[r1,r19]|,|[r2,r29]|} & [.r1,r2,r19,r29.] = (L~ f1) \/ (L~ f2) ) A4: |[r2,r19]| `1 = r2 by EUCLID:52; A5: |[r2,r29]| `2 = r29 by EUCLID:52; A6: |[r2,r19]| `2 = r19 by EUCLID:52; set f1 = <*|[r1,r19]|,|[r1,r29]|,|[r2,r29]|*>; set f2 = <*|[r1,r19]|,|[r2,r19]|,|[r2,r29]|*>; A7: |[r1,r19]| `1 = r1 by EUCLID:52; A8: len <*|[r1,r19]|,|[r2,r19]|,|[r2,r29]|*> = 3 by FINSEQ_1:45; A9: len <*|[r1,r19]|,|[r1,r29]|,|[r2,r29]|*> = 3 by FINSEQ_1:45; A10: |[r1,r19]| `2 = r19 by EUCLID:52; then reconsider f1 = <*|[r1,r19]|,|[r1,r29]|,|[r2,r29]|*>, f2 = <*|[r1,r19]|,|[r2,r19]|,|[r2,r29]|*> as S-Sequence_in_R2 by A1, A2, A7, A3, A5, TOPREAL3:34, TOPREAL3:35; take f1 ; ::_thesis: ex f2 being S-Sequence_in_R2 st ( |[r1,r19]| = f1 /. 1 & |[r1,r19]| = f2 /. 1 & |[r2,r29]| = f1 /. (len f1) & |[r2,r29]| = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {|[r1,r19]|,|[r2,r29]|} & [.r1,r2,r19,r29.] = (L~ f1) \/ (L~ f2) ) take f2 ; ::_thesis: ( |[r1,r19]| = f1 /. 1 & |[r1,r19]| = f2 /. 1 & |[r2,r29]| = f1 /. (len f1) & |[r2,r29]| = f2 /. (len f2) & (L~ f1) /\ (L~ f2) = {|[r1,r19]|,|[r2,r29]|} & [.r1,r2,r19,r29.] = (L~ f1) \/ (L~ f2) ) thus ( |[r1,r19]| = f1 /. 1 & |[r1,r19]| = f2 /. 1 & |[r2,r29]| = f1 /. (len f1) & |[r2,r29]| = f2 /. (len f2) ) by A9, A8, FINSEQ_4:18; ::_thesis: ( (L~ f1) /\ (L~ f2) = {|[r1,r19]|,|[r2,r29]|} & [.r1,r2,r19,r29.] = (L~ f1) \/ (L~ f2) ) A11: L~ f2 = (LSeg (|[r2,r29]|,|[r2,r19]|)) \/ (LSeg (|[r2,r19]|,|[r1,r19]|)) by TOPREAL3:16; L~ f1 = (LSeg (|[r1,r19]|,|[r1,r29]|)) \/ (LSeg (|[r1,r29]|,|[r2,r29]|)) by TOPREAL3:16; hence (L~ f1) /\ (L~ f2) = (((LSeg (|[r1,r19]|,|[r1,r29]|)) \/ (LSeg (|[r1,r29]|,|[r2,r29]|))) /\ (LSeg (|[r2,r29]|,|[r2,r19]|))) \/ (((LSeg (|[r1,r19]|,|[r1,r29]|)) \/ (LSeg (|[r1,r29]|,|[r2,r29]|))) /\ (LSeg (|[r2,r19]|,|[r1,r19]|))) by A11, XBOOLE_1:23 .= (((LSeg (|[r1,r29]|,|[r1,r19]|)) \/ (LSeg (|[r2,r29]|,|[r1,r29]|))) /\ (LSeg (|[r2,r19]|,|[r2,r29]|))) \/ {|[r1,r19]|} by A2, A7, A10, A5, A6, TOPREAL3:27 .= {|[r2,r29]|} \/ {|[r1,r19]|} by A1, A7, A3, A5, A4, TOPREAL3:28 .= {|[r1,r19]|,|[r2,r29]|} by ENUMSET1:1 ; ::_thesis: [.r1,r2,r19,r29.] = (L~ f1) \/ (L~ f2) thus [.r1,r2,r19,r29.] = (L~ f1) \/ (L~ f2) by A11, TOPREAL3:16; ::_thesis: verum end; theorem Th56: :: SPPOL_2:56 R^2-unit_square = [.0,1,0,1.] ; registration cluster special_polygonal for Element of bool the carrier of (TOP-REAL 2); existence ex b1 being Subset of (TOP-REAL 2) st b1 is special_polygonal proof take [.0,1,0,1.] ; ::_thesis: [.0,1,0,1.] is special_polygonal thus [.0,1,0,1.] is special_polygonal by Th55; ::_thesis: verum end; end; registration cluster R^2-unit_square -> special_polygonal ; coherence R^2-unit_square is special_polygonal by Th55, Th56; end; registration cluster special_polygonal for Element of bool the carrier of (TOP-REAL 2); existence ex b1 being Subset of (TOP-REAL 2) st b1 is special_polygonal by Th56; cluster special_polygonal -> non empty for Element of bool the carrier of (TOP-REAL 2); coherence for b1 being Subset of (TOP-REAL 2) st b1 is special_polygonal holds not b1 is empty proof let P be Subset of (TOP-REAL 2); ::_thesis: ( P is special_polygonal implies not P is empty ) assume P is special_polygonal ; ::_thesis: not P is empty then ex p1, p2 being Point of (TOP-REAL 2) st ( p1 <> p2 & p1 in P & p2 in P ) by Lm17; hence not P is empty ; ::_thesis: verum end; cluster special_polygonal -> non trivial for Element of bool the carrier of (TOP-REAL 2); coherence for b1 being Subset of (TOP-REAL 2) st b1 is special_polygonal holds not b1 is trivial proof let P be Subset of (TOP-REAL 2); ::_thesis: ( P is special_polygonal implies not P is trivial ) assume P is special_polygonal ; ::_thesis: not P is trivial then ex p1, p2 being Point of (TOP-REAL 2) st ( p1 <> p2 & p1 in P & p2 in P ) by Lm17; hence not P is trivial by ZFMISC_1:def_10; ::_thesis: verum end; end; definition mode Special_polygon_in_R2 is special_polygonal Subset of (TOP-REAL 2); end; theorem Th57: :: SPPOL_2:57 for P being Subset of (TOP-REAL 2) st P is being_S-P_arc holds P is compact proof let P be Subset of (TOP-REAL 2); ::_thesis: ( P is being_S-P_arc implies P is compact ) A1: I[01] is compact by HEINE:4, TOPMETR:20; assume P is being_S-P_arc ; ::_thesis: P is compact then reconsider P = 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 P is compact by COMPTS_1:3; ::_thesis: verum end; registration cluster special_polygonal -> compact for Element of bool the carrier of (TOP-REAL 2); coherence for b1 being Special_polygon_in_R2 holds b1 is compact proof let G be Special_polygon_in_R2; ::_thesis: G is compact 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 = P1, P2 = 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 G is compact by A3, A4, COMPTS_1:10; ::_thesis: verum end; end; theorem Th58: :: SPPOL_2:58 for P being Subset of (TOP-REAL 2) st P is special_polygonal holds for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p1 in P & p2 in P holds p1,p2 split P proof let P be Subset of (TOP-REAL 2); ::_thesis: ( P is special_polygonal implies for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p1 in P & p2 in P holds p1,p2 split P ) assume P is special_polygonal ; ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p1 in P & p2 in P holds p1,p2 split P then ex q1, q2 being Point of (TOP-REAL 2) st q1,q2 split P by Def2; hence for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p1 in P & p2 in P holds p1,p2 split P by Th53; ::_thesis: verum end; theorem :: SPPOL_2:59 for P being Subset of (TOP-REAL 2) st P is special_polygonal holds for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p1 in P & p2 in P holds 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 let P be Subset of (TOP-REAL 2); ::_thesis: ( P is special_polygonal implies for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p1 in P & p2 in P holds 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 ) ) assume A1: P is special_polygonal ; ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st p1 <> p2 & p1 in P & p2 in P holds 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 ) let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( p1 <> p2 & p1 in P & p2 in P implies 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 ) ) assume that A2: p1 <> p2 and A3: p1 in P and A4: p2 in P ; ::_thesis: 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 ) 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; ::_thesis: ex 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 ) take P2 = L~ f2; ::_thesis: ( P1 is_S-P_arc_joining p1,p2 & P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 ) thus P1 is_S-P_arc_joining p1,p2 by A5, A7, TOPREAL4:def_1; ::_thesis: ( P2 is_S-P_arc_joining p1,p2 & P1 /\ P2 = {p1,p2} & P = P1 \/ P2 ) thus P2 is_S-P_arc_joining p1,p2 by A6, A8, TOPREAL4:def_1; ::_thesis: ( P1 /\ P2 = {p1,p2} & P = P1 \/ P2 ) thus ( P1 /\ P2 = {p1,p2} & P = P1 \/ P2 ) by A9, A10; ::_thesis: verum end;