:: TOPREAL3 semantic presentation begin begin theorem Th1: :: TOPREAL3:1 for x, y, z being set holds ( 1 in dom <*x,y,z*> & 2 in dom <*x,y,z*> & 3 in dom <*x,y,z*> ) proof let x, y, z be set ; ::_thesis: ( 1 in dom <*x,y,z*> & 2 in dom <*x,y,z*> & 3 in dom <*x,y,z*> ) len <*x,y,z*> = 3 by FINSEQ_1:45; hence ( 1 in dom <*x,y,z*> & 2 in dom <*x,y,z*> & 3 in dom <*x,y,z*> ) by FINSEQ_3:25; ::_thesis: verum end; theorem Th2: :: TOPREAL3:2 for p1, p2 being Point of (TOP-REAL 2) holds ( (p1 + p2) `1 = (p1 `1) + (p2 `1) & (p1 + p2) `2 = (p1 `2) + (p2 `2) ) proof let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( (p1 + p2) `1 = (p1 `1) + (p2 `1) & (p1 + p2) `2 = (p1 `2) + (p2 `2) ) p1 + p2 = |[((p1 `1) + (p2 `1)),((p1 `2) + (p2 `2))]| by EUCLID:55; hence ( (p1 + p2) `1 = (p1 `1) + (p2 `1) & (p1 + p2) `2 = (p1 `2) + (p2 `2) ) by EUCLID:52; ::_thesis: verum end; theorem :: TOPREAL3:3 for p1, p2 being Point of (TOP-REAL 2) holds ( (p1 - p2) `1 = (p1 `1) - (p2 `1) & (p1 - p2) `2 = (p1 `2) - (p2 `2) ) proof let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( (p1 - p2) `1 = (p1 `1) - (p2 `1) & (p1 - p2) `2 = (p1 `2) - (p2 `2) ) p1 - p2 = |[((p1 `1) - (p2 `1)),((p1 `2) - (p2 `2))]| by EUCLID:61; hence ( (p1 - p2) `1 = (p1 `1) - (p2 `1) & (p1 - p2) `2 = (p1 `2) - (p2 `2) ) by EUCLID:52; ::_thesis: verum end; theorem Th4: :: TOPREAL3:4 for p being Point of (TOP-REAL 2) for r being real number holds ( (r * p) `1 = r * (p `1) & (r * p) `2 = r * (p `2) ) proof let p be Point of (TOP-REAL 2); ::_thesis: for r being real number holds ( (r * p) `1 = r * (p `1) & (r * p) `2 = r * (p `2) ) let r be real number ; ::_thesis: ( (r * p) `1 = r * (p `1) & (r * p) `2 = r * (p `2) ) r * p = |[(r * (p `1)),(r * (p `2))]| by EUCLID:57; hence ( (r * p) `1 = r * (p `1) & (r * p) `2 = r * (p `2) ) by EUCLID:52; ::_thesis: verum end; theorem Th5: :: TOPREAL3:5 for p1, p2 being Point of (TOP-REAL 2) for r1, s1, r2, s2 being real number st p1 = <*r1,s1*> & p2 = <*r2,s2*> holds ( p1 + p2 = <*(r1 + r2),(s1 + s2)*> & p1 - p2 = <*(r1 - r2),(s1 - s2)*> ) proof let p1, p2 be Point of (TOP-REAL 2); ::_thesis: for r1, s1, r2, s2 being real number st p1 = <*r1,s1*> & p2 = <*r2,s2*> holds ( p1 + p2 = <*(r1 + r2),(s1 + s2)*> & p1 - p2 = <*(r1 - r2),(s1 - s2)*> ) let r1, s1, r2, s2 be real number ; ::_thesis: ( p1 = <*r1,s1*> & p2 = <*r2,s2*> implies ( p1 + p2 = <*(r1 + r2),(s1 + s2)*> & p1 - p2 = <*(r1 - r2),(s1 - s2)*> ) ) A1: ( |[r1,s1]| `1 = r1 & |[r1,s1]| `2 = s1 ) by EUCLID:52; A2: ( |[r2,s2]| `1 = r2 & |[r2,s2]| `2 = s2 ) by EUCLID:52; assume ( p1 = <*r1,s1*> & p2 = <*r2,s2*> ) ; ::_thesis: ( p1 + p2 = <*(r1 + r2),(s1 + s2)*> & p1 - p2 = <*(r1 - r2),(s1 - s2)*> ) hence ( p1 + p2 = <*(r1 + r2),(s1 + s2)*> & p1 - p2 = <*(r1 - r2),(s1 - s2)*> ) by A1, A2, EUCLID:55, EUCLID:61; ::_thesis: verum end; theorem Th6: :: TOPREAL3:6 for p, q being Point of (TOP-REAL 2) st p `1 = q `1 & p `2 = q `2 holds p = q proof let p, q be Point of (TOP-REAL 2); ::_thesis: ( p `1 = q `1 & p `2 = q `2 implies p = q ) assume ( p `1 = q `1 & p `2 = q `2 ) ; ::_thesis: p = q hence p = |[(q `1),(q `2)]| by EUCLID:53 .= q by EUCLID:53 ; ::_thesis: verum end; theorem Th7: :: TOPREAL3:7 for p1, p2 being Point of (TOP-REAL 2) for u1, u2 being Point of (Euclid 2) st u1 = p1 & u2 = p2 holds (Pitag_dist 2) . (u1,u2) = sqrt ((((p1 `1) - (p2 `1)) ^2) + (((p1 `2) - (p2 `2)) ^2)) proof let p1, p2 be Point of (TOP-REAL 2); ::_thesis: for u1, u2 being Point of (Euclid 2) st u1 = p1 & u2 = p2 holds (Pitag_dist 2) . (u1,u2) = sqrt ((((p1 `1) - (p2 `1)) ^2) + (((p1 `2) - (p2 `2)) ^2)) let u1, u2 be Point of (Euclid 2); ::_thesis: ( u1 = p1 & u2 = p2 implies (Pitag_dist 2) . (u1,u2) = sqrt ((((p1 `1) - (p2 `1)) ^2) + (((p1 `2) - (p2 `2)) ^2)) ) assume that A1: u1 = p1 and A2: u2 = p2 ; ::_thesis: (Pitag_dist 2) . (u1,u2) = sqrt ((((p1 `1) - (p2 `1)) ^2) + (((p1 `2) - (p2 `2)) ^2)) reconsider v1 = u1, v2 = u2 as Element of REAL 2 ; ( p1 = |[(p1 `1),(p1 `2)]| & u2 = <*(p2 `1),(p2 `2)*> ) by A2, EUCLID:53; then v1 - v2 = <*(diffreal . ((p1 `1),(p2 `1))),(diffreal . ((p1 `2),(p2 `2)))*> by A1, FINSEQ_2:75 .= <*((p1 `1) - (p2 `1)),(diffreal . ((p1 `2),(p2 `2)))*> by BINOP_2:def_10 .= <*((p1 `1) - (p2 `1)),((p1 `2) - (p2 `2))*> by BINOP_2:def_10 ; then abs (v1 - v2) = <*(absreal . ((p1 `1) - (p2 `1))),(absreal . ((p1 `2) - (p2 `2)))*> by FINSEQ_2:36 .= <*(abs ((p1 `1) - (p2 `1))),(absreal . ((p1 `2) - (p2 `2)))*> by EUCLID:def_2 .= <*(abs ((p1 `1) - (p2 `1))),(abs ((p1 `2) - (p2 `2)))*> by EUCLID:def_2 ; then A3: sqr (abs (v1 - v2)) = <*(sqrreal . (abs ((p1 `1) - (p2 `1)))),(sqrreal . (abs ((p1 `2) - (p2 `2))))*> by FINSEQ_2:36 .= <*((abs ((p1 `1) - (p2 `1))) ^2),(sqrreal . (abs ((p1 `2) - (p2 `2))))*> by RVSUM_1:def_2 .= <*((abs ((p1 `1) - (p2 `1))) ^2),((abs ((p1 `2) - (p2 `2))) ^2)*> by RVSUM_1:def_2 .= <*(((p1 `1) - (p2 `1)) ^2),((abs ((p1 `2) - (p2 `2))) ^2)*> by COMPLEX1:75 .= <*(((p1 `1) - (p2 `1)) ^2),(((p1 `2) - (p2 `2)) ^2)*> by COMPLEX1:75 ; (Pitag_dist 2) . (u1,u2) = |.(v1 - v2).| by EUCLID:def_6 .= sqrt (Sum (sqr (abs (v1 - v2)))) by EUCLID:25 ; hence (Pitag_dist 2) . (u1,u2) = sqrt ((((p1 `1) - (p2 `1)) ^2) + (((p1 `2) - (p2 `2)) ^2)) by A3, RVSUM_1:77; ::_thesis: verum end; theorem Th8: :: TOPREAL3:8 for n being Nat holds the carrier of (TOP-REAL n) = the carrier of (Euclid n) by EUCLID:22; theorem Th9: :: TOPREAL3:9 for r1, s1, r being real number st r1 <= s1 holds { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = r & r1 <= p1 `2 & p1 `2 <= s1 ) } = LSeg (|[r,r1]|,|[r,s1]|) proof let r1, s1, r be real number ; ::_thesis: ( r1 <= s1 implies { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = r & r1 <= p1 `2 & p1 `2 <= s1 ) } = LSeg (|[r,r1]|,|[r,s1]|) ) set L = { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `1 = r & r1 <= p3 `2 & p3 `2 <= s1 ) } ; set p = |[r,r1]|; set q = |[r,s1]|; A1: |[r,r1]| `1 = r by EUCLID:52; assume A2: r1 <= s1 ; ::_thesis: { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = r & r1 <= p1 `2 & p1 `2 <= s1 ) } = LSeg (|[r,r1]|,|[r,s1]|) then A3: s1 - r1 >= r1 - r1 by XREAL_1:13; A4: |[r,s1]| `2 = s1 by EUCLID:52; A5: |[r,r1]| `2 = r1 by EUCLID:52; A6: |[r,s1]| `1 = r by EUCLID:52; thus { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `1 = r & r1 <= p3 `2 & p3 `2 <= s1 ) } c= LSeg (|[r,r1]|,|[r,s1]|) :: according to XBOOLE_0:def_10 ::_thesis: LSeg (|[r,r1]|,|[r,s1]|) c= { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = r & r1 <= p1 `2 & p1 `2 <= s1 ) } proof percases ( r1 = s1 or r1 < s1 ) by A2, XXREAL_0:1; supposeA7: r1 = s1 ; ::_thesis: { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `1 = r & r1 <= p3 `2 & p3 `2 <= s1 ) } c= LSeg (|[r,r1]|,|[r,s1]|) { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `1 = r & r1 <= p3 `2 & p3 `2 <= s1 ) } c= {|[r,r1]|} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `1 = r & r1 <= p3 `2 & p3 `2 <= s1 ) } or x in {|[r,r1]|} ) assume x in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `1 = r & r1 <= p3 `2 & p3 `2 <= s1 ) } ; ::_thesis: x in {|[r,r1]|} then consider p2 being Point of (TOP-REAL 2) such that A8: x = p2 and A9: p2 `1 = r and A10: ( r1 <= p2 `2 & p2 `2 <= s1 ) ; |[r,r1]| `2 = p2 `2 by A5, A7, A10, XXREAL_0:1; then p2 = |[r,r1]| by A1, A9, Th6; hence x in {|[r,r1]|} by A8, TARSKI:def_1; ::_thesis: verum end; hence { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `1 = r & r1 <= p3 `2 & p3 `2 <= s1 ) } c= LSeg (|[r,r1]|,|[r,s1]|) by A7, RLTOPSP1:70; ::_thesis: verum end; supposeA11: r1 < s1 ; ::_thesis: { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `1 = r & r1 <= p3 `2 & p3 `2 <= s1 ) } c= LSeg (|[r,r1]|,|[r,s1]|) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `1 = r & r1 <= p3 `2 & p3 `2 <= s1 ) } or x in LSeg (|[r,r1]|,|[r,s1]|) ) assume x in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `1 = r & r1 <= p3 `2 & p3 `2 <= s1 ) } ; ::_thesis: x in LSeg (|[r,r1]|,|[r,s1]|) then consider p2 being Point of (TOP-REAL 2) such that A12: x = p2 and A13: p2 `1 = r and A14: r1 <= p2 `2 and A15: p2 `2 <= s1 ; set t = p2 `2 ; set l = ((p2 `2) - r1) / (s1 - r1); A16: s1 - r1 > 0 by A11, XREAL_1:50; then A17: 1 - (((p2 `2) - r1) / (s1 - r1)) = ((1 * (s1 - r1)) - ((p2 `2) - r1)) / (s1 - r1) by XCMPLX_1:127 .= (s1 - (p2 `2)) / (s1 - r1) ; (p2 `2) - r1 <= s1 - r1 by A15, XREAL_1:9; then ((p2 `2) - r1) / (s1 - r1) <= (s1 - r1) / (s1 - r1) by A16, XREAL_1:72; then A18: ((p2 `2) - r1) / (s1 - r1) <= 1 by A16, XCMPLX_1:60; A19: (((1 - (((p2 `2) - r1) / (s1 - r1))) * |[r,r1]|) + ((((p2 `2) - r1) / (s1 - r1)) * |[r,s1]|)) `1 = (((1 - (((p2 `2) - r1) / (s1 - r1))) * |[r,r1]|) `1) + (((((p2 `2) - r1) / (s1 - r1)) * |[r,s1]|) `1) by Th2 .= ((1 - (((p2 `2) - r1) / (s1 - r1))) * (|[r,r1]| `1)) + (((((p2 `2) - r1) / (s1 - r1)) * |[r,s1]|) `1) by Th4 .= ((1 - (((p2 `2) - r1) / (s1 - r1))) * r) + ((((p2 `2) - r1) / (s1 - r1)) * r) by A1, A6, Th4 .= p2 `1 by A13 ; (((1 - (((p2 `2) - r1) / (s1 - r1))) * |[r,r1]|) + ((((p2 `2) - r1) / (s1 - r1)) * |[r,s1]|)) `2 = (((1 - (((p2 `2) - r1) / (s1 - r1))) * |[r,r1]|) `2) + (((((p2 `2) - r1) / (s1 - r1)) * |[r,s1]|) `2) by Th2 .= ((1 - (((p2 `2) - r1) / (s1 - r1))) * (|[r,r1]| `2)) + (((((p2 `2) - r1) / (s1 - r1)) * |[r,s1]|) `2) by Th4 .= ((1 - (((p2 `2) - r1) / (s1 - r1))) * (|[r,r1]| `2)) + ((((p2 `2) - r1) / (s1 - r1)) * (|[r,s1]| `2)) by Th4 .= (((s1 - (p2 `2)) * (|[r,r1]| `2)) / (s1 - r1)) + ((((p2 `2) - r1) / (s1 - r1)) * (|[r,s1]| `2)) by A17, XCMPLX_1:74 .= (((s1 - (p2 `2)) * (|[r,r1]| `2)) / (s1 - r1)) + ((((p2 `2) - r1) * (|[r,s1]| `2)) / (s1 - r1)) by XCMPLX_1:74 .= (((s1 * r1) - ((p2 `2) * r1)) + (((p2 `2) - r1) * s1)) / (s1 - r1) by A5, A4, XCMPLX_1:62 .= ((p2 `2) * (s1 - r1)) / (s1 - r1) .= (p2 `2) * ((s1 - r1) / (s1 - r1)) by XCMPLX_1:74 .= (p2 `2) * 1 by A16, XCMPLX_1:60 .= p2 `2 ; then A20: p2 = ((1 - (((p2 `2) - r1) / (s1 - r1))) * |[r,r1]|) + ((((p2 `2) - r1) / (s1 - r1)) * |[r,s1]|) by A19, Th6; r1 - r1 <= (p2 `2) - r1 by A14, XREAL_1:9; hence x in LSeg (|[r,r1]|,|[r,s1]|) by A16, A12, A18, A20; ::_thesis: verum end; end; end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LSeg (|[r,r1]|,|[r,s1]|) or x in { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = r & r1 <= p1 `2 & p1 `2 <= s1 ) } ) assume x in LSeg (|[r,r1]|,|[r,s1]|) ; ::_thesis: x in { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = r & r1 <= p1 `2 & p1 `2 <= s1 ) } then consider lambda being Real such that A21: ((1 - lambda) * |[r,r1]|) + (lambda * |[r,s1]|) = x and A22: 0 <= lambda and A23: lambda <= 1 ; A24: r1 + 0 <= r1 + (lambda * (s1 - r1)) by A3, A22, XREAL_1:7; lambda * (s1 - r1) <= 1 * (s1 - r1) by A3, A23, XREAL_1:64; then A25: r1 + (lambda * (s1 - r1)) <= (s1 - r1) + r1 by XREAL_1:7; set p2 = ((1 - lambda) * |[r,r1]|) + (lambda * |[r,s1]|); A26: (((1 - lambda) * |[r,r1]|) + (lambda * |[r,s1]|)) `2 = (((1 - lambda) * |[r,r1]|) `2) + ((lambda * |[r,s1]|) `2) by Th2 .= ((1 - lambda) * (|[r,r1]| `2)) + ((lambda * |[r,s1]|) `2) by Th4 .= ((1 * r1) - (lambda * r1)) + (lambda * s1) by A5, A4, Th4 .= r1 + (lambda * (s1 - r1)) ; (((1 - lambda) * |[r,r1]|) + (lambda * |[r,s1]|)) `1 = (((1 - lambda) * |[r,r1]|) `1) + ((lambda * |[r,s1]|) `1) by Th2 .= ((1 - lambda) * (|[r,r1]| `1)) + ((lambda * |[r,s1]|) `1) by Th4 .= ((1 - lambda) * r) + (lambda * r) by A1, A6, Th4 .= 1 * r ; hence x in { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = r & r1 <= p1 `2 & p1 `2 <= s1 ) } by A21, A26, A24, A25; ::_thesis: verum end; theorem Th10: :: TOPREAL3:10 for r1, s1, r being real number st r1 <= s1 holds { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `2 = r & r1 <= p1 `1 & p1 `1 <= s1 ) } = LSeg (|[r1,r]|,|[s1,r]|) proof let r1, s1, r be real number ; ::_thesis: ( r1 <= s1 implies { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `2 = r & r1 <= p1 `1 & p1 `1 <= s1 ) } = LSeg (|[r1,r]|,|[s1,r]|) ) set L = { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `2 = r & r1 <= p3 `1 & p3 `1 <= s1 ) } ; set p = |[r1,r]|; set q = |[s1,r]|; A1: |[r1,r]| `1 = r1 by EUCLID:52; assume A2: r1 <= s1 ; ::_thesis: { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `2 = r & r1 <= p1 `1 & p1 `1 <= s1 ) } = LSeg (|[r1,r]|,|[s1,r]|) then A3: s1 - r1 >= r1 - r1 by XREAL_1:13; A4: |[s1,r]| `2 = r by EUCLID:52; A5: |[r1,r]| `2 = r by EUCLID:52; A6: |[s1,r]| `1 = s1 by EUCLID:52; thus { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `2 = r & r1 <= p3 `1 & p3 `1 <= s1 ) } c= LSeg (|[r1,r]|,|[s1,r]|) :: according to XBOOLE_0:def_10 ::_thesis: LSeg (|[r1,r]|,|[s1,r]|) c= { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `2 = r & r1 <= p1 `1 & p1 `1 <= s1 ) } proof percases ( r1 = s1 or r1 < s1 ) by A2, XXREAL_0:1; supposeA7: r1 = s1 ; ::_thesis: { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `2 = r & r1 <= p3 `1 & p3 `1 <= s1 ) } c= LSeg (|[r1,r]|,|[s1,r]|) { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `2 = r & r1 <= p3 `1 & p3 `1 <= s1 ) } c= {|[r1,r]|} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `2 = r & r1 <= p3 `1 & p3 `1 <= s1 ) } or x in {|[r1,r]|} ) assume x in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `2 = r & r1 <= p3 `1 & p3 `1 <= s1 ) } ; ::_thesis: x in {|[r1,r]|} then consider p2 being Point of (TOP-REAL 2) such that A8: x = p2 and A9: p2 `2 = r and A10: ( r1 <= p2 `1 & p2 `1 <= s1 ) ; |[r1,r]| `1 = p2 `1 by A1, A7, A10, XXREAL_0:1; then p2 = |[r1,r]| by A5, A9, Th6; hence x in {|[r1,r]|} by A8, TARSKI:def_1; ::_thesis: verum end; hence { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `2 = r & r1 <= p3 `1 & p3 `1 <= s1 ) } c= LSeg (|[r1,r]|,|[s1,r]|) by A7, RLTOPSP1:70; ::_thesis: verum end; supposeA11: r1 < s1 ; ::_thesis: { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `2 = r & r1 <= p3 `1 & p3 `1 <= s1 ) } c= LSeg (|[r1,r]|,|[s1,r]|) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `2 = r & r1 <= p3 `1 & p3 `1 <= s1 ) } or x in LSeg (|[r1,r]|,|[s1,r]|) ) assume x in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `2 = r & r1 <= p3 `1 & p3 `1 <= s1 ) } ; ::_thesis: x in LSeg (|[r1,r]|,|[s1,r]|) then consider p2 being Point of (TOP-REAL 2) such that A12: x = p2 and A13: p2 `2 = r and A14: r1 <= p2 `1 and A15: p2 `1 <= s1 ; set t = p2 `1 ; set l = ((p2 `1) - r1) / (s1 - r1); A16: s1 - r1 > 0 by A11, XREAL_1:50; then A17: 1 - (((p2 `1) - r1) / (s1 - r1)) = ((1 * (s1 - r1)) - ((p2 `1) - r1)) / (s1 - r1) by XCMPLX_1:127 .= (s1 - (p2 `1)) / (s1 - r1) ; (p2 `1) - r1 <= s1 - r1 by A15, XREAL_1:9; then ((p2 `1) - r1) / (s1 - r1) <= (s1 - r1) / (s1 - r1) by A16, XREAL_1:72; then A18: ((p2 `1) - r1) / (s1 - r1) <= 1 by A16, XCMPLX_1:60; A19: (((1 - (((p2 `1) - r1) / (s1 - r1))) * |[r1,r]|) + ((((p2 `1) - r1) / (s1 - r1)) * |[s1,r]|)) `2 = (((1 - (((p2 `1) - r1) / (s1 - r1))) * |[r1,r]|) `2) + (((((p2 `1) - r1) / (s1 - r1)) * |[s1,r]|) `2) by Th2 .= ((1 - (((p2 `1) - r1) / (s1 - r1))) * (|[r1,r]| `2)) + (((((p2 `1) - r1) / (s1 - r1)) * |[s1,r]|) `2) by Th4 .= ((1 - (((p2 `1) - r1) / (s1 - r1))) * r) + ((((p2 `1) - r1) / (s1 - r1)) * r) by A5, A4, Th4 .= p2 `2 by A13 ; (((1 - (((p2 `1) - r1) / (s1 - r1))) * |[r1,r]|) + ((((p2 `1) - r1) / (s1 - r1)) * |[s1,r]|)) `1 = (((1 - (((p2 `1) - r1) / (s1 - r1))) * |[r1,r]|) `1) + (((((p2 `1) - r1) / (s1 - r1)) * |[s1,r]|) `1) by Th2 .= ((1 - (((p2 `1) - r1) / (s1 - r1))) * (|[r1,r]| `1)) + (((((p2 `1) - r1) / (s1 - r1)) * |[s1,r]|) `1) by Th4 .= ((1 - (((p2 `1) - r1) / (s1 - r1))) * (|[r1,r]| `1)) + ((((p2 `1) - r1) / (s1 - r1)) * (|[s1,r]| `1)) by Th4 .= (((s1 - (p2 `1)) * (|[r1,r]| `1)) / (s1 - r1)) + ((((p2 `1) - r1) / (s1 - r1)) * (|[s1,r]| `1)) by A17, XCMPLX_1:74 .= (((s1 - (p2 `1)) * (|[r1,r]| `1)) / (s1 - r1)) + ((((p2 `1) - r1) * (|[s1,r]| `1)) / (s1 - r1)) by XCMPLX_1:74 .= (((s1 * r1) - ((p2 `1) * r1)) + (((p2 `1) - r1) * s1)) / (s1 - r1) by A1, A6, XCMPLX_1:62 .= ((p2 `1) * (s1 - r1)) / (s1 - r1) .= (p2 `1) * ((s1 - r1) / (s1 - r1)) by XCMPLX_1:74 .= (p2 `1) * 1 by A16, XCMPLX_1:60 .= p2 `1 ; then A20: p2 = ((1 - (((p2 `1) - r1) / (s1 - r1))) * |[r1,r]|) + ((((p2 `1) - r1) / (s1 - r1)) * |[s1,r]|) by A19, Th6; r1 - r1 <= (p2 `1) - r1 by A14, XREAL_1:9; hence x in LSeg (|[r1,r]|,|[s1,r]|) by A16, A12, A18, A20; ::_thesis: verum end; end; end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LSeg (|[r1,r]|,|[s1,r]|) or x in { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `2 = r & r1 <= p1 `1 & p1 `1 <= s1 ) } ) assume x in LSeg (|[r1,r]|,|[s1,r]|) ; ::_thesis: x in { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `2 = r & r1 <= p1 `1 & p1 `1 <= s1 ) } then consider lambda being Real such that A21: ((1 - lambda) * |[r1,r]|) + (lambda * |[s1,r]|) = x and A22: 0 <= lambda and A23: lambda <= 1 ; A24: r1 + 0 <= r1 + (lambda * (s1 - r1)) by A3, A22, XREAL_1:7; lambda * (s1 - r1) <= 1 * (s1 - r1) by A3, A23, XREAL_1:64; then A25: r1 + (lambda * (s1 - r1)) <= (s1 - r1) + r1 by XREAL_1:7; set p2 = ((1 - lambda) * |[r1,r]|) + (lambda * |[s1,r]|); A26: (((1 - lambda) * |[r1,r]|) + (lambda * |[s1,r]|)) `1 = (((1 - lambda) * |[r1,r]|) `1) + ((lambda * |[s1,r]|) `1) by Th2 .= ((1 - lambda) * (|[r1,r]| `1)) + ((lambda * |[s1,r]|) `1) by Th4 .= ((1 * r1) - (lambda * r1)) + (lambda * s1) by A1, A6, Th4 .= r1 + (lambda * (s1 - r1)) ; (((1 - lambda) * |[r1,r]|) + (lambda * |[s1,r]|)) `2 = (((1 - lambda) * |[r1,r]|) `2) + ((lambda * |[s1,r]|) `2) by Th2 .= ((1 - lambda) * (|[r1,r]| `2)) + ((lambda * |[s1,r]|) `2) by Th4 .= ((1 - lambda) * r) + (lambda * r) by A5, A4, Th4 .= r ; hence x in { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `2 = r & r1 <= p1 `1 & p1 `1 <= s1 ) } by A21, A26, A24, A25; ::_thesis: verum end; theorem :: TOPREAL3:11 for p being Point of (TOP-REAL 2) for r, r1, s1 being real number st p in LSeg (|[r,r1]|,|[r,s1]|) holds p `1 = r proof let p be Point of (TOP-REAL 2); ::_thesis: for r, r1, s1 being real number st p in LSeg (|[r,r1]|,|[r,s1]|) holds p `1 = r let r, r1, s1 be real number ; ::_thesis: ( p in LSeg (|[r,r1]|,|[r,s1]|) implies p `1 = r ) assume A1: p in LSeg (|[r,r1]|,|[r,s1]|) ; ::_thesis: p `1 = r percases ( r1 < s1 or r1 = s1 or r1 > s1 ) by XXREAL_0:1; suppose r1 < s1 ; ::_thesis: p `1 = r then LSeg (|[r,r1]|,|[r,s1]|) = { q where q is Point of (TOP-REAL 2) : ( q `1 = r & r1 <= q `2 & q `2 <= s1 ) } by Th9; then ex p1 being Point of (TOP-REAL 2) st ( p1 = p & p1 `1 = r & r1 <= p1 `2 & p1 `2 <= s1 ) by A1; hence p `1 = r ; ::_thesis: verum end; suppose r1 = s1 ; ::_thesis: p `1 = r then p in {|[r,r1]|} by A1, RLTOPSP1:70; then p = |[r,r1]| by TARSKI:def_1; hence p `1 = r by EUCLID:52; ::_thesis: verum end; suppose r1 > s1 ; ::_thesis: p `1 = r then LSeg (|[r,r1]|,|[r,s1]|) = { q where q is Point of (TOP-REAL 2) : ( q `1 = r & s1 <= q `2 & q `2 <= r1 ) } by Th9; then ex p1 being Point of (TOP-REAL 2) st ( p1 = p & p1 `1 = r & s1 <= p1 `2 & p1 `2 <= r1 ) by A1; hence p `1 = r ; ::_thesis: verum end; end; end; theorem :: TOPREAL3:12 for p being Point of (TOP-REAL 2) for r1, r, s1 being real number st p in LSeg (|[r1,r]|,|[s1,r]|) holds p `2 = r proof let p be Point of (TOP-REAL 2); ::_thesis: for r1, r, s1 being real number st p in LSeg (|[r1,r]|,|[s1,r]|) holds p `2 = r let r1, r, s1 be real number ; ::_thesis: ( p in LSeg (|[r1,r]|,|[s1,r]|) implies p `2 = r ) assume A1: p in LSeg (|[r1,r]|,|[s1,r]|) ; ::_thesis: p `2 = r percases ( r1 < s1 or r1 = s1 or r1 > s1 ) by XXREAL_0:1; suppose r1 < s1 ; ::_thesis: p `2 = r then LSeg (|[r1,r]|,|[s1,r]|) = { q where q is Point of (TOP-REAL 2) : ( q `2 = r & r1 <= q `1 & q `1 <= s1 ) } by Th10; then ex p1 being Point of (TOP-REAL 2) st ( p1 = p & p1 `2 = r & r1 <= p1 `1 & p1 `1 <= s1 ) by A1; hence p `2 = r ; ::_thesis: verum end; suppose r1 = s1 ; ::_thesis: p `2 = r then p in {|[r1,r]|} by A1, RLTOPSP1:70; then p = |[r1,r]| by TARSKI:def_1; hence p `2 = r by EUCLID:52; ::_thesis: verum end; suppose r1 > s1 ; ::_thesis: p `2 = r then LSeg (|[r1,r]|,|[s1,r]|) = { q where q is Point of (TOP-REAL 2) : ( q `2 = r & s1 <= q `1 & q `1 <= r1 ) } by Th10; then ex p1 being Point of (TOP-REAL 2) st ( p1 = p & p1 `2 = r & s1 <= p1 `1 & p1 `1 <= r1 ) by A1; hence p `2 = r ; ::_thesis: verum end; end; end; theorem :: TOPREAL3:13 for p, q being Point of (TOP-REAL 2) st p `1 <> q `1 & p `2 = q `2 holds |[(((p `1) + (q `1)) / 2),(p `2)]| in LSeg (p,q) proof let p, q be Point of (TOP-REAL 2); ::_thesis: ( p `1 <> q `1 & p `2 = q `2 implies |[(((p `1) + (q `1)) / 2),(p `2)]| in LSeg (p,q) ) set p1 = |[(((p `1) + (q `1)) / 2),(p `2)]|; assume that A1: p `1 <> q `1 and A2: p `2 = q `2 ; ::_thesis: |[(((p `1) + (q `1)) / 2),(p `2)]| in LSeg (p,q) A3: ( p = |[(p `1),(p `2)]| & q = |[(q `1),(p `2)]| ) by A2, EUCLID:53; A4: ( |[(((p `1) + (q `1)) / 2),(p `2)]| `1 = ((p `1) + (q `1)) / 2 & |[(((p `1) + (q `1)) / 2),(p `2)]| `2 = p `2 ) by EUCLID:52; percases ( p `1 < q `1 or p `1 > q `1 ) by A1, XXREAL_0:1; supposeA5: p `1 < q `1 ; ::_thesis: |[(((p `1) + (q `1)) / 2),(p `2)]| in LSeg (p,q) then ( p `1 <= ((p `1) + (q `1)) / 2 & ((p `1) + (q `1)) / 2 <= q `1 ) by XREAL_1:226; then |[(((p `1) + (q `1)) / 2),(p `2)]| in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = p `2 & p `1 <= p2 `1 & p2 `1 <= q `1 ) } by A4; hence |[(((p `1) + (q `1)) / 2),(p `2)]| in LSeg (p,q) by A3, A5, Th10; ::_thesis: verum end; supposeA6: p `1 > q `1 ; ::_thesis: |[(((p `1) + (q `1)) / 2),(p `2)]| in LSeg (p,q) then ( q `1 <= ((p `1) + (q `1)) / 2 & ((p `1) + (q `1)) / 2 <= p `1 ) by XREAL_1:226; then |[(((p `1) + (q `1)) / 2),(p `2)]| in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = p `2 & q `1 <= p2 `1 & p2 `1 <= p `1 ) } by A4; hence |[(((p `1) + (q `1)) / 2),(p `2)]| in LSeg (p,q) by A3, A6, Th10; ::_thesis: verum end; end; end; theorem :: TOPREAL3:14 for p, q being Point of (TOP-REAL 2) st p `1 = q `1 & p `2 <> q `2 holds |[(p `1),(((p `2) + (q `2)) / 2)]| in LSeg (p,q) proof let p, q be Point of (TOP-REAL 2); ::_thesis: ( p `1 = q `1 & p `2 <> q `2 implies |[(p `1),(((p `2) + (q `2)) / 2)]| in LSeg (p,q) ) set p1 = |[(p `1),(((p `2) + (q `2)) / 2)]|; assume that A1: p `1 = q `1 and A2: p `2 <> q `2 ; ::_thesis: |[(p `1),(((p `2) + (q `2)) / 2)]| in LSeg (p,q) A3: ( p = |[(p `1),(p `2)]| & q = |[(p `1),(q `2)]| ) by A1, EUCLID:53; A4: ( |[(p `1),(((p `2) + (q `2)) / 2)]| `1 = p `1 & |[(p `1),(((p `2) + (q `2)) / 2)]| `2 = ((p `2) + (q `2)) / 2 ) by EUCLID:52; percases ( p `2 < q `2 or p `2 > q `2 ) by A2, XXREAL_0:1; supposeA5: p `2 < q `2 ; ::_thesis: |[(p `1),(((p `2) + (q `2)) / 2)]| in LSeg (p,q) then ( p `2 <= ((p `2) + (q `2)) / 2 & ((p `2) + (q `2)) / 2 <= q `2 ) by XREAL_1:226; then |[(p `1),(((p `2) + (q `2)) / 2)]| in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = p `1 & p `2 <= p2 `2 & p2 `2 <= q `2 ) } by A4; hence |[(p `1),(((p `2) + (q `2)) / 2)]| in LSeg (p,q) by A3, A5, Th9; ::_thesis: verum end; supposeA6: p `2 > q `2 ; ::_thesis: |[(p `1),(((p `2) + (q `2)) / 2)]| in LSeg (p,q) then ( q `2 <= ((p `2) + (q `2)) / 2 & ((p `2) + (q `2)) / 2 <= p `2 ) by XREAL_1:226; then |[(p `1),(((p `2) + (q `2)) / 2)]| in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = p `1 & q `2 <= p2 `2 & p2 `2 <= p `2 ) } by A4; hence |[(p `1),(((p `2) + (q `2)) / 2)]| in LSeg (p,q) by A3, A6, Th9; ::_thesis: verum end; end; end; theorem Th15: :: TOPREAL3:15 for p, p1, q being Point of (TOP-REAL 2) for f being FinSequence of (TOP-REAL 2) for i, j being Nat st f = <*p,p1,q*> & i <> 0 & j > i + 1 holds LSeg (f,j) = {} proof let p, p1, q be Point of (TOP-REAL 2); ::_thesis: for f being FinSequence of (TOP-REAL 2) for i, j being Nat st f = <*p,p1,q*> & i <> 0 & j > i + 1 holds LSeg (f,j) = {} let f be FinSequence of (TOP-REAL 2); ::_thesis: for i, j being Nat st f = <*p,p1,q*> & i <> 0 & j > i + 1 holds LSeg (f,j) = {} let i, j be Nat; ::_thesis: ( f = <*p,p1,q*> & i <> 0 & j > i + 1 implies LSeg (f,j) = {} ) assume that A1: f = <*p,p1,q*> and A2: i <> 0 and A3: j > i + 1 ; ::_thesis: LSeg (f,j) = {} i >= 0 + 1 by A2, NAT_1:13; then 1 + i >= 1 + 1 by XREAL_1:7; then j > 2 by A3, XXREAL_0:2; then j >= 2 + 1 by NAT_1:13; then A4: j + 1 > 3 by NAT_1:13; len f = 3 by A1, FINSEQ_1:45; hence LSeg (f,j) = {} by A4, TOPREAL1:def_3; ::_thesis: verum end; theorem :: TOPREAL3:16 for p1, p2, p3 being Point of (TOP-REAL 2) for f being FinSequence of (TOP-REAL 2) st f = <*p1,p2,p3*> holds L~ f = (LSeg (p1,p2)) \/ (LSeg (p2,p3)) proof let p1, p2, p3 be Point of (TOP-REAL 2); ::_thesis: for f being FinSequence of (TOP-REAL 2) st f = <*p1,p2,p3*> holds L~ f = (LSeg (p1,p2)) \/ (LSeg (p2,p3)) let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f = <*p1,p2,p3*> implies L~ f = (LSeg (p1,p2)) \/ (LSeg (p2,p3)) ) set M = { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ; assume A1: f = <*p1,p2,p3*> ; ::_thesis: L~ f = (LSeg (p1,p2)) \/ (LSeg (p2,p3)) then A2: len f = 2 + 1 by FINSEQ_1:45; A3: f /. 3 = p3 by A1, FINSEQ_4:18; A4: f /. 1 = p1 by A1, FINSEQ_4:18; A5: f /. 2 = p2 by A1, FINSEQ_4:18; A6: 1 + 1 in dom f by A1, Th1; { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } = {(LSeg (p1,p2)),(LSeg (p2,p3))} proof thus { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } c= {(LSeg (p1,p2)),(LSeg (p2,p3))} :: according to XBOOLE_0:def_10 ::_thesis: {(LSeg (p1,p2)),(LSeg (p2,p3))} c= { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } or x in {(LSeg (p1,p2)),(LSeg (p2,p3))} ) assume x in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ; ::_thesis: x in {(LSeg (p1,p2)),(LSeg (p2,p3))} then consider j being Element of NAT such that A7: x = LSeg (f,j) and A8: 1 <= j and A9: j + 1 <= len f ; A10: j <= 2 by A2, A9, XREAL_1:6; percases ( j = 1 or j = 2 ) by A8, A10, NAT_1:26; suppose j = 1 ; ::_thesis: x in {(LSeg (p1,p2)),(LSeg (p2,p3))} then x = LSeg (p1,p2) by A4, A5, A7, A9, TOPREAL1:def_3; hence x in {(LSeg (p1,p2)),(LSeg (p2,p3))} by TARSKI:def_2; ::_thesis: verum end; suppose j = 2 ; ::_thesis: x in {(LSeg (p1,p2)),(LSeg (p2,p3))} then x = LSeg (p2,p3) by A2, A5, A3, A7, TOPREAL1:def_3; hence x in {(LSeg (p1,p2)),(LSeg (p2,p3))} by TARSKI:def_2; ::_thesis: verum end; end; end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(LSeg (p1,p2)),(LSeg (p2,p3))} or x in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ) assume A11: x in {(LSeg (p1,p2)),(LSeg (p2,p3))} ; ::_thesis: x in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } percases ( x = LSeg (p1,p2) or x = LSeg (p2,p3) ) by A11, TARSKI:def_2; supposeA12: x = LSeg (p1,p2) ; ::_thesis: x in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } A13: 1 + 1 <= len f by A2; x = LSeg (f,1) by A2, A4, A5, A6, A12, TOPREAL1:def_3; hence x in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by A13; ::_thesis: verum end; suppose x = LSeg (p2,p3) ; ::_thesis: x in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } then x = LSeg (f,2) by A2, A5, A3, TOPREAL1:def_3; hence x in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } by A2; ::_thesis: verum end; end; end; hence L~ f = (LSeg (p1,p2)) \/ (LSeg (p2,p3)) by ZFMISC_1:75; ::_thesis: verum end; theorem Th17: :: TOPREAL3:17 for f being FinSequence of (TOP-REAL 2) for j, i being Element of NAT st j in dom (f | i) & j + 1 in dom (f | i) holds LSeg (f,j) = LSeg ((f | i),j) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for j, i being Element of NAT st j in dom (f | i) & j + 1 in dom (f | i) holds LSeg (f,j) = LSeg ((f | i),j) let j, i be Element of NAT ; ::_thesis: ( j in dom (f | i) & j + 1 in dom (f | i) implies LSeg (f,j) = LSeg ((f | i),j) ) assume that A1: j in dom (f | i) and A2: j + 1 in dom (f | i) ; ::_thesis: LSeg (f,j) = LSeg ((f | i),j) A3: ( 1 <= j & j + 1 <= len (f | i) ) by A1, A2, FINSEQ_3:25; set p1 = (f | i) /. j; set p2 = (f | i) /. (j + 1); A4: f | i = f | (Seg i) by FINSEQ_1:def_15; then j in (dom f) /\ (Seg i) by A1, RELAT_1:61; then j in dom f by XBOOLE_0:def_4; then A5: 1 <= j by FINSEQ_3:25; j + 1 in (dom f) /\ (Seg i) by A2, A4, RELAT_1:61; then j + 1 in dom f by XBOOLE_0:def_4; then A6: j + 1 <= len f by FINSEQ_3:25; ( (f | i) /. j = f /. j & (f | i) /. (j + 1) = f /. (j + 1) ) by A1, A2, FINSEQ_4:70; then LSeg (f,j) = LSeg (((f | i) /. j),((f | i) /. (j + 1))) by A5, A6, TOPREAL1:def_3; hence LSeg (f,j) = LSeg ((f | i),j) by A3, TOPREAL1:def_3; ::_thesis: verum end; theorem :: TOPREAL3:18 for f, h being FinSequence of (TOP-REAL 2) for j being Element of NAT st j in dom f & j + 1 in dom f holds LSeg ((f ^ h),j) = LSeg (f,j) proof let f, h be FinSequence of (TOP-REAL 2); ::_thesis: for j being Element of NAT st j in dom f & j + 1 in dom f holds LSeg ((f ^ h),j) = LSeg (f,j) let j be Element of NAT ; ::_thesis: ( j in dom f & j + 1 in dom f implies LSeg ((f ^ h),j) = LSeg (f,j) ) assume that A1: j in dom f and A2: j + 1 in dom f ; ::_thesis: LSeg ((f ^ h),j) = LSeg (f,j) A3: ( 1 <= j & j + 1 <= len f ) by A1, A2, FINSEQ_3:25; dom f c= dom (f ^ h) by FINSEQ_1:26; then A4: j + 1 <= len (f ^ h) by A2, FINSEQ_3:25; set p1 = f /. j; set p2 = f /. (j + 1); A5: 1 <= j by A1, FINSEQ_3:25; ( f /. j = (f ^ h) /. j & f /. (j + 1) = (f ^ h) /. (j + 1) ) by A1, A2, FINSEQ_4:68; then LSeg ((f ^ h),j) = LSeg ((f /. j),(f /. (j + 1))) by A5, A4, TOPREAL1:def_3; hence LSeg ((f ^ h),j) = LSeg (f,j) by A3, TOPREAL1:def_3; ::_thesis: verum end; theorem Th19: :: TOPREAL3:19 for n being Element of NAT for f being FinSequence of (TOP-REAL n) for i being Nat holds LSeg (f,i) c= L~ f proof let n be Element of NAT ; ::_thesis: for f being FinSequence of (TOP-REAL n) for i being Nat holds LSeg (f,i) c= L~ f let f be FinSequence of (TOP-REAL n); ::_thesis: for i being Nat holds LSeg (f,i) c= L~ f let i be Nat; ::_thesis: LSeg (f,i) c= L~ f let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LSeg (f,i) or x in L~ f ) assume A1: x in LSeg (f,i) ; ::_thesis: x in L~ f A2: i in NAT by ORDINAL1:def_12; now__::_thesis:_(_(_i_<_1_&_contradiction_)_or_(_i_>=_1_&_x_in_L~_f_)_) percases ( i < 1 or i >= 1 ) ; case i < 1 ; ::_thesis: contradiction hence contradiction by A1, TOPREAL1:def_3; ::_thesis: verum end; caseA3: i >= 1 ; ::_thesis: x in L~ f now__::_thesis:_(_(_i_+_1_>_len_f_&_contradiction_)_or_(_i_+_1_<=_len_f_&_x_in_L~_f_)_) percases ( i + 1 > len f or i + 1 <= len f ) ; case i + 1 > len f ; ::_thesis: contradiction hence contradiction by A1, TOPREAL1:def_3; ::_thesis: verum end; caseA4: i + 1 <= len f ; ::_thesis: x in L~ f set M = { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } ; LSeg (f,i) in { (LSeg (f,j)) where j is Element of NAT : ( 1 <= j & j + 1 <= len f ) } by A2, A3, A4; hence x in L~ f by A1, TARSKI:def_4; ::_thesis: verum end; end; end; hence x in L~ f ; ::_thesis: verum end; end; end; hence x in L~ f ; ::_thesis: verum end; theorem :: TOPREAL3:20 for f being FinSequence of (TOP-REAL 2) for i being Element of NAT holds L~ (f | i) c= L~ f proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for i being Element of NAT holds L~ (f | i) c= L~ f let i be Element of NAT ; ::_thesis: L~ (f | i) c= L~ f set h = f | i; set Mh = { (LSeg ((f | i),n)) where n is Element of NAT : ( 1 <= n & n + 1 <= len (f | i) ) } ; set Mf = { (LSeg (f,m)) where m is Element of NAT : ( 1 <= m & m + 1 <= len f ) } ; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L~ (f | i) or x in L~ f ) A1: f | i = f | (Seg i) by FINSEQ_1:def_15; A2: dom f = Seg (len f) by FINSEQ_1:def_3; assume A3: x in L~ (f | i) ; ::_thesis: x in L~ f then consider X being set such that A4: x in X and A5: X in { (LSeg ((f | i),n)) where n is Element of NAT : ( 1 <= n & n + 1 <= len (f | i) ) } by TARSKI:def_4; consider k being Element of NAT such that A6: X = LSeg ((f | i),k) and A7: 1 <= k and A8: k + 1 <= len (f | i) by A5; percases ( i in dom f or not i in dom f ) ; supposeA9: i in dom f ; ::_thesis: x in L~ f A10: dom (f | i) = (dom f) /\ (Seg i) by A1, RELAT_1:61; A11: i <= len f by A9, FINSEQ_3:25; then Seg i c= dom f by A2, FINSEQ_1:5; then dom (f | i) = Seg i by A10, XBOOLE_1:28; then len (f | i) <= len f by A11, FINSEQ_1:def_3; then A12: k + 1 <= len f by A8, XXREAL_0:2; k <= k + 1 by NAT_1:12; then k <= len (f | i) by A8, XXREAL_0:2; then A13: k in dom (f | i) by A7, FINSEQ_3:25; 1 <= k + 1 by NAT_1:12; then k + 1 in dom (f | i) by A8, FINSEQ_3:25; then X = LSeg (f,k) by A6, A13, Th17; then X in { (LSeg (f,m)) where m is Element of NAT : ( 1 <= m & m + 1 <= len f ) } by A7, A12; hence x in L~ f by A4, TARSKI:def_4; ::_thesis: verum end; supposeA14: not i in dom f ; ::_thesis: x in L~ f now__::_thesis:_(_(_i_<_1_&_contradiction_)_or_(_len_f_<_i_&_x_in_L~_f_)_) percases ( i < 1 or len f < i ) by A14, FINSEQ_3:25; case i < 1 ; ::_thesis: contradiction then i < 0 + 1 ; then i <= 0 by NAT_1:13; then Seg i = {} ; then dom (f | i) = (dom f) /\ {} by A1, RELAT_1:61; then dom (f | i) = {} ; then Seg (len (f | i)) = {} by FINSEQ_1:def_3; then len (f | i) = 0 ; hence contradiction by A3, TOPREAL1:22; ::_thesis: verum end; case len f < i ; ::_thesis: x in L~ f then Seg (len f) c= Seg i by FINSEQ_1:5; then dom f c= Seg i by FINSEQ_1:def_3; then A15: dom f = (dom f) /\ (Seg i) by XBOOLE_1:28; for x being set st x in dom (f | i) holds (f | i) . x = f . x by A1, FUNCT_1:47; then f | i = f by A1, A15, FUNCT_1:2, RELAT_1:61; hence x in L~ f by A4, A5, TARSKI:def_4; ::_thesis: verum end; end; end; hence x in L~ f ; ::_thesis: verum end; end; end; theorem Th21: :: TOPREAL3:21 for r being real number for n being Element of NAT for p1, p2 being Point of (TOP-REAL n) for u being Point of (Euclid n) st p1 in Ball (u,r) & p2 in Ball (u,r) holds LSeg (p1,p2) c= Ball (u,r) proof let r be real number ; ::_thesis: for n being Element of NAT for p1, p2 being Point of (TOP-REAL n) for u being Point of (Euclid n) st p1 in Ball (u,r) & p2 in Ball (u,r) holds LSeg (p1,p2) c= Ball (u,r) let n be Element of NAT ; ::_thesis: for p1, p2 being Point of (TOP-REAL n) for u being Point of (Euclid n) st p1 in Ball (u,r) & p2 in Ball (u,r) holds LSeg (p1,p2) c= Ball (u,r) let p1, p2 be Point of (TOP-REAL n); ::_thesis: for u being Point of (Euclid n) st p1 in Ball (u,r) & p2 in Ball (u,r) holds LSeg (p1,p2) c= Ball (u,r) let u be Point of (Euclid n); ::_thesis: ( p1 in Ball (u,r) & p2 in Ball (u,r) implies LSeg (p1,p2) c= Ball (u,r) ) assume that A1: p1 in Ball (u,r) and A2: p2 in Ball (u,r) ; ::_thesis: LSeg (p1,p2) c= Ball (u,r) reconsider p9 = p1 as Point of (Euclid n) by A1; A3: dist (p9,u) < r by A1, METRIC_1:11; thus LSeg (p1,p2) c= Ball (u,r) ::_thesis: verum proof p2 in { u4 where u4 is Point of (Euclid n) : dist (u,u4) < r } by A2, METRIC_1:17; then A4: ex u4 being Point of (Euclid n) st ( u4 = p2 & dist (u,u4) < r ) ; reconsider q29 = u as Element of REAL n ; let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in LSeg (p1,p2) or a in Ball (u,r) ) reconsider q2 = q29 as Point of (TOP-REAL n) by EUCLID:22; assume a in LSeg (p1,p2) ; ::_thesis: a in Ball (u,r) then consider lambda being Real such that A5: ((1 - lambda) * p1) + (lambda * p2) = a and A6: 0 <= lambda and A7: lambda <= 1 ; A8: lambda = abs lambda by A6, ABSVALUE:def_1; set p = ((1 - lambda) * p1) + (lambda * p2); reconsider p9 = ((1 - lambda) * p1) + (lambda * p2), p19 = p1, p29 = p2 as Element of REAL n by EUCLID:22; reconsider u5 = ((1 - lambda) * p1) + (lambda * p2) as Point of (Euclid n) by EUCLID:22; A9: ( (Pitag_dist n) . (q29,p9) = |.(q29 - p9).| & (Pitag_dist n) . (u,u5) = dist (u,u5) ) by EUCLID:def_6, METRIC_1:def_1; (Pitag_dist n) . (q29,p29) = |.(q29 - p29).| by EUCLID:def_6; then A10: |.(q29 + (- p29)).| < r by A4, METRIC_1:def_1; A11: 0 <= 1 - lambda by A7, XREAL_1:48; then A12: 1 - lambda = abs (1 - lambda) by ABSVALUE:def_1; consider u3 being Point of (Euclid n) such that A13: u3 = p1 and A14: dist (u,u3) < r by A3; A15: (Pitag_dist n) . (q29,p19) = |.(q29 - p19).| by EUCLID:def_6; then A16: dist (u,u3) = |.(q29 - p19).| by A13, METRIC_1:def_1; ( ( (abs (1 - lambda)) * |.(q29 + (- p19)).| < (1 - lambda) * r & (abs lambda) * |.(q29 + (- p29)).| <= lambda * r ) or ( (abs (1 - lambda)) * |.(q29 + (- p19)).| <= (1 - lambda) * r & (abs lambda) * |.(q29 + (- p29)).| < lambda * r ) ) proof percases ( lambda = 0 or lambda > 0 ) by A6; suppose lambda = 0 ; ::_thesis: ( ( (abs (1 - lambda)) * |.(q29 + (- p19)).| < (1 - lambda) * r & (abs lambda) * |.(q29 + (- p29)).| <= lambda * r ) or ( (abs (1 - lambda)) * |.(q29 + (- p19)).| <= (1 - lambda) * r & (abs lambda) * |.(q29 + (- p29)).| < lambda * r ) ) hence ( ( (abs (1 - lambda)) * |.(q29 + (- p19)).| < (1 - lambda) * r & (abs lambda) * |.(q29 + (- p29)).| <= lambda * r ) or ( (abs (1 - lambda)) * |.(q29 + (- p19)).| <= (1 - lambda) * r & (abs lambda) * |.(q29 + (- p29)).| < lambda * r ) ) by A13, A14, A15, A12, A8, METRIC_1:def_1; ::_thesis: verum end; suppose lambda > 0 ; ::_thesis: ( ( (abs (1 - lambda)) * |.(q29 + (- p19)).| < (1 - lambda) * r & (abs lambda) * |.(q29 + (- p29)).| <= lambda * r ) or ( (abs (1 - lambda)) * |.(q29 + (- p19)).| <= (1 - lambda) * r & (abs lambda) * |.(q29 + (- p29)).| < lambda * r ) ) hence ( ( (abs (1 - lambda)) * |.(q29 + (- p19)).| < (1 - lambda) * r & (abs lambda) * |.(q29 + (- p29)).| <= lambda * r ) or ( (abs (1 - lambda)) * |.(q29 + (- p19)).| <= (1 - lambda) * r & (abs lambda) * |.(q29 + (- p29)).| < lambda * r ) ) by A14, A16, A10, A11, A12, A8, XREAL_1:64, XREAL_1:68; ::_thesis: verum end; end; end; then A17: ((abs (1 - lambda)) * |.(q29 + (- p19)).|) + ((abs lambda) * |.(q29 + (- p29)).|) < ((1 - lambda) * r) + (lambda * r) by XREAL_1:8; q29 - p19 = q2 - p1 by EUCLID:69; then A18: ( q29 - p9 = q2 - (((1 - lambda) * p1) + (lambda * p2)) & (1 - lambda) * (q29 - p19) = (1 - lambda) * (q2 - p1) ) by EUCLID:65, EUCLID:69; q29 - p29 = q2 - p2 by EUCLID:69; then A19: lambda * (q29 - p29) = lambda * (q2 - p2) by EUCLID:65; q2 - (((1 - lambda) * p1) + (lambda * p2)) = (((1 - lambda) + lambda) * q2) - (((1 - lambda) * p1) + (lambda * p2)) by EUCLID:29 .= (((1 - lambda) * q2) + (lambda * q2)) - (((1 - lambda) * p1) + (lambda * p2)) by EUCLID:33 .= (((1 - lambda) * q2) + (lambda * q2)) + (- (((1 - lambda) * p1) + (lambda * p2))) .= (((1 - lambda) * q2) + (lambda * q2)) + ((- ((1 - lambda) * p1)) - (lambda * p2)) by EUCLID:38 .= ((((1 - lambda) * q2) + (lambda * q2)) + (- ((1 - lambda) * p1))) + (- (lambda * p2)) by EUCLID:26 .= ((((1 - lambda) * q2) + (- ((1 - lambda) * p1))) + (lambda * q2)) + (- (lambda * p2)) by EUCLID:26 .= ((((1 - lambda) * q2) + ((1 - lambda) * (- p1))) + (lambda * q2)) + (- (lambda * p2)) by EUCLID:40 .= (((1 - lambda) * (q2 + (- p1))) + (lambda * q2)) + (- (lambda * p2)) by EUCLID:32 .= ((1 - lambda) * (q2 + (- p1))) + ((lambda * q2) + (- (lambda * p2))) by EUCLID:26 .= ((1 - lambda) * (q2 + (- p1))) + ((lambda * q2) + (lambda * (- p2))) by EUCLID:40 .= ((1 - lambda) * (q2 - p1)) + (lambda * (q2 - p2)) by EUCLID:32 ; then q29 - p9 = ((1 - lambda) * (q29 - p19)) + (lambda * (q29 - p29)) by A18, A19, EUCLID:64; then A20: |.(q29 - p9).| <= |.((1 - lambda) * (q29 - p19)).| + |.(lambda * (q29 - p29)).| by EUCLID:12; |.((1 - lambda) * (q29 + (- p19))).| + |.(lambda * (q29 + (- p29))).| = ((abs (1 - lambda)) * |.(q29 + (- p19)).|) + |.(lambda * (q29 + (- p29))).| by EUCLID:11 .= ((abs (1 - lambda)) * |.(q29 + (- p19)).|) + ((abs lambda) * |.(q29 + (- p29)).|) by EUCLID:11 ; then |.(q29 - p9).| < r by A20, A17, XXREAL_0:2; then a in { u6 where u6 is Element of (Euclid n) : dist (u,u6) < r } by A5, A9; hence a in Ball (u,r) by METRIC_1:17; ::_thesis: verum end; end; theorem :: TOPREAL3:22 for p1, p2, p being Point of (TOP-REAL 2) for r1, s1, r2, s2, r being real number for u being Point of (Euclid 2) st u = p1 & p1 = |[r1,s1]| & p2 = |[r2,s2]| & p = |[r2,s1]| & p2 in Ball (u,r) holds p in Ball (u,r) proof let p1, p2, p be Point of (TOP-REAL 2); ::_thesis: for r1, s1, r2, s2, r being real number for u being Point of (Euclid 2) st u = p1 & p1 = |[r1,s1]| & p2 = |[r2,s2]| & p = |[r2,s1]| & p2 in Ball (u,r) holds p in Ball (u,r) let r1, s1, r2, s2, r be real number ; ::_thesis: for u being Point of (Euclid 2) st u = p1 & p1 = |[r1,s1]| & p2 = |[r2,s2]| & p = |[r2,s1]| & p2 in Ball (u,r) holds p in Ball (u,r) let u be Point of (Euclid 2); ::_thesis: ( u = p1 & p1 = |[r1,s1]| & p2 = |[r2,s2]| & p = |[r2,s1]| & p2 in Ball (u,r) implies p in Ball (u,r) ) assume that A1: u = p1 and A2: p1 = |[r1,s1]| and A3: p2 = |[r2,s2]| and A4: p = |[r2,s1]| and A5: p2 in Ball (u,r) ; ::_thesis: p in Ball (u,r) reconsider p19 = p1, p29 = p2, p9 = p as Element of REAL 2 by EUCLID:22; reconsider r1 = r1, s1 = s1, r2 = r2, s2 = s2 as Real by XREAL_0:def_1; A6: (Pitag_dist 2) . (p19,p29) = |.(p19 - p29).| by EUCLID:def_6; p2 in { u6 where u6 is Element of (Euclid 2) : dist (u,u6) < r } by A5, METRIC_1:17; then ex u5 being Point of (Euclid 2) st ( u5 = p2 & dist (u,u5) < r ) ; then A7: |.(p19 - p29).| < r by A1, A6, METRIC_1:def_1; reconsider up = p as Point of (Euclid 2) by EUCLID:22; (Pitag_dist 2) . (p19,p9) = |.(p19 - p9).| by EUCLID:def_6; then A8: dist (u,up) = |.(p19 - p9).| by A1, METRIC_1:def_1; (s1 - s2) ^2 >= 0 by XREAL_1:63; then sqrreal . (s1 - s2) >= 0 by RVSUM_1:def_2; then A9: (sqrreal . (r1 - r2)) + 0 <= (sqrreal . (r1 - r2)) + (sqrreal . (s1 - s2)) by XREAL_1:7; p19 - p9 = p1 - p by EUCLID:69; then p19 - p9 = <*(r1 - r2),(s1 - s1)*> by A2, A4, Th5; then sqr (p19 - p9) = <*(sqrreal . (r1 - r2)),(sqrreal . (s1 - s1))*> by FINSEQ_2:36; then A10: Sum (sqr (p19 - p9)) = (sqrreal . (r1 - r2)) + (sqrreal . 0) by RVSUM_1:77 .= (sqrreal . (r1 - r2)) + (0 ^2) by RVSUM_1:def_2 .= sqrreal . (r1 - r2) ; p19 - p29 = p1 - p2 by EUCLID:69; then p19 - p29 = <*(r1 - r2),(s1 - s2)*> by A2, A3, Th5; then sqr (p19 - p29) = <*(sqrreal . (r1 - r2)),(sqrreal . (s1 - s2))*> by FINSEQ_2:36; then A11: |.(p19 - p29).| = sqrt ((sqrreal . (r1 - r2)) + (sqrreal . (s1 - s2))) by RVSUM_1:77; (r1 - r2) ^2 >= 0 by XREAL_1:63; then sqrreal . (r1 - r2) >= 0 by RVSUM_1:def_2; then |.(p19 - p9).| <= sqrt ((sqrreal . (r1 - r2)) + (sqrreal . (s1 - s2))) by A10, A9, SQUARE_1:26; then |.(p19 - p9).| < r by A7, A11, XXREAL_0:2; then p in { u6 where u6 is Element of (Euclid 2) : dist (u,u6) < r } by A8; hence p in Ball (u,r) by METRIC_1:17; ::_thesis: verum end; theorem :: TOPREAL3:23 for s, r1, r, s1 being real number for u being Point of (Euclid 2) st |[s,r1]| in Ball (u,r) & |[s,s1]| in Ball (u,r) holds |[s,((r1 + s1) / 2)]| in Ball (u,r) proof let s, r1, r, s1 be real number ; ::_thesis: for u being Point of (Euclid 2) st |[s,r1]| in Ball (u,r) & |[s,s1]| in Ball (u,r) holds |[s,((r1 + s1) / 2)]| in Ball (u,r) let u be Point of (Euclid 2); ::_thesis: ( |[s,r1]| in Ball (u,r) & |[s,s1]| in Ball (u,r) implies |[s,((r1 + s1) / 2)]| in Ball (u,r) ) set p = |[s,r1]|; set q = |[s,s1]|; set p3 = |[s,((r1 + s1) / 2)]|; assume ( |[s,r1]| in Ball (u,r) & |[s,s1]| in Ball (u,r) ) ; ::_thesis: |[s,((r1 + s1) / 2)]| in Ball (u,r) then A1: LSeg (|[s,r1]|,|[s,s1]|) c= Ball (u,r) by Th21; ( |[s,r1]| `2 = r1 & |[s,s1]| `2 = s1 ) by EUCLID:52; then A2: |[s,((r1 + s1) / 2)]| `2 = ((1 - (1 / 2)) * (|[s,r1]| `2)) + ((1 / 2) * (|[s,s1]| `2)) by EUCLID:52 .= (((1 - (1 / 2)) * |[s,r1]|) `2) + ((1 / 2) * (|[s,s1]| `2)) by Th4 .= (((1 - (1 / 2)) * |[s,r1]|) `2) + (((1 / 2) * |[s,s1]|) `2) by Th4 .= (((1 - (1 / 2)) * |[s,r1]|) + ((1 / 2) * |[s,s1]|)) `2 by Th2 ; ( |[s,r1]| `1 = s & |[s,s1]| `1 = s ) by EUCLID:52; then |[s,((r1 + s1) / 2)]| `1 = ((1 - (1 / 2)) * (|[s,r1]| `1)) + ((1 / 2) * (|[s,s1]| `1)) by EUCLID:52 .= (((1 - (1 / 2)) * |[s,r1]|) `1) + ((1 / 2) * (|[s,s1]| `1)) by Th4 .= (((1 - (1 / 2)) * |[s,r1]|) `1) + (((1 / 2) * |[s,s1]|) `1) by Th4 .= (((1 - (1 / 2)) * |[s,r1]|) + ((1 / 2) * |[s,s1]|)) `1 by Th2 ; then |[s,((r1 + s1) / 2)]| = ((1 - (1 / 2)) * |[s,r1]|) + ((1 / 2) * |[s,s1]|) by A2, Th6; then |[s,((r1 + s1) / 2)]| in { (((1 - lambda) * |[s,r1]|) + (lambda * |[s,s1]|)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) } ; hence |[s,((r1 + s1) / 2)]| in Ball (u,r) by A1; ::_thesis: verum end; theorem :: TOPREAL3:24 for r1, s, r, s1 being real number for u being Point of (Euclid 2) st |[r1,s]| in Ball (u,r) & |[s1,s]| in Ball (u,r) holds |[((r1 + s1) / 2),s]| in Ball (u,r) proof let r1, s, r, s1 be real number ; ::_thesis: for u being Point of (Euclid 2) st |[r1,s]| in Ball (u,r) & |[s1,s]| in Ball (u,r) holds |[((r1 + s1) / 2),s]| in Ball (u,r) let u be Point of (Euclid 2); ::_thesis: ( |[r1,s]| in Ball (u,r) & |[s1,s]| in Ball (u,r) implies |[((r1 + s1) / 2),s]| in Ball (u,r) ) set p = |[r1,s]|; set q = |[s1,s]|; set p3 = |[((r1 + s1) / 2),s]|; assume ( |[r1,s]| in Ball (u,r) & |[s1,s]| in Ball (u,r) ) ; ::_thesis: |[((r1 + s1) / 2),s]| in Ball (u,r) then A1: LSeg (|[r1,s]|,|[s1,s]|) c= Ball (u,r) by Th21; ( |[r1,s]| `1 = r1 & |[s1,s]| `1 = s1 ) by EUCLID:52; then A2: |[((r1 + s1) / 2),s]| `1 = ((1 - (1 / 2)) * (|[r1,s]| `1)) + ((1 / 2) * (|[s1,s]| `1)) by EUCLID:52 .= (((1 - (1 / 2)) * |[r1,s]|) `1) + ((1 / 2) * (|[s1,s]| `1)) by Th4 .= (((1 - (1 / 2)) * |[r1,s]|) `1) + (((1 / 2) * |[s1,s]|) `1) by Th4 .= (((1 - (1 / 2)) * |[r1,s]|) + ((1 / 2) * |[s1,s]|)) `1 by Th2 ; ( |[r1,s]| `2 = s & |[s1,s]| `2 = s ) by EUCLID:52; then |[((r1 + s1) / 2),s]| `2 = ((1 - (1 / 2)) * (|[r1,s]| `2)) + ((1 / 2) * (|[s1,s]| `2)) by EUCLID:52 .= (((1 - (1 / 2)) * |[r1,s]|) `2) + ((1 / 2) * (|[s1,s]| `2)) by Th4 .= (((1 - (1 / 2)) * |[r1,s]|) `2) + (((1 / 2) * |[s1,s]|) `2) by Th4 .= (((1 - (1 / 2)) * |[r1,s]|) + ((1 / 2) * |[s1,s]|)) `2 by Th2 ; then |[((r1 + s1) / 2),s]| = ((1 - (1 / 2)) * |[r1,s]|) + ((1 / 2) * |[s1,s]|) by A2, Th6; then |[((r1 + s1) / 2),s]| in { (((1 - lambda) * |[r1,s]|) + (lambda * |[s1,s]|)) where lambda is Real : ( 0 <= lambda & lambda <= 1 ) } ; hence |[((r1 + s1) / 2),s]| in Ball (u,r) by A1; ::_thesis: verum end; theorem :: TOPREAL3:25 for r1, r2, r, s1, s2 being real number for u being Point of (Euclid 2) st |[r1,r2]| in Ball (u,r) & |[s1,s2]| in Ball (u,r) & not |[r1,s2]| in Ball (u,r) holds |[s1,r2]| in Ball (u,r) proof let r1, r2, r, s1, s2 be real number ; ::_thesis: for u being Point of (Euclid 2) st |[r1,r2]| in Ball (u,r) & |[s1,s2]| in Ball (u,r) & not |[r1,s2]| in Ball (u,r) holds |[s1,r2]| in Ball (u,r) let u be Point of (Euclid 2); ::_thesis: ( |[r1,r2]| in Ball (u,r) & |[s1,s2]| in Ball (u,r) & not |[r1,s2]| in Ball (u,r) implies |[s1,r2]| in Ball (u,r) ) assume that A1: |[r1,r2]| in Ball (u,r) and A2: |[s1,s2]| in Ball (u,r) ; ::_thesis: ( |[r1,s2]| in Ball (u,r) or |[s1,r2]| in Ball (u,r) ) A3: r > 0 by A1, TBSP_1:12; percases ( |[r1,s2]| in Ball (u,r) or not |[r1,s2]| in Ball (u,r) ) ; suppose |[r1,s2]| in Ball (u,r) ; ::_thesis: ( |[r1,s2]| in Ball (u,r) or |[s1,r2]| in Ball (u,r) ) hence ( |[r1,s2]| in Ball (u,r) or |[s1,r2]| in Ball (u,r) ) ; ::_thesis: verum end; supposeA4: not |[r1,s2]| in Ball (u,r) ; ::_thesis: ( |[r1,s2]| in Ball (u,r) or |[s1,r2]| in Ball (u,r) ) reconsider p = u as Point of (TOP-REAL 2) by EUCLID:22; set p1 = |[r1,s2]|; set p2 = |[s1,r2]|; set p3 = |[s1,s2]|; set p4 = |[r1,r2]|; reconsider u1 = |[r1,s2]|, u2 = |[s1,r2]|, u3 = |[s1,s2]|, u4 = |[r1,r2]| as Point of (Euclid 2) by EUCLID:22; set a = (((p `1) - (|[r1,s2]| `1)) ^2) + (((p `2) - (|[r1,s2]| `2)) ^2); set b = (((p `1) - (|[r1,r2]| `1)) ^2) + (((p `2) - (|[r1,r2]| `2)) ^2); set c = (((p `1) - (|[s1,s2]| `1)) ^2) + (((p `2) - (|[s1,s2]| `2)) ^2); set d = (((p `1) - (|[s1,r2]| `1)) ^2) + (((p `2) - (|[s1,r2]| `2)) ^2); ( (Pitag_dist 2) . (u,u1) = dist (u,u1) & r <= dist (u,u1) ) by A4, METRIC_1:11, METRIC_1:def_1; then r <= sqrt ((((p `1) - (|[r1,s2]| `1)) ^2) + (((p `2) - (|[r1,s2]| `2)) ^2)) by Th7; then A5: r * r <= (sqrt ((((p `1) - (|[r1,s2]| `1)) ^2) + (((p `2) - (|[r1,s2]| `2)) ^2))) ^2 by A3, XREAL_1:66; ( ((p `1) - (|[r1,s2]| `1)) ^2 >= 0 & ((p `2) - (|[r1,s2]| `2)) ^2 >= 0 ) by XREAL_1:63; then A6: r ^2 <= (((p `1) - (|[r1,s2]| `1)) ^2) + (((p `2) - (|[r1,s2]| `2)) ^2) by A5, SQUARE_1:def_2; A7: ( |[s1,r2]| `1 = s1 & |[s1,r2]| `2 = r2 ) by EUCLID:52; A8: ( |[r1,r2]| `1 = r1 & |[r1,r2]| `2 = r2 ) by EUCLID:52; A9: ( |[s1,s2]| `1 = s1 & |[s1,s2]| `2 = s2 ) by EUCLID:52; ( (Pitag_dist 2) . (u,u3) = dist (u,u3) & dist (u,u3) < r ) by A2, METRIC_1:11, METRIC_1:def_1; then A10: sqrt ((((p `1) - (|[s1,s2]| `1)) ^2) + (((p `2) - (|[s1,s2]| `2)) ^2)) < r by Th7; A11: ( ((p `1) - (|[s1,s2]| `1)) ^2 >= 0 & ((p `2) - (|[s1,s2]| `2)) ^2 >= 0 ) by XREAL_1:63; then 0 <= sqrt ((((p `1) - (|[s1,s2]| `1)) ^2) + (((p `2) - (|[s1,s2]| `2)) ^2)) by SQUARE_1:def_2; then (sqrt ((((p `1) - (|[s1,s2]| `1)) ^2) + (((p `2) - (|[s1,s2]| `2)) ^2))) ^2 < r * r by A10, XREAL_1:96; then A12: (((p `1) - (|[s1,s2]| `1)) ^2) + (((p `2) - (|[s1,s2]| `2)) ^2) < r * r by A11, SQUARE_1:def_2; ( (Pitag_dist 2) . (u,u4) = dist (u,u4) & dist (u,u4) < r ) by A1, METRIC_1:11, METRIC_1:def_1; then A13: sqrt ((((p `1) - (|[r1,r2]| `1)) ^2) + (((p `2) - (|[r1,r2]| `2)) ^2)) < r by Th7; ( |[r1,s2]| `1 = r1 & |[r1,s2]| `2 = s2 ) by EUCLID:52; then ((((p `1) - (|[s1,s2]| `1)) ^2) + (((p `2) - (|[s1,s2]| `2)) ^2)) + ((((p `1) - (|[r1,r2]| `1)) ^2) + (((p `2) - (|[r1,r2]| `2)) ^2)) = ((((p `1) - (|[r1,s2]| `1)) ^2) + (((p `2) - (|[r1,s2]| `2)) ^2)) + ((((p `1) - (|[s1,r2]| `1)) ^2) + (((p `2) - (|[s1,r2]| `2)) ^2)) by A7, A9, A8; then A14: (r ^2) + ((((p `1) - (|[s1,r2]| `1)) ^2) + (((p `2) - (|[s1,r2]| `2)) ^2)) <= ((((p `1) - (|[s1,s2]| `1)) ^2) + (((p `2) - (|[s1,s2]| `2)) ^2)) + ((((p `1) - (|[r1,r2]| `1)) ^2) + (((p `2) - (|[r1,r2]| `2)) ^2)) by A6, XREAL_1:6; A15: ( ((p `1) - (|[r1,r2]| `1)) ^2 >= 0 & ((p `2) - (|[r1,r2]| `2)) ^2 >= 0 ) by XREAL_1:63; then 0 <= sqrt ((((p `1) - (|[r1,r2]| `1)) ^2) + (((p `2) - (|[r1,r2]| `2)) ^2)) by SQUARE_1:def_2; then (sqrt ((((p `1) - (|[r1,r2]| `1)) ^2) + (((p `2) - (|[r1,r2]| `2)) ^2))) ^2 < r * r by A13, XREAL_1:96; then (((p `1) - (|[r1,r2]| `1)) ^2) + (((p `2) - (|[r1,r2]| `2)) ^2) < r ^2 by A15, SQUARE_1:def_2; then ((((p `1) - (|[s1,s2]| `1)) ^2) + (((p `2) - (|[s1,s2]| `2)) ^2)) + ((((p `1) - (|[r1,r2]| `1)) ^2) + (((p `2) - (|[r1,r2]| `2)) ^2)) < (r ^2) + (r ^2) by A12, XREAL_1:8; then (r ^2) + ((((p `1) - (|[s1,r2]| `1)) ^2) + (((p `2) - (|[s1,r2]| `2)) ^2)) < (r ^2) + (r ^2) by A14, XXREAL_0:2; then A16: (((p `1) - (|[s1,r2]| `1)) ^2) + (((p `2) - (|[s1,r2]| `2)) ^2) < ((r ^2) + (r ^2)) - (r ^2) by XREAL_1:20; ( ((p `1) - (|[s1,r2]| `1)) ^2 >= 0 & ((p `2) - (|[s1,r2]| `2)) ^2 >= 0 ) by XREAL_1:63; then sqrt ((((p `1) - (|[s1,r2]| `1)) ^2) + (((p `2) - (|[s1,r2]| `2)) ^2)) < sqrt (r ^2) by A16, SQUARE_1:27; then A17: sqrt ((((p `1) - (|[s1,r2]| `1)) ^2) + (((p `2) - (|[s1,r2]| `2)) ^2)) < r by A3, SQUARE_1:22; dist (u,u2) = (Pitag_dist 2) . (u,u2) by METRIC_1:def_1 .= sqrt ((((p `1) - (|[s1,r2]| `1)) ^2) + (((p `2) - (|[s1,r2]| `2)) ^2)) by Th7 ; hence ( |[r1,s2]| in Ball (u,r) or |[s1,r2]| in Ball (u,r) ) by A17, METRIC_1:11; ::_thesis: verum end; end; end; theorem :: TOPREAL3:26 for f being FinSequence of (TOP-REAL 2) for r being real number for u being Point of (Euclid 2) for m being Element of NAT st not f /. 1 in Ball (u,r) & 1 <= m & m <= (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 & (LSeg (f,i)) /\ (Ball (u,r)) <> {} holds m <= i ) holds not f /. m in Ball (u,r) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for r being real number for u being Point of (Euclid 2) for m being Element of NAT st not f /. 1 in Ball (u,r) & 1 <= m & m <= (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 & (LSeg (f,i)) /\ (Ball (u,r)) <> {} holds m <= i ) holds not f /. m in Ball (u,r) let r be real number ; ::_thesis: for u being Point of (Euclid 2) for m being Element of NAT st not f /. 1 in Ball (u,r) & 1 <= m & m <= (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 & (LSeg (f,i)) /\ (Ball (u,r)) <> {} holds m <= i ) holds not f /. m in Ball (u,r) let u be Point of (Euclid 2); ::_thesis: for m being Element of NAT st not f /. 1 in Ball (u,r) & 1 <= m & m <= (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 & (LSeg (f,i)) /\ (Ball (u,r)) <> {} holds m <= i ) holds not f /. m in Ball (u,r) let m be Element of NAT ; ::_thesis: ( not f /. 1 in Ball (u,r) & 1 <= m & m <= (len f) - 1 & ( for i being Element of NAT st 1 <= i & i <= (len f) - 1 & (LSeg (f,i)) /\ (Ball (u,r)) <> {} holds m <= i ) implies not f /. m in Ball (u,r) ) assume that A1: not f /. 1 in Ball (u,r) and A2: 1 <= m and A3: m <= (len f) - 1 and A4: for i being Element of NAT st 1 <= i & i <= (len f) - 1 & (LSeg (f,i)) /\ (Ball (u,r)) <> {} holds m <= i ; ::_thesis: not f /. m in Ball (u,r) assume A5: f /. m in Ball (u,r) ; ::_thesis: contradiction percases ( 1 = m or 1 < m ) by A2, XXREAL_0:1; suppose 1 = m ; ::_thesis: contradiction hence contradiction by A1, A5; ::_thesis: verum end; supposeA6: 1 < m ; ::_thesis: contradiction then reconsider k = m - 1 as Element of NAT by INT_1:5; 1 + 1 <= m by A6, NAT_1:13; then A7: 1 <= m - 1 by XREAL_1:19; m - 1 <= m by XREAL_1:43; then A8: k <= (len f) - 1 by A3, XXREAL_0:2; then k + 1 <= len f by XREAL_1:19; then f /. (k + 1) in LSeg (f,k) by A7, TOPREAL1:21; then (LSeg (f,k)) /\ (Ball (u,r)) <> {} by A5, XBOOLE_0:def_4; then m <= k by A4, A7, A8; then m + 1 <= m by XREAL_1:19; hence contradiction by NAT_1:13; ::_thesis: verum end; end; end; theorem :: TOPREAL3:27 for q, p2, p being Point of (TOP-REAL 2) st q `2 = p2 `2 & p `2 <> p2 `2 holds ((LSeg (p2,|[(p2 `1),(p `2)]|)) \/ (LSeg (|[(p2 `1),(p `2)]|,p))) /\ (LSeg (q,p2)) = {p2} proof let q, p2, p be Point of (TOP-REAL 2); ::_thesis: ( q `2 = p2 `2 & p `2 <> p2 `2 implies ((LSeg (p2,|[(p2 `1),(p `2)]|)) \/ (LSeg (|[(p2 `1),(p `2)]|,p))) /\ (LSeg (q,p2)) = {p2} ) assume that A1: q `2 = p2 `2 and A2: p `2 <> p2 `2 ; ::_thesis: ((LSeg (p2,|[(p2 `1),(p `2)]|)) \/ (LSeg (|[(p2 `1),(p `2)]|,p))) /\ (LSeg (q,p2)) = {p2} set p3 = |[(p2 `1),(p `2)]|; set l23 = LSeg (p2,|[(p2 `1),(p `2)]|); set l3 = LSeg (|[(p2 `1),(p `2)]|,p); set l = LSeg (q,p2); A3: (LSeg (|[(p2 `1),(p `2)]|,p)) /\ (LSeg (q,p2)) = {} proof set x = the Element of (LSeg (|[(p2 `1),(p `2)]|,p)) /\ (LSeg (q,p2)); assume A4: (LSeg (|[(p2 `1),(p `2)]|,p)) /\ (LSeg (q,p2)) <> {} ; ::_thesis: contradiction then the Element of (LSeg (|[(p2 `1),(p `2)]|,p)) /\ (LSeg (q,p2)) in LSeg (|[(p2 `1),(p `2)]|,p) by XBOOLE_0:def_4; then consider s1 being Real such that A5: the Element of (LSeg (|[(p2 `1),(p `2)]|,p)) /\ (LSeg (q,p2)) = ((1 - s1) * |[(p2 `1),(p `2)]|) + (s1 * p) and 0 <= s1 and s1 <= 1 ; the Element of (LSeg (|[(p2 `1),(p `2)]|,p)) /\ (LSeg (q,p2)) in LSeg (q,p2) by A4, XBOOLE_0:def_4; then consider s2 being Real such that A6: the Element of (LSeg (|[(p2 `1),(p `2)]|,p)) /\ (LSeg (q,p2)) = ((1 - s2) * q) + (s2 * p2) and 0 <= s2 and s2 <= 1 ; A7: (((1 - s1) * |[(p2 `1),(p `2)]|) + (s1 * p)) `2 = (((1 - s1) * |[(p2 `1),(p `2)]|) `2) + ((s1 * p) `2) by Th2 .= ((1 - s1) * (|[(p2 `1),(p `2)]| `2)) + ((s1 * p) `2) by Th4 .= ((1 - s1) * (|[(p2 `1),(p `2)]| `2)) + (s1 * (p `2)) by Th4 .= ((1 - s1) * (p `2)) + (s1 * (p `2)) by EUCLID:52 .= p `2 ; (((1 - s2) * q) + (s2 * p2)) `2 = (((1 - s2) * q) `2) + ((s2 * p2) `2) by Th2 .= ((1 - s2) * (q `2)) + ((s2 * p2) `2) by Th4 .= ((1 - s2) * (q `2)) + (s2 * (p2 `2)) by Th4 .= p2 `2 by A1 ; hence contradiction by A2, A5, A7, A6; ::_thesis: verum end; A8: (LSeg (p2,|[(p2 `1),(p `2)]|)) /\ (LSeg (q,p2)) = {p2} proof thus (LSeg (p2,|[(p2 `1),(p `2)]|)) /\ (LSeg (q,p2)) c= {p2} :: according to XBOOLE_0:def_10 ::_thesis: {p2} c= (LSeg (p2,|[(p2 `1),(p `2)]|)) /\ (LSeg (q,p2)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (LSeg (p2,|[(p2 `1),(p `2)]|)) /\ (LSeg (q,p2)) or x in {p2} ) assume A9: x in (LSeg (p2,|[(p2 `1),(p `2)]|)) /\ (LSeg (q,p2)) ; ::_thesis: x in {p2} then x in LSeg (p2,|[(p2 `1),(p `2)]|) by XBOOLE_0:def_4; then consider s1 being Real such that A10: ((1 - s1) * p2) + (s1 * |[(p2 `1),(p `2)]|) = x and 0 <= s1 and s1 <= 1 ; x in LSeg (q,p2) by A9, XBOOLE_0:def_4; then consider s2 being Real such that A11: ((1 - s2) * q) + (s2 * p2) = x and 0 <= s2 and s2 <= 1 ; A12: (((1 - s2) * q) + (s2 * p2)) `2 = (((1 - s2) * q) `2) + ((s2 * p2) `2) by Th2 .= ((1 - s2) * (q `2)) + ((s2 * p2) `2) by Th4 .= ((1 - s2) * (q `2)) + (s2 * (p2 `2)) by Th4 .= p2 `2 by A1 ; set t = ((1 - s1) * p2) + (s1 * |[(p2 `1),(p `2)]|); A13: (((1 - s1) * p2) + (s1 * |[(p2 `1),(p `2)]|)) `1 = (((1 - s1) * p2) `1) + ((s1 * |[(p2 `1),(p `2)]|) `1) by Th2 .= ((1 - s1) * (p2 `1)) + ((s1 * |[(p2 `1),(p `2)]|) `1) by Th4 .= ((1 - s1) * (p2 `1)) + (s1 * (|[(p2 `1),(p `2)]| `1)) by Th4 .= ((1 - s1) * (p2 `1)) + (s1 * (p2 `1)) by EUCLID:52 .= p2 `1 ; ((1 - s1) * p2) + (s1 * |[(p2 `1),(p `2)]|) = |[((((1 - s1) * p2) + (s1 * |[(p2 `1),(p `2)]|)) `1),((((1 - s1) * p2) + (s1 * |[(p2 `1),(p `2)]|)) `2)]| by EUCLID:53 .= p2 by A10, A13, A11, A12, EUCLID:53 ; hence x in {p2} by A10, TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {p2} or x in (LSeg (p2,|[(p2 `1),(p `2)]|)) /\ (LSeg (q,p2)) ) assume x in {p2} ; ::_thesis: x in (LSeg (p2,|[(p2 `1),(p `2)]|)) /\ (LSeg (q,p2)) then A14: x = p2 by TARSKI:def_1; ( p2 in LSeg (p2,|[(p2 `1),(p `2)]|) & p2 in LSeg (q,p2) ) by RLTOPSP1:68; hence x in (LSeg (p2,|[(p2 `1),(p `2)]|)) /\ (LSeg (q,p2)) by A14, XBOOLE_0:def_4; ::_thesis: verum end; thus ((LSeg (p2,|[(p2 `1),(p `2)]|)) \/ (LSeg (|[(p2 `1),(p `2)]|,p))) /\ (LSeg (q,p2)) = ((LSeg (p2,|[(p2 `1),(p `2)]|)) /\ (LSeg (q,p2))) \/ ((LSeg (|[(p2 `1),(p `2)]|,p)) /\ (LSeg (q,p2))) by XBOOLE_1:23 .= {p2} by A8, A3 ; ::_thesis: verum end; theorem :: TOPREAL3:28 for q, p2, p being Point of (TOP-REAL 2) st q `1 = p2 `1 & p `1 <> p2 `1 holds ((LSeg (p2,|[(p `1),(p2 `2)]|)) \/ (LSeg (|[(p `1),(p2 `2)]|,p))) /\ (LSeg (q,p2)) = {p2} proof let q, p2, p be Point of (TOP-REAL 2); ::_thesis: ( q `1 = p2 `1 & p `1 <> p2 `1 implies ((LSeg (p2,|[(p `1),(p2 `2)]|)) \/ (LSeg (|[(p `1),(p2 `2)]|,p))) /\ (LSeg (q,p2)) = {p2} ) assume that A1: q `1 = p2 `1 and A2: p `1 <> p2 `1 ; ::_thesis: ((LSeg (p2,|[(p `1),(p2 `2)]|)) \/ (LSeg (|[(p `1),(p2 `2)]|,p))) /\ (LSeg (q,p2)) = {p2} set p3 = |[(p `1),(p2 `2)]|; set l23 = LSeg (p2,|[(p `1),(p2 `2)]|); set l3 = LSeg (|[(p `1),(p2 `2)]|,p); set l = LSeg (q,p2); A3: (LSeg (|[(p `1),(p2 `2)]|,p)) /\ (LSeg (q,p2)) = {} proof set x = the Element of (LSeg (|[(p `1),(p2 `2)]|,p)) /\ (LSeg (q,p2)); assume A4: (LSeg (|[(p `1),(p2 `2)]|,p)) /\ (LSeg (q,p2)) <> {} ; ::_thesis: contradiction then the Element of (LSeg (|[(p `1),(p2 `2)]|,p)) /\ (LSeg (q,p2)) in LSeg (|[(p `1),(p2 `2)]|,p) by XBOOLE_0:def_4; then consider d1 being Real such that A5: the Element of (LSeg (|[(p `1),(p2 `2)]|,p)) /\ (LSeg (q,p2)) = ((1 - d1) * |[(p `1),(p2 `2)]|) + (d1 * p) and 0 <= d1 and d1 <= 1 ; the Element of (LSeg (|[(p `1),(p2 `2)]|,p)) /\ (LSeg (q,p2)) in LSeg (q,p2) by A4, XBOOLE_0:def_4; then consider d2 being Real such that A6: the Element of (LSeg (|[(p `1),(p2 `2)]|,p)) /\ (LSeg (q,p2)) = ((1 - d2) * q) + (d2 * p2) and 0 <= d2 and d2 <= 1 ; A7: (((1 - d1) * |[(p `1),(p2 `2)]|) + (d1 * p)) `1 = (((1 - d1) * |[(p `1),(p2 `2)]|) `1) + ((d1 * p) `1) by Th2 .= ((1 - d1) * (|[(p `1),(p2 `2)]| `1)) + ((d1 * p) `1) by Th4 .= ((1 - d1) * (|[(p `1),(p2 `2)]| `1)) + (d1 * (p `1)) by Th4 .= ((1 - d1) * (p `1)) + (d1 * (p `1)) by EUCLID:52 .= p `1 ; (((1 - d2) * q) + (d2 * p2)) `1 = (((1 - d2) * q) `1) + ((d2 * p2) `1) by Th2 .= ((1 - d2) * (q `1)) + ((d2 * p2) `1) by Th4 .= ((1 - d2) * (q `1)) + (d2 * (p2 `1)) by Th4 .= p2 `1 by A1 ; hence contradiction by A2, A5, A7, A6; ::_thesis: verum end; A8: (LSeg (p2,|[(p `1),(p2 `2)]|)) /\ (LSeg (q,p2)) = {p2} proof thus (LSeg (p2,|[(p `1),(p2 `2)]|)) /\ (LSeg (q,p2)) c= {p2} :: according to XBOOLE_0:def_10 ::_thesis: {p2} c= (LSeg (p2,|[(p `1),(p2 `2)]|)) /\ (LSeg (q,p2)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (LSeg (p2,|[(p `1),(p2 `2)]|)) /\ (LSeg (q,p2)) or x in {p2} ) assume A9: x in (LSeg (p2,|[(p `1),(p2 `2)]|)) /\ (LSeg (q,p2)) ; ::_thesis: x in {p2} then x in LSeg (p2,|[(p `1),(p2 `2)]|) by XBOOLE_0:def_4; then consider s1 being Real such that A10: x = ((1 - s1) * p2) + (s1 * |[(p `1),(p2 `2)]|) and 0 <= s1 and s1 <= 1 ; x in LSeg (q,p2) by A9, XBOOLE_0:def_4; then consider s2 being Real such that A11: x = ((1 - s2) * q) + (s2 * p2) and 0 <= s2 and s2 <= 1 ; A12: (((1 - s2) * q) + (s2 * p2)) `1 = (((1 - s2) * q) `1) + ((s2 * p2) `1) by Th2 .= ((1 - s2) * (q `1)) + ((s2 * p2) `1) by Th4 .= ((1 - s2) * (q `1)) + (s2 * (p2 `1)) by Th4 .= p2 `1 by A1 ; set t = ((1 - s1) * p2) + (s1 * |[(p `1),(p2 `2)]|); A13: (((1 - s1) * p2) + (s1 * |[(p `1),(p2 `2)]|)) `2 = (((1 - s1) * p2) `2) + ((s1 * |[(p `1),(p2 `2)]|) `2) by Th2 .= ((1 - s1) * (p2 `2)) + ((s1 * |[(p `1),(p2 `2)]|) `2) by Th4 .= ((1 - s1) * (p2 `2)) + (s1 * (|[(p `1),(p2 `2)]| `2)) by Th4 .= ((1 - s1) * (p2 `2)) + (s1 * (p2 `2)) by EUCLID:52 .= p2 `2 ; ((1 - s1) * p2) + (s1 * |[(p `1),(p2 `2)]|) = |[((((1 - s1) * p2) + (s1 * |[(p `1),(p2 `2)]|)) `1),((((1 - s1) * p2) + (s1 * |[(p `1),(p2 `2)]|)) `2)]| by EUCLID:53 .= p2 by A10, A13, A11, A12, EUCLID:53 ; hence x in {p2} by A10, TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {p2} or x in (LSeg (p2,|[(p `1),(p2 `2)]|)) /\ (LSeg (q,p2)) ) assume x in {p2} ; ::_thesis: x in (LSeg (p2,|[(p `1),(p2 `2)]|)) /\ (LSeg (q,p2)) then A14: x = p2 by TARSKI:def_1; ( p2 in LSeg (p2,|[(p `1),(p2 `2)]|) & p2 in LSeg (q,p2) ) by RLTOPSP1:68; hence x in (LSeg (p2,|[(p `1),(p2 `2)]|)) /\ (LSeg (q,p2)) by A14, XBOOLE_0:def_4; ::_thesis: verum end; thus ((LSeg (p2,|[(p `1),(p2 `2)]|)) \/ (LSeg (|[(p `1),(p2 `2)]|,p))) /\ (LSeg (q,p2)) = ((LSeg (p2,|[(p `1),(p2 `2)]|)) /\ (LSeg (q,p2))) \/ ((LSeg (|[(p `1),(p2 `2)]|,p)) /\ (LSeg (q,p2))) by XBOOLE_1:23 .= {p2} by A8, A3 ; ::_thesis: verum end; theorem Th29: :: TOPREAL3:29 for p, q being Point of (TOP-REAL 2) holds (LSeg (p,|[(p `1),(q `2)]|)) /\ (LSeg (|[(p `1),(q `2)]|,q)) = {|[(p `1),(q `2)]|} proof let p, q be Point of (TOP-REAL 2); ::_thesis: (LSeg (p,|[(p `1),(q `2)]|)) /\ (LSeg (|[(p `1),(q `2)]|,q)) = {|[(p `1),(q `2)]|} set p3 = |[(p `1),(q `2)]|; set l23 = LSeg (p,|[(p `1),(q `2)]|); set l = LSeg (|[(p `1),(q `2)]|,q); thus (LSeg (p,|[(p `1),(q `2)]|)) /\ (LSeg (|[(p `1),(q `2)]|,q)) c= {|[(p `1),(q `2)]|} :: according to XBOOLE_0:def_10 ::_thesis: {|[(p `1),(q `2)]|} c= (LSeg (p,|[(p `1),(q `2)]|)) /\ (LSeg (|[(p `1),(q `2)]|,q)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (LSeg (p,|[(p `1),(q `2)]|)) /\ (LSeg (|[(p `1),(q `2)]|,q)) or x in {|[(p `1),(q `2)]|} ) assume A1: x in (LSeg (p,|[(p `1),(q `2)]|)) /\ (LSeg (|[(p `1),(q `2)]|,q)) ; ::_thesis: x in {|[(p `1),(q `2)]|} then x in LSeg (p,|[(p `1),(q `2)]|) by XBOOLE_0:def_4; then consider d1 being Real such that A2: x = ((1 - d1) * p) + (d1 * |[(p `1),(q `2)]|) and 0 <= d1 and d1 <= 1 ; x in LSeg (|[(p `1),(q `2)]|,q) by A1, XBOOLE_0:def_4; then consider d2 being Real such that A3: x = ((1 - d2) * |[(p `1),(q `2)]|) + (d2 * q) and 0 <= d2 and d2 <= 1 ; set t = ((1 - d1) * p) + (d1 * |[(p `1),(q `2)]|); A4: (((1 - d1) * p) + (d1 * |[(p `1),(q `2)]|)) `1 = (((1 - d1) * p) `1) + ((d1 * |[(p `1),(q `2)]|) `1) by Th2 .= ((1 - d1) * (p `1)) + ((d1 * |[(p `1),(q `2)]|) `1) by Th4 .= ((1 - d1) * (p `1)) + (d1 * (|[(p `1),(q `2)]| `1)) by Th4 .= ((1 - d1) * (p `1)) + (d1 * (p `1)) by EUCLID:52 .= |[(p `1),(q `2)]| `1 by EUCLID:52 ; (((1 - d1) * p) + (d1 * |[(p `1),(q `2)]|)) `2 = (((1 - d2) * |[(p `1),(q `2)]|) `2) + ((d2 * q) `2) by A2, A3, Th2 .= ((1 - d2) * (|[(p `1),(q `2)]| `2)) + ((d2 * q) `2) by Th4 .= ((1 - d2) * (|[(p `1),(q `2)]| `2)) + (d2 * (q `2)) by Th4 .= ((1 - d2) * (q `2)) + (d2 * (q `2)) by EUCLID:52 .= |[(p `1),(q `2)]| `2 by EUCLID:52 ; then ((1 - d1) * p) + (d1 * |[(p `1),(q `2)]|) = |[(p `1),(q `2)]| by A4, Th6; hence x in {|[(p `1),(q `2)]|} by A2, TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {|[(p `1),(q `2)]|} or x in (LSeg (p,|[(p `1),(q `2)]|)) /\ (LSeg (|[(p `1),(q `2)]|,q)) ) assume x in {|[(p `1),(q `2)]|} ; ::_thesis: x in (LSeg (p,|[(p `1),(q `2)]|)) /\ (LSeg (|[(p `1),(q `2)]|,q)) then A5: x = |[(p `1),(q `2)]| by TARSKI:def_1; ( |[(p `1),(q `2)]| in LSeg (p,|[(p `1),(q `2)]|) & |[(p `1),(q `2)]| in LSeg (|[(p `1),(q `2)]|,q) ) by RLTOPSP1:68; hence x in (LSeg (p,|[(p `1),(q `2)]|)) /\ (LSeg (|[(p `1),(q `2)]|,q)) by A5, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th30: :: TOPREAL3:30 for p, q being Point of (TOP-REAL 2) holds (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (|[(q `1),(p `2)]|,q)) = {|[(q `1),(p `2)]|} proof let p, q be Point of (TOP-REAL 2); ::_thesis: (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (|[(q `1),(p `2)]|,q)) = {|[(q `1),(p `2)]|} set p3 = |[(q `1),(p `2)]|; set l23 = LSeg (p,|[(q `1),(p `2)]|); set l = LSeg (|[(q `1),(p `2)]|,q); thus (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (|[(q `1),(p `2)]|,q)) c= {|[(q `1),(p `2)]|} :: according to XBOOLE_0:def_10 ::_thesis: {|[(q `1),(p `2)]|} c= (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (|[(q `1),(p `2)]|,q)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (|[(q `1),(p `2)]|,q)) or x in {|[(q `1),(p `2)]|} ) assume A1: x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (|[(q `1),(p `2)]|,q)) ; ::_thesis: x in {|[(q `1),(p `2)]|} then x in LSeg (p,|[(q `1),(p `2)]|) by XBOOLE_0:def_4; then consider d1 being Real such that A2: x = ((1 - d1) * p) + (d1 * |[(q `1),(p `2)]|) and 0 <= d1 and d1 <= 1 ; x in LSeg (|[(q `1),(p `2)]|,q) by A1, XBOOLE_0:def_4; then consider d2 being Real such that A3: x = ((1 - d2) * |[(q `1),(p `2)]|) + (d2 * q) and 0 <= d2 and d2 <= 1 ; set t = ((1 - d1) * p) + (d1 * |[(q `1),(p `2)]|); A4: (((1 - d1) * p) + (d1 * |[(q `1),(p `2)]|)) `2 = (((1 - d1) * p) `2) + ((d1 * |[(q `1),(p `2)]|) `2) by Th2 .= ((1 - d1) * (p `2)) + ((d1 * |[(q `1),(p `2)]|) `2) by Th4 .= ((1 - d1) * (p `2)) + (d1 * (|[(q `1),(p `2)]| `2)) by Th4 .= ((1 - d1) * (|[(q `1),(p `2)]| `2)) + (d1 * (|[(q `1),(p `2)]| `2)) by EUCLID:52 .= |[(q `1),(p `2)]| `2 ; (((1 - d1) * p) + (d1 * |[(q `1),(p `2)]|)) `1 = (((1 - d2) * |[(q `1),(p `2)]|) `1) + ((d2 * q) `1) by A2, A3, Th2 .= ((1 - d2) * (|[(q `1),(p `2)]| `1)) + ((d2 * q) `1) by Th4 .= ((1 - d2) * (|[(q `1),(p `2)]| `1)) + (d2 * (q `1)) by Th4 .= ((1 - d2) * (|[(q `1),(p `2)]| `1)) + (d2 * (|[(q `1),(p `2)]| `1)) by EUCLID:52 .= |[(q `1),(p `2)]| `1 ; then ((1 - d1) * p) + (d1 * |[(q `1),(p `2)]|) = |[(q `1),(p `2)]| by A4, Th6; hence x in {|[(q `1),(p `2)]|} by A2, TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {|[(q `1),(p `2)]|} or x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (|[(q `1),(p `2)]|,q)) ) assume x in {|[(q `1),(p `2)]|} ; ::_thesis: x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (|[(q `1),(p `2)]|,q)) then A5: x = |[(q `1),(p `2)]| by TARSKI:def_1; ( |[(q `1),(p `2)]| in LSeg (p,|[(q `1),(p `2)]|) & |[(q `1),(p `2)]| in LSeg (|[(q `1),(p `2)]|,q) ) by RLTOPSP1:68; hence x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (|[(q `1),(p `2)]|,q)) by A5, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th31: :: TOPREAL3:31 for p, q being Point of (TOP-REAL 2) st p `1 = q `1 & p `2 <> q `2 holds (LSeg (p,|[(p `1),(((p `2) + (q `2)) / 2)]|)) /\ (LSeg (|[(p `1),(((p `2) + (q `2)) / 2)]|,q)) = {|[(p `1),(((p `2) + (q `2)) / 2)]|} proof let p, q be Point of (TOP-REAL 2); ::_thesis: ( p `1 = q `1 & p `2 <> q `2 implies (LSeg (p,|[(p `1),(((p `2) + (q `2)) / 2)]|)) /\ (LSeg (|[(p `1),(((p `2) + (q `2)) / 2)]|,q)) = {|[(p `1),(((p `2) + (q `2)) / 2)]|} ) assume that A1: p `1 = q `1 and A2: p `2 <> q `2 ; ::_thesis: (LSeg (p,|[(p `1),(((p `2) + (q `2)) / 2)]|)) /\ (LSeg (|[(p `1),(((p `2) + (q `2)) / 2)]|,q)) = {|[(p `1),(((p `2) + (q `2)) / 2)]|} set p3 = |[(p `1),(((p `2) + (q `2)) / 2)]|; set l23 = LSeg (p,|[(p `1),(((p `2) + (q `2)) / 2)]|); set l = LSeg (|[(p `1),(((p `2) + (q `2)) / 2)]|,q); thus (LSeg (p,|[(p `1),(((p `2) + (q `2)) / 2)]|)) /\ (LSeg (|[(p `1),(((p `2) + (q `2)) / 2)]|,q)) c= {|[(p `1),(((p `2) + (q `2)) / 2)]|} :: according to XBOOLE_0:def_10 ::_thesis: {|[(p `1),(((p `2) + (q `2)) / 2)]|} c= (LSeg (p,|[(p `1),(((p `2) + (q `2)) / 2)]|)) /\ (LSeg (|[(p `1),(((p `2) + (q `2)) / 2)]|,q)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (LSeg (p,|[(p `1),(((p `2) + (q `2)) / 2)]|)) /\ (LSeg (|[(p `1),(((p `2) + (q `2)) / 2)]|,q)) or x in {|[(p `1),(((p `2) + (q `2)) / 2)]|} ) A3: LSeg (p,|[(p `1),(((p `2) + (q `2)) / 2)]|) = LSeg (|[(p `1),(p `2)]|,|[(p `1),(((p `2) + (q `2)) / 2)]|) by EUCLID:53; assume A4: x in (LSeg (p,|[(p `1),(((p `2) + (q `2)) / 2)]|)) /\ (LSeg (|[(p `1),(((p `2) + (q `2)) / 2)]|,q)) ; ::_thesis: x in {|[(p `1),(((p `2) + (q `2)) / 2)]|} then A5: x in LSeg (|[(p `1),(((p `2) + (q `2)) / 2)]|,q) by XBOOLE_0:def_4; A6: LSeg (|[(p `1),(((p `2) + (q `2)) / 2)]|,q) = LSeg (|[(q `1),(((p `2) + (q `2)) / 2)]|,|[(q `1),(q `2)]|) by A1, EUCLID:53; A7: x in LSeg (p,|[(p `1),(((p `2) + (q `2)) / 2)]|) by A4, XBOOLE_0:def_4; now__::_thesis:_x_=_|[(p_`1),(((p_`2)_+_(q_`2))_/_2)]| percases ( p `2 < q `2 or p `2 > q `2 ) by A2, XXREAL_0:1; supposeA8: p `2 < q `2 ; ::_thesis: x = |[(p `1),(((p `2) + (q `2)) / 2)]| then p `2 < ((p `2) + (q `2)) / 2 by XREAL_1:226; then x in { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = p `1 & p `2 <= p1 `2 & p1 `2 <= ((p `2) + (q `2)) / 2 ) } by A7, A3, Th9; then consider t1 being Point of (TOP-REAL 2) such that A9: t1 = x and A10: t1 `1 = p `1 and p `2 <= t1 `2 and A11: t1 `2 <= ((p `2) + (q `2)) / 2 ; A12: t1 `2 <= |[(p `1),(((p `2) + (q `2)) / 2)]| `2 by A11, EUCLID:52; ((p `2) + (q `2)) / 2 < q `2 by A8, XREAL_1:226; then x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = q `1 & ((p `2) + (q `2)) / 2 <= p2 `2 & p2 `2 <= q `2 ) } by A5, A6, Th9; then ex t2 being Point of (TOP-REAL 2) st ( t2 = x & t2 `1 = q `1 & ((p `2) + (q `2)) / 2 <= t2 `2 & t2 `2 <= q `2 ) ; then t1 `2 >= |[(p `1),(((p `2) + (q `2)) / 2)]| `2 by A9, EUCLID:52; then A13: t1 `2 = |[(p `1),(((p `2) + (q `2)) / 2)]| `2 by A12, XXREAL_0:1; t1 `1 = |[(p `1),(((p `2) + (q `2)) / 2)]| `1 by A10, EUCLID:52; hence x = |[(p `1),(((p `2) + (q `2)) / 2)]| by A9, A13, Th6; ::_thesis: verum end; supposeA14: p `2 > q `2 ; ::_thesis: x = |[(p `1),(((p `2) + (q `2)) / 2)]| then p `2 > ((p `2) + (q `2)) / 2 by XREAL_1:226; then x in { p11 where p11 is Point of (TOP-REAL 2) : ( p11 `1 = p `1 & ((p `2) + (q `2)) / 2 <= p11 `2 & p11 `2 <= p `2 ) } by A7, A3, Th9; then consider t1 being Point of (TOP-REAL 2) such that A15: t1 = x and A16: t1 `1 = p `1 and A17: ((p `2) + (q `2)) / 2 <= t1 `2 and t1 `2 <= p `2 ; A18: |[(p `1),(((p `2) + (q `2)) / 2)]| `2 <= t1 `2 by A17, EUCLID:52; q `2 < ((p `2) + (q `2)) / 2 by A14, XREAL_1:226; then x in { p22 where p22 is Point of (TOP-REAL 2) : ( p22 `1 = q `1 & q `2 <= p22 `2 & p22 `2 <= ((p `2) + (q `2)) / 2 ) } by A5, A6, Th9; then ex t2 being Point of (TOP-REAL 2) st ( t2 = x & t2 `1 = q `1 & q `2 <= t2 `2 & t2 `2 <= ((p `2) + (q `2)) / 2 ) ; then t1 `2 <= |[(p `1),(((p `2) + (q `2)) / 2)]| `2 by A15, EUCLID:52; then A19: t1 `2 = |[(p `1),(((p `2) + (q `2)) / 2)]| `2 by A18, XXREAL_0:1; t1 `1 = |[(p `1),(((p `2) + (q `2)) / 2)]| `1 by A16, EUCLID:52; hence x = |[(p `1),(((p `2) + (q `2)) / 2)]| by A15, A19, Th6; ::_thesis: verum end; end; end; hence x in {|[(p `1),(((p `2) + (q `2)) / 2)]|} by TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {|[(p `1),(((p `2) + (q `2)) / 2)]|} or x in (LSeg (p,|[(p `1),(((p `2) + (q `2)) / 2)]|)) /\ (LSeg (|[(p `1),(((p `2) + (q `2)) / 2)]|,q)) ) assume x in {|[(p `1),(((p `2) + (q `2)) / 2)]|} ; ::_thesis: x in (LSeg (p,|[(p `1),(((p `2) + (q `2)) / 2)]|)) /\ (LSeg (|[(p `1),(((p `2) + (q `2)) / 2)]|,q)) then A20: x = |[(p `1),(((p `2) + (q `2)) / 2)]| by TARSKI:def_1; ( |[(p `1),(((p `2) + (q `2)) / 2)]| in LSeg (p,|[(p `1),(((p `2) + (q `2)) / 2)]|) & |[(p `1),(((p `2) + (q `2)) / 2)]| in LSeg (|[(p `1),(((p `2) + (q `2)) / 2)]|,q) ) by RLTOPSP1:68; hence x in (LSeg (p,|[(p `1),(((p `2) + (q `2)) / 2)]|)) /\ (LSeg (|[(p `1),(((p `2) + (q `2)) / 2)]|,q)) by A20, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th32: :: TOPREAL3:32 for p, q being Point of (TOP-REAL 2) st p `1 <> q `1 & p `2 = q `2 holds (LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|)) /\ (LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q)) = {|[(((p `1) + (q `1)) / 2),(p `2)]|} proof let p, q be Point of (TOP-REAL 2); ::_thesis: ( p `1 <> q `1 & p `2 = q `2 implies (LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|)) /\ (LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q)) = {|[(((p `1) + (q `1)) / 2),(p `2)]|} ) assume that A1: p `1 <> q `1 and A2: p `2 = q `2 ; ::_thesis: (LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|)) /\ (LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q)) = {|[(((p `1) + (q `1)) / 2),(p `2)]|} set p3 = |[(((p `1) + (q `1)) / 2),(p `2)]|; set l23 = LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|); set l = LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q); thus (LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|)) /\ (LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q)) c= {|[(((p `1) + (q `1)) / 2),(p `2)]|} :: according to XBOOLE_0:def_10 ::_thesis: {|[(((p `1) + (q `1)) / 2),(p `2)]|} c= (LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|)) /\ (LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|)) /\ (LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q)) or x in {|[(((p `1) + (q `1)) / 2),(p `2)]|} ) A3: LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|) = LSeg (|[(p `1),(p `2)]|,|[(((p `1) + (q `1)) / 2),(p `2)]|) by EUCLID:53; assume A4: x in (LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|)) /\ (LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q)) ; ::_thesis: x in {|[(((p `1) + (q `1)) / 2),(p `2)]|} then A5: x in LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q) by XBOOLE_0:def_4; A6: LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q) = LSeg (|[(((p `1) + (q `1)) / 2),(q `2)]|,|[(q `1),(q `2)]|) by A2, EUCLID:53; A7: x in LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|) by A4, XBOOLE_0:def_4; now__::_thesis:_x_=_|[(((p_`1)_+_(q_`1))_/_2),(p_`2)]| percases ( p `1 < q `1 or p `1 > q `1 ) by A1, XXREAL_0:1; supposeA8: p `1 < q `1 ; ::_thesis: x = |[(((p `1) + (q `1)) / 2),(p `2)]| then p `1 < ((p `1) + (q `1)) / 2 by XREAL_1:226; then x in { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `2 = p `2 & p `1 <= p1 `1 & p1 `1 <= ((p `1) + (q `1)) / 2 ) } by A7, A3, Th10; then consider t1 being Point of (TOP-REAL 2) such that A9: t1 = x and A10: t1 `2 = p `2 and p `1 <= t1 `1 and A11: t1 `1 <= ((p `1) + (q `1)) / 2 ; A12: t1 `1 <= |[(((p `1) + (q `1)) / 2),(p `2)]| `1 by A11, EUCLID:52; ((p `1) + (q `1)) / 2 < q `1 by A8, XREAL_1:226; then x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = q `2 & ((p `1) + (q `1)) / 2 <= p2 `1 & p2 `1 <= q `1 ) } by A5, A6, Th10; then ex t2 being Point of (TOP-REAL 2) st ( t2 = x & t2 `2 = q `2 & ((p `1) + (q `1)) / 2 <= t2 `1 & t2 `1 <= q `1 ) ; then t1 `1 >= |[(((p `1) + (q `1)) / 2),(p `2)]| `1 by A9, EUCLID:52; then A13: t1 `1 = |[(((p `1) + (q `1)) / 2),(p `2)]| `1 by A12, XXREAL_0:1; t1 `2 = |[(((p `1) + (q `1)) / 2),(p `2)]| `2 by A10, EUCLID:52; hence x = |[(((p `1) + (q `1)) / 2),(p `2)]| by A9, A13, Th6; ::_thesis: verum end; supposeA14: p `1 > q `1 ; ::_thesis: x = |[(((p `1) + (q `1)) / 2),(p `2)]| then p `1 > ((p `1) + (q `1)) / 2 by XREAL_1:226; then x in { p11 where p11 is Point of (TOP-REAL 2) : ( p11 `2 = p `2 & ((p `1) + (q `1)) / 2 <= p11 `1 & p11 `1 <= p `1 ) } by A7, A3, Th10; then consider t1 being Point of (TOP-REAL 2) such that A15: t1 = x and A16: t1 `2 = p `2 and A17: ((p `1) + (q `1)) / 2 <= t1 `1 and t1 `1 <= p `1 ; A18: |[(((p `1) + (q `1)) / 2),(p `2)]| `1 <= t1 `1 by A17, EUCLID:52; q `1 < ((p `1) + (q `1)) / 2 by A14, XREAL_1:226; then x in { p22 where p22 is Point of (TOP-REAL 2) : ( p22 `2 = q `2 & q `1 <= p22 `1 & p22 `1 <= ((p `1) + (q `1)) / 2 ) } by A5, A6, Th10; then ex t2 being Point of (TOP-REAL 2) st ( t2 = x & t2 `2 = q `2 & q `1 <= t2 `1 & t2 `1 <= ((p `1) + (q `1)) / 2 ) ; then t1 `1 <= |[(((p `1) + (q `1)) / 2),(p `2)]| `1 by A15, EUCLID:52; then A19: t1 `1 = |[(((p `1) + (q `1)) / 2),(p `2)]| `1 by A18, XXREAL_0:1; t1 `2 = |[(((p `1) + (q `1)) / 2),(p `2)]| `2 by A16, EUCLID:52; hence x = |[(((p `1) + (q `1)) / 2),(p `2)]| by A15, A19, Th6; ::_thesis: verum end; end; end; hence x in {|[(((p `1) + (q `1)) / 2),(p `2)]|} by TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {|[(((p `1) + (q `1)) / 2),(p `2)]|} or x in (LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|)) /\ (LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q)) ) assume x in {|[(((p `1) + (q `1)) / 2),(p `2)]|} ; ::_thesis: x in (LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|)) /\ (LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q)) then A20: x = |[(((p `1) + (q `1)) / 2),(p `2)]| by TARSKI:def_1; ( |[(((p `1) + (q `1)) / 2),(p `2)]| in LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|) & |[(((p `1) + (q `1)) / 2),(p `2)]| in LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q) ) by RLTOPSP1:68; hence x in (LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|)) /\ (LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q)) by A20, XBOOLE_0:def_4; ::_thesis: verum end; theorem :: TOPREAL3:33 for f being FinSequence of (TOP-REAL 2) for i being Element of NAT st i > 2 & i in dom f & f is being_S-Seq holds f | i is being_S-Seq proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for i being Element of NAT st i > 2 & i in dom f & f is being_S-Seq holds f | i is being_S-Seq let i be Element of NAT ; ::_thesis: ( i > 2 & i in dom f & f is being_S-Seq implies f | i is being_S-Seq ) assume that A1: i > 2 and A2: i in dom f and A3: f is being_S-Seq ; ::_thesis: f | i is being_S-Seq A4: f | i = f | (Seg i) by FINSEQ_1:def_15; then A5: dom (f | i) = (dom f) /\ (Seg i) by RELAT_1:61; thus f | i is one-to-one :: according to TOPREAL1:def_8 ::_thesis: ( 2 <= len (f | i) & f | i is unfolded & f | i is s.n.c. & f | i is special ) proof A6: f is one-to-one by A3, TOPREAL1:def_8; let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds ( not x in dom (f | i) or not b1 in dom (f | i) or not (f | i) . x = (f | i) . b1 or x = b1 ) let y be set ; ::_thesis: ( not x in dom (f | i) or not y in dom (f | i) or not (f | i) . x = (f | i) . y or x = y ) assume that A7: x in dom (f | i) and A8: y in dom (f | i) and A9: (f | i) . x = (f | i) . y ; ::_thesis: x = y A10: ( x in dom f & y in dom f ) by A5, A7, A8, XBOOLE_0:def_4; f . x = (f | i) . x by A4, A7, FUNCT_1:47 .= f . y by A4, A8, A9, FUNCT_1:47 ; hence x = y by A6, A10, FUNCT_1:def_4; ::_thesis: verum end; A11: i <= len f by A2, FINSEQ_3:25; Seg (len f) = dom f by FINSEQ_1:def_3; then Seg i c= dom f by A11, FINSEQ_1:5; then A12: dom (f | i) = Seg i by A5, XBOOLE_1:28; hence len (f | i) >= 2 by A1, FINSEQ_1:def_3; ::_thesis: ( f | i is unfolded & f | i is s.n.c. & f | i is special ) A13: f is unfolded by A3, TOPREAL1:def_8; thus f | i is unfolded ::_thesis: ( f | i is s.n.c. & f | i is special ) proof let j be Nat; :: according to TOPREAL1:def_6 ::_thesis: ( not 1 <= j or not j + 2 <= len (f | i) or (LSeg ((f | i),j)) /\ (LSeg ((f | i),(j + 1))) = {((f | i) /. (j + 1))} ) assume that A14: 1 <= j and A15: j + 2 <= len (f | i) ; ::_thesis: (LSeg ((f | i),j)) /\ (LSeg ((f | i),(j + 1))) = {((f | i) /. (j + 1))} j + 1 <= j + 2 by XREAL_1:6; then A16: j + 1 <= len (f | i) by A15, XXREAL_0:2; len (f | i) <= len f by A11, A12, FINSEQ_1:def_3; then A17: j + 2 <= len f by A15, XXREAL_0:2; 1 <= j + 1 by NAT_1:12; then A18: j + 1 in dom (f | i) by A16, FINSEQ_3:25; 1 <= (j + 1) + 1 by NAT_1:12; then (j + 1) + 1 in dom (f | i) by A15, FINSEQ_3:25; then A19: LSeg (f,(j + 1)) = LSeg ((f | i),(j + 1)) by A18, Th17; j <= j + 2 by NAT_1:11; then j <= len (f | i) by A15, XXREAL_0:2; then j in dom (f | i) by A14, FINSEQ_3:25; then LSeg (f,j) = LSeg ((f | i),j) by A18, Th17; then (LSeg ((f | i),j)) /\ (LSeg ((f | i),(j + 1))) = {(f /. (j + 1))} by A13, A14, A17, A19, TOPREAL1:def_6; hence (LSeg ((f | i),j)) /\ (LSeg ((f | i),(j + 1))) = {((f | i) /. (j + 1))} by A18, FINSEQ_4:70; ::_thesis: verum end; A20: f is s.n.c. by A3, TOPREAL1:def_8; thus f | i is s.n.c. ::_thesis: f | i is special proof let n, k be Nat; :: according to TOPREAL1:def_7 ::_thesis: ( k <= n + 1 or LSeg ((f | i),n) misses LSeg ((f | i),k) ) A21: k + 1 >= 1 by NAT_1:11; A22: n + 1 >= 1 by NAT_1:11; assume n + 1 < k ; ::_thesis: LSeg ((f | i),n) misses LSeg ((f | i),k) then LSeg (f,n) misses LSeg (f,k) by A20, TOPREAL1:def_7; then A23: (LSeg (f,n)) /\ (LSeg (f,k)) = {} by XBOOLE_0:def_7; A24: k + 1 >= k by NAT_1:11; A25: n + 1 >= n by NAT_1:11; percases ( n in dom (f | i) or not n in dom (f | i) ) ; supposeA26: n in dom (f | i) ; ::_thesis: LSeg ((f | i),n) misses LSeg ((f | i),k) now__::_thesis:_(LSeg_((f_|_i),n))_/\_(LSeg_((f_|_i),k))_=_{} percases ( n + 1 in dom (f | i) or not n + 1 in dom (f | i) ) ; suppose n + 1 in dom (f | i) ; ::_thesis: (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {} then A27: LSeg (f,n) = LSeg ((f | i),n) by A26, Th17; now__::_thesis:_(LSeg_((f_|_i),n))_/\_(LSeg_((f_|_i),k))_=_{} percases ( k in dom (f | i) or not k in dom (f | i) ) ; supposeA28: k in dom (f | i) ; ::_thesis: (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {} now__::_thesis:_(LSeg_((f_|_i),n))_/\_(LSeg_((f_|_i),k))_=_{} percases ( k + 1 in dom (f | i) or not k + 1 in dom (f | i) ) ; suppose k + 1 in dom (f | i) ; ::_thesis: (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {} hence (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {} by A23, A27, A28, Th17; ::_thesis: verum end; suppose not k + 1 in dom (f | i) ; ::_thesis: (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {} then k + 1 > len (f | i) by A21, FINSEQ_3:25; then LSeg ((f | i),k) = {} by TOPREAL1:def_3; hence (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {} ; ::_thesis: verum end; end; end; hence (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {} ; ::_thesis: verum end; suppose not k in dom (f | i) ; ::_thesis: (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {} then ( k < 1 or k > len (f | i) ) by FINSEQ_3:25; then ( k < 1 or k + 1 > len (f | i) ) by A24, XXREAL_0:2; then LSeg ((f | i),k) = {} by TOPREAL1:def_3; hence (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {} ; ::_thesis: verum end; end; end; hence (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {} ; ::_thesis: verum end; suppose not n + 1 in dom (f | i) ; ::_thesis: (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {} then n + 1 > len (f | i) by A22, FINSEQ_3:25; then LSeg ((f | i),n) = {} by TOPREAL1:def_3; hence (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {} ; ::_thesis: verum end; end; end; hence (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: verum end; suppose not n in dom (f | i) ; ::_thesis: LSeg ((f | i),n) misses LSeg ((f | i),k) then ( n < 1 or n > len (f | i) ) by FINSEQ_3:25; then ( n < 1 or n + 1 > len (f | i) ) by A25, XXREAL_0:2; then LSeg ((f | i),n) = {} by TOPREAL1:def_3; hence (LSeg ((f | i),n)) /\ (LSeg ((f | i),k)) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: verum end; end; end; let j be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( not 1 <= j or not j + 1 <= len (f | i) or ((f | i) /. j) `1 = ((f | i) /. (j + 1)) `1 or ((f | i) /. j) `2 = ((f | i) /. (j + 1)) `2 ) assume that A29: 1 <= j and A30: j + 1 <= len (f | i) ; ::_thesis: ( ((f | i) /. j) `1 = ((f | i) /. (j + 1)) `1 or ((f | i) /. j) `2 = ((f | i) /. (j + 1)) `2 ) len (f | i) <= len f by A11, A12, FINSEQ_1:def_3; then A31: j + 1 <= len f by A30, XXREAL_0:2; j <= j + 1 by NAT_1:11; then j <= len (f | i) by A30, XXREAL_0:2; then j in dom (f | i) by A29, FINSEQ_3:25; then A32: (f | i) /. j = f /. j by FINSEQ_4:70; 1 <= j + 1 by NAT_1:12; then j + 1 in dom (f | i) by A30, FINSEQ_3:25; then A33: (f | i) /. (j + 1) = f /. (j + 1) by FINSEQ_4:70; f is special by A3, TOPREAL1:def_8; hence ( ((f | i) /. j) `1 = ((f | i) /. (j + 1)) `1 or ((f | i) /. j) `2 = ((f | i) /. (j + 1)) `2 ) by A29, A31, A32, A33, TOPREAL1:def_5; ::_thesis: verum end; theorem :: TOPREAL3:34 for p, q being Point of (TOP-REAL 2) for f being FinSequence of (TOP-REAL 2) st p `1 <> q `1 & p `2 <> q `2 & f = <*p,|[(p `1),(q `2)]|,q*> holds ( f /. 1 = p & f /. (len f) = q & f is being_S-Seq ) proof let p, q be Point of (TOP-REAL 2); ::_thesis: for f being FinSequence of (TOP-REAL 2) st p `1 <> q `1 & p `2 <> q `2 & f = <*p,|[(p `1),(q `2)]|,q*> holds ( f /. 1 = p & f /. (len f) = q & f is being_S-Seq ) let f be FinSequence of (TOP-REAL 2); ::_thesis: ( p `1 <> q `1 & p `2 <> q `2 & f = <*p,|[(p `1),(q `2)]|,q*> implies ( f /. 1 = p & f /. (len f) = q & f is being_S-Seq ) ) set p1 = |[(p `1),(q `2)]|; assume that A1: p `1 <> q `1 and A2: p `2 <> q `2 and A3: f = <*p,|[(p `1),(q `2)]|,q*> ; ::_thesis: ( f /. 1 = p & f /. (len f) = q & f is being_S-Seq ) A4: len f = 1 + 2 by A3, FINSEQ_1:45; hence ( f /. 1 = p & f /. (len f) = q ) by A3, FINSEQ_4:18; ::_thesis: f is being_S-Seq ( p <> |[(p `1),(q `2)]| & q <> |[(p `1),(q `2)]| ) by A1, A2, EUCLID:52; hence ( f is one-to-one & len f >= 2 ) by A1, A3, A4, FINSEQ_3:95; :: according to TOPREAL1:def_8 ::_thesis: ( f is unfolded & f is s.n.c. & f is special ) A5: f /. 2 = |[(p `1),(q `2)]| by A3, FINSEQ_4:18; A6: f /. 3 = q by A3, FINSEQ_4:18; A7: f /. 1 = p by A3, FINSEQ_4:18; thus f is unfolded ::_thesis: ( f is s.n.c. & f is special ) proof 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 that A8: 1 <= i and A9: i + 2 <= len f ; ::_thesis: (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} i <= 1 by A4, A9, XREAL_1:6; then A10: i = 1 by A8, XXREAL_0:1; hence (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = (LSeg (p,|[(p `1),(q `2)]|)) /\ (LSeg (f,2)) by A4, A7, A5, TOPREAL1:def_3 .= (LSeg (p,|[(p `1),(q `2)]|)) /\ (LSeg (|[(p `1),(q `2)]|,q)) by A4, A5, A6, TOPREAL1:def_3 .= {(f /. (i + 1))} by A5, A10, Th29 ; ::_thesis: verum end; thus f is s.n.c. ::_thesis: f is special proof let i, j be Nat; :: according to TOPREAL1:def_7 ::_thesis: ( j <= i + 1 or LSeg (f,i) misses LSeg (f,j) ) assume A11: i + 1 < j ; ::_thesis: LSeg (f,i) misses LSeg (f,j) now__::_thesis:_LSeg_(f,i)_misses_LSeg_(f,j) percases ( i = 0 or i <> 0 ) ; suppose i = 0 ; ::_thesis: LSeg (f,i) misses LSeg (f,j) then LSeg (f,i) = {} by TOPREAL1:def_3; then (LSeg (f,i)) /\ (LSeg (f,j)) = {} ; hence LSeg (f,i) misses LSeg (f,j) by XBOOLE_0:def_7; ::_thesis: verum end; suppose i <> 0 ; ::_thesis: LSeg (f,i) misses LSeg (f,j) then LSeg (f,j) = {} by A3, A11, Th15; then (LSeg (f,i)) /\ (LSeg (f,j)) = {} ; hence LSeg (f,i) misses LSeg (f,j) by XBOOLE_0:def_7; ::_thesis: verum end; end; end; hence LSeg (f,i) misses LSeg (f,j) ; ::_thesis: verum end; let i be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( not 1 <= i or not i + 1 <= len f or (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) assume that A12: 1 <= i and A13: i + 1 <= len f ; ::_thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) A14: i <= 2 by A4, A13, XREAL_1:6; percases ( i = 1 or i = 2 ) by A12, A14, NAT_1:26; suppose i = 1 ; ::_thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) hence ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A7, A5, EUCLID:52; ::_thesis: verum end; suppose i = 2 ; ::_thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) hence ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A5, A6, EUCLID:52; ::_thesis: verum end; end; end; theorem :: TOPREAL3:35 for p, q being Point of (TOP-REAL 2) for f being FinSequence of (TOP-REAL 2) st p `1 <> q `1 & p `2 <> q `2 & f = <*p,|[(q `1),(p `2)]|,q*> holds ( f /. 1 = p & f /. (len f) = q & f is being_S-Seq ) proof let p, q be Point of (TOP-REAL 2); ::_thesis: for f being FinSequence of (TOP-REAL 2) st p `1 <> q `1 & p `2 <> q `2 & f = <*p,|[(q `1),(p `2)]|,q*> holds ( f /. 1 = p & f /. (len f) = q & f is being_S-Seq ) let f be FinSequence of (TOP-REAL 2); ::_thesis: ( p `1 <> q `1 & p `2 <> q `2 & f = <*p,|[(q `1),(p `2)]|,q*> implies ( f /. 1 = p & f /. (len f) = q & f is being_S-Seq ) ) set p1 = |[(q `1),(p `2)]|; assume that A1: p `1 <> q `1 and A2: p `2 <> q `2 and A3: f = <*p,|[(q `1),(p `2)]|,q*> ; ::_thesis: ( f /. 1 = p & f /. (len f) = q & f is being_S-Seq ) A4: len f = 1 + 2 by A3, FINSEQ_1:45; hence ( f /. 1 = p & f /. (len f) = q ) by A3, FINSEQ_4:18; ::_thesis: f is being_S-Seq ( p <> |[(q `1),(p `2)]| & q <> |[(q `1),(p `2)]| ) by A1, A2, EUCLID:52; hence ( f is one-to-one & len f >= 2 ) by A1, A3, A4, FINSEQ_3:95; :: according to TOPREAL1:def_8 ::_thesis: ( f is unfolded & f is s.n.c. & f is special ) A5: f /. 2 = |[(q `1),(p `2)]| by A3, FINSEQ_4:18; A6: f /. 3 = q by A3, FINSEQ_4:18; A7: f /. 1 = p by A3, FINSEQ_4:18; thus f is unfolded ::_thesis: ( f is s.n.c. & f is special ) proof 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 that A8: 1 <= i and A9: i + 2 <= len f ; ::_thesis: (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} i <= 1 by A4, A9, XREAL_1:6; then A10: i = 1 by A8, XXREAL_0:1; hence (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (f,2)) by A4, A7, A5, TOPREAL1:def_3 .= (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (|[(q `1),(p `2)]|,q)) by A4, A5, A6, TOPREAL1:def_3 .= {(f /. (i + 1))} by A5, A10, Th30 ; ::_thesis: verum end; thus f is s.n.c. ::_thesis: f is special proof let i, j be Nat; :: according to TOPREAL1:def_7 ::_thesis: ( j <= i + 1 or LSeg (f,i) misses LSeg (f,j) ) assume A11: i + 1 < j ; ::_thesis: LSeg (f,i) misses LSeg (f,j) now__::_thesis:_LSeg_(f,i)_misses_LSeg_(f,j) percases ( i = 0 or i <> 0 ) ; suppose i = 0 ; ::_thesis: LSeg (f,i) misses LSeg (f,j) then LSeg (f,i) = {} by TOPREAL1:def_3; then (LSeg (f,i)) /\ (LSeg (f,j)) = {} ; hence LSeg (f,i) misses LSeg (f,j) by XBOOLE_0:def_7; ::_thesis: verum end; suppose i <> 0 ; ::_thesis: LSeg (f,i) misses LSeg (f,j) then LSeg (f,j) = {} by A3, A11, Th15; then (LSeg (f,i)) /\ (LSeg (f,j)) = {} ; hence LSeg (f,i) misses LSeg (f,j) by XBOOLE_0:def_7; ::_thesis: verum end; end; end; hence LSeg (f,i) misses LSeg (f,j) ; ::_thesis: verum end; let i be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( not 1 <= i or not i + 1 <= len f or (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) assume that A12: 1 <= i and A13: i + 1 <= len f ; ::_thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) A14: i <= 2 by A4, A13, XREAL_1:6; percases ( i = 1 or i = 2 ) by A12, A14, NAT_1:26; suppose i = 1 ; ::_thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) hence ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A7, A5, EUCLID:52; ::_thesis: verum end; suppose i = 2 ; ::_thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) hence ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A5, A6, EUCLID:52; ::_thesis: verum end; end; end; theorem :: TOPREAL3:36 for p, q being Point of (TOP-REAL 2) for f being FinSequence of (TOP-REAL 2) st p `1 = q `1 & p `2 <> q `2 & f = <*p,|[(p `1),(((p `2) + (q `2)) / 2)]|,q*> holds ( f /. 1 = p & f /. (len f) = q & f is being_S-Seq ) proof let p, q be Point of (TOP-REAL 2); ::_thesis: for f being FinSequence of (TOP-REAL 2) st p `1 = q `1 & p `2 <> q `2 & f = <*p,|[(p `1),(((p `2) + (q `2)) / 2)]|,q*> holds ( f /. 1 = p & f /. (len f) = q & f is being_S-Seq ) let f be FinSequence of (TOP-REAL 2); ::_thesis: ( p `1 = q `1 & p `2 <> q `2 & f = <*p,|[(p `1),(((p `2) + (q `2)) / 2)]|,q*> implies ( f /. 1 = p & f /. (len f) = q & f is being_S-Seq ) ) set p1 = |[(p `1),(((p `2) + (q `2)) / 2)]|; assume that A1: p `1 = q `1 and A2: p `2 <> q `2 and A3: f = <*p,|[(p `1),(((p `2) + (q `2)) / 2)]|,q*> ; ::_thesis: ( f /. 1 = p & f /. (len f) = q & f is being_S-Seq ) A4: |[(p `1),(((p `2) + (q `2)) / 2)]| `2 = ((p `2) + (q `2)) / 2 by EUCLID:52; A5: len f = 1 + 2 by A3, FINSEQ_1:45; hence ( f /. 1 = p & f /. (len f) = q ) by A3, FINSEQ_4:18; ::_thesis: f is being_S-Seq ( p `2 <> ((p `2) + (q `2)) / 2 & q `2 <> ((p `2) + (q `2)) / 2 ) by A2; hence ( f is one-to-one & len f >= 2 ) by A2, A3, A5, A4, FINSEQ_3:95; :: according to TOPREAL1:def_8 ::_thesis: ( f is unfolded & f is s.n.c. & f is special ) A6: f /. 2 = |[(p `1),(((p `2) + (q `2)) / 2)]| by A3, FINSEQ_4:18; A7: f /. 3 = q by A3, FINSEQ_4:18; A8: f /. 1 = p by A3, FINSEQ_4:18; thus f is unfolded ::_thesis: ( f is s.n.c. & f is special ) proof 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 that A9: 1 <= i and A10: i + 2 <= len f ; ::_thesis: (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} i <= 1 by A5, A10, XREAL_1:6; then A11: i = 1 by A9, XXREAL_0:1; hence (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = (LSeg (p,|[(p `1),(((p `2) + (q `2)) / 2)]|)) /\ (LSeg (f,2)) by A5, A8, A6, TOPREAL1:def_3 .= (LSeg (p,|[(p `1),(((p `2) + (q `2)) / 2)]|)) /\ (LSeg (|[(p `1),(((p `2) + (q `2)) / 2)]|,q)) by A5, A6, A7, TOPREAL1:def_3 .= {(f /. (i + 1))} by A1, A2, A6, A11, Th31 ; ::_thesis: verum end; thus f is s.n.c. ::_thesis: f is special proof let i, j be Nat; :: according to TOPREAL1:def_7 ::_thesis: ( j <= i + 1 or LSeg (f,i) misses LSeg (f,j) ) assume A12: i + 1 < j ; ::_thesis: LSeg (f,i) misses LSeg (f,j) now__::_thesis:_LSeg_(f,i)_misses_LSeg_(f,j) percases ( i = 0 or i <> 0 ) ; suppose i = 0 ; ::_thesis: LSeg (f,i) misses LSeg (f,j) then LSeg (f,i) = {} by TOPREAL1:def_3; then (LSeg (f,i)) /\ (LSeg (f,j)) = {} ; hence LSeg (f,i) misses LSeg (f,j) by XBOOLE_0:def_7; ::_thesis: verum end; suppose i <> 0 ; ::_thesis: LSeg (f,i) misses LSeg (f,j) then LSeg (f,j) = {} by A3, A12, Th15; then (LSeg (f,i)) /\ (LSeg (f,j)) = {} ; hence LSeg (f,i) misses LSeg (f,j) by XBOOLE_0:def_7; ::_thesis: verum end; end; end; hence LSeg (f,i) misses LSeg (f,j) ; ::_thesis: verum end; let i be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( not 1 <= i or not i + 1 <= len f or (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) assume that A13: 1 <= i and A14: i + 1 <= len f ; ::_thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) A15: i <= 2 by A5, A14, XREAL_1:6; percases ( i = 1 or i = 2 ) by A13, A15, NAT_1:26; suppose i = 1 ; ::_thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) hence ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A8, A6, EUCLID:52; ::_thesis: verum end; suppose i = 2 ; ::_thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) hence ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A1, A6, A7, EUCLID:52; ::_thesis: verum end; end; end; theorem :: TOPREAL3:37 for p, q being Point of (TOP-REAL 2) for f being FinSequence of (TOP-REAL 2) st p `1 <> q `1 & p `2 = q `2 & f = <*p,|[(((p `1) + (q `1)) / 2),(p `2)]|,q*> holds ( f /. 1 = p & f /. (len f) = q & f is being_S-Seq ) proof let p, q be Point of (TOP-REAL 2); ::_thesis: for f being FinSequence of (TOP-REAL 2) st p `1 <> q `1 & p `2 = q `2 & f = <*p,|[(((p `1) + (q `1)) / 2),(p `2)]|,q*> holds ( f /. 1 = p & f /. (len f) = q & f is being_S-Seq ) let f be FinSequence of (TOP-REAL 2); ::_thesis: ( p `1 <> q `1 & p `2 = q `2 & f = <*p,|[(((p `1) + (q `1)) / 2),(p `2)]|,q*> implies ( f /. 1 = p & f /. (len f) = q & f is being_S-Seq ) ) set p1 = |[(((p `1) + (q `1)) / 2),(p `2)]|; assume that A1: p `1 <> q `1 and A2: p `2 = q `2 and A3: f = <*p,|[(((p `1) + (q `1)) / 2),(p `2)]|,q*> ; ::_thesis: ( f /. 1 = p & f /. (len f) = q & f is being_S-Seq ) A4: |[(((p `1) + (q `1)) / 2),(p `2)]| `1 = ((p `1) + (q `1)) / 2 by EUCLID:52; A5: len f = 1 + 2 by A3, FINSEQ_1:45; hence ( f /. 1 = p & f /. (len f) = q ) by A3, FINSEQ_4:18; ::_thesis: f is being_S-Seq ( p `1 <> ((p `1) + (q `1)) / 2 & q `1 <> ((p `1) + (q `1)) / 2 ) by A1; hence ( f is one-to-one & len f >= 2 ) by A1, A3, A5, A4, FINSEQ_3:95; :: according to TOPREAL1:def_8 ::_thesis: ( f is unfolded & f is s.n.c. & f is special ) A6: f /. 2 = |[(((p `1) + (q `1)) / 2),(p `2)]| by A3, FINSEQ_4:18; A7: f /. 3 = q by A3, FINSEQ_4:18; A8: f /. 1 = p by A3, FINSEQ_4:18; thus f is unfolded ::_thesis: ( f is s.n.c. & f is special ) proof 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 that A9: 1 <= i and A10: i + 2 <= len f ; ::_thesis: (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = {(f /. (i + 1))} i <= 1 by A5, A10, XREAL_1:6; then A11: i = 1 by A9, XXREAL_0:1; hence (LSeg (f,i)) /\ (LSeg (f,(i + 1))) = (LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|)) /\ (LSeg (f,2)) by A5, A8, A6, TOPREAL1:def_3 .= (LSeg (p,|[(((p `1) + (q `1)) / 2),(p `2)]|)) /\ (LSeg (|[(((p `1) + (q `1)) / 2),(p `2)]|,q)) by A5, A6, A7, TOPREAL1:def_3 .= {(f /. (i + 1))} by A1, A2, A6, A11, Th32 ; ::_thesis: verum end; thus f is s.n.c. ::_thesis: f is special proof let i, j be Nat; :: according to TOPREAL1:def_7 ::_thesis: ( j <= i + 1 or LSeg (f,i) misses LSeg (f,j) ) assume A12: i + 1 < j ; ::_thesis: LSeg (f,i) misses LSeg (f,j) now__::_thesis:_LSeg_(f,i)_misses_LSeg_(f,j) percases ( i = 0 or i <> 0 ) ; suppose i = 0 ; ::_thesis: LSeg (f,i) misses LSeg (f,j) then LSeg (f,i) = {} by TOPREAL1:def_3; then (LSeg (f,i)) /\ (LSeg (f,j)) = {} ; hence LSeg (f,i) misses LSeg (f,j) by XBOOLE_0:def_7; ::_thesis: verum end; suppose i <> 0 ; ::_thesis: LSeg (f,i) misses LSeg (f,j) then LSeg (f,j) = {} by A3, A12, Th15; then (LSeg (f,i)) /\ (LSeg (f,j)) = {} ; hence LSeg (f,i) misses LSeg (f,j) by XBOOLE_0:def_7; ::_thesis: verum end; end; end; hence LSeg (f,i) misses LSeg (f,j) ; ::_thesis: verum end; let i be Nat; :: according to TOPREAL1:def_5 ::_thesis: ( not 1 <= i or not i + 1 <= len f or (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) assume that A13: 1 <= i and A14: i + 1 <= len f ; ::_thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) A15: i <= 2 by A5, A14, XREAL_1:6; percases ( i = 1 or i = 2 ) by A13, A15, NAT_1:26; suppose i = 1 ; ::_thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) hence ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A8, A6, EUCLID:52; ::_thesis: verum end; suppose i = 2 ; ::_thesis: ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) hence ( (f /. i) `1 = (f /. (i + 1)) `1 or (f /. i) `2 = (f /. (i + 1)) `2 ) by A2, A6, A7, EUCLID:52; ::_thesis: verum end; end; end; theorem :: TOPREAL3:38 for f being FinSequence of (TOP-REAL 2) for i being Element of NAT st i in dom f & i + 1 in dom f holds L~ (f | (i + 1)) = (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1)))) proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for i being Element of NAT st i in dom f & i + 1 in dom f holds L~ (f | (i + 1)) = (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1)))) let i be Element of NAT ; ::_thesis: ( i in dom f & i + 1 in dom f implies L~ (f | (i + 1)) = (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1)))) ) set M1 = { (LSeg ((f | (i + 1)),k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len (f | (i + 1)) ) } ; set Mi = { (LSeg ((f | i),n)) where n is Element of NAT : ( 1 <= n & n + 1 <= len (f | i) ) } ; assume that A1: i in dom f and A2: i + 1 in dom f ; ::_thesis: L~ (f | (i + 1)) = (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1)))) set p = f /. i; set q = f /. (i + 1); A3: i + 1 <= len f by A2, FINSEQ_3:25; then Seg (i + 1) c= Seg (len f) by FINSEQ_1:5; then Seg (i + 1) c= dom f by FINSEQ_1:def_3; then Seg (i + 1) = (dom f) /\ (Seg (i + 1)) by XBOOLE_1:28; then A4: ( f | (i + 1) = f | (Seg (i + 1)) & Seg (i + 1) = dom (f | (Seg (i + 1))) ) by FINSEQ_1:def_15, RELAT_1:61; then A5: i + 1 = len (f | (i + 1)) by FINSEQ_1:def_3; A6: 1 <= i by A1, FINSEQ_3:25; then A7: LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A3, TOPREAL1:def_3; 1 <= i + 1 by A2, FINSEQ_3:25; then A8: i + 1 in dom (f | (i + 1)) by A5, FINSEQ_3:25; A9: i <= i + 1 by NAT_1:11; then i in dom (f | (i + 1)) by A6, A5, FINSEQ_3:25; then A10: LSeg ((f | (i + 1)),i) = LSeg ((f /. i),(f /. (i + 1))) by A7, A8, Th17; then A11: LSeg ((f /. i),(f /. (i + 1))) c= L~ (f | (i + 1)) by Th19; i <= len f by A1, FINSEQ_3:25; then Seg i c= Seg (len f) by FINSEQ_1:5; then Seg i c= dom f by FINSEQ_1:def_3; then (dom f) /\ (Seg i) = Seg i by XBOOLE_1:28; then A12: ( f | i = f | (Seg i) & dom (f | (Seg i)) = Seg i ) by FINSEQ_1:def_15, RELAT_1:61; then A13: i = len (f | i) by FINSEQ_1:def_3; A14: Seg (len (f | (i + 1))) = dom (f | (i + 1)) by FINSEQ_1:def_3; thus L~ (f | (i + 1)) c= (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1)))) :: according to XBOOLE_0:def_10 ::_thesis: (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1)))) c= L~ (f | (i + 1)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in L~ (f | (i + 1)) or x in (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1)))) ) assume x in L~ (f | (i + 1)) ; ::_thesis: x in (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1)))) then consider X being set such that A15: x in X and A16: X in { (LSeg ((f | (i + 1)),k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len (f | (i + 1)) ) } by TARSKI:def_4; consider m being Element of NAT such that A17: X = LSeg ((f | (i + 1)),m) and A18: 1 <= m and A19: m + 1 <= len (f | (i + 1)) by A16; A20: m <= i by A5, A19, XREAL_1:6; percases ( m = i or m < i ) by A20, XXREAL_0:1; suppose m = i ; ::_thesis: x in (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1)))) then X c= (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1)))) by A10, A17, XBOOLE_1:7; hence x in (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1)))) by A15; ::_thesis: verum end; supposeA21: m < i ; ::_thesis: x in (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1)))) then m <= i + 1 by NAT_1:13; then A22: m in dom (f | (i + 1)) by A4, A18, FINSEQ_1:1; A23: m in dom (f | i) by A12, A18, A21, FINSEQ_1:1; A24: 1 <= m + 1 by A18, NAT_1:13; A25: m + 1 <= i by A21, NAT_1:13; then A26: m + 1 in dom (f | i) by A12, A24, FINSEQ_1:1; m + 1 in dom (f | (i + 1)) by A14, A19, A24, FINSEQ_1:1; then X = LSeg (f,m) by A17, A22, Th17 .= LSeg ((f | i),m) by A23, A26, Th17 ; then X in { (LSeg ((f | i),n)) where n is Element of NAT : ( 1 <= n & n + 1 <= len (f | i) ) } by A13, A18, A25; then x in union { (LSeg ((f | i),n)) where n is Element of NAT : ( 1 <= n & n + 1 <= len (f | i) ) } by A15, TARSKI:def_4; hence x in (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1)))) by XBOOLE_0:def_3; ::_thesis: verum end; end; end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1)))) or x in L~ (f | (i + 1)) ) assume A27: x in (L~ (f | i)) \/ (LSeg ((f /. i),(f /. (i + 1)))) ; ::_thesis: x in L~ (f | (i + 1)) percases ( x in L~ (f | i) or x in LSeg ((f /. i),(f /. (i + 1))) ) by A27, XBOOLE_0:def_3; suppose x in L~ (f | i) ; ::_thesis: x in L~ (f | (i + 1)) then consider X being set such that A28: x in X and A29: X in { (LSeg ((f | i),n)) where n is Element of NAT : ( 1 <= n & n + 1 <= len (f | i) ) } by TARSKI:def_4; consider m being Element of NAT such that A30: X = LSeg ((f | i),m) and A31: 1 <= m and A32: m + 1 <= len (f | i) by A29; A33: 1 <= m + 1 by NAT_1:11; then A34: m + 1 in dom (f | i) by A32, FINSEQ_3:25; m <= m + 1 by NAT_1:11; then A35: m <= len (f | i) by A32, XXREAL_0:2; then m <= len (f | (i + 1)) by A5, A13, A9, XXREAL_0:2; then A36: m in dom (f | (i + 1)) by A31, FINSEQ_3:25; A37: m + 1 <= len (f | (i + 1)) by A5, A13, A9, A32, XXREAL_0:2; then A38: m + 1 in dom (f | (i + 1)) by A33, FINSEQ_3:25; m in dom (f | i) by A31, A35, FINSEQ_3:25; then X = LSeg (f,m) by A30, A34, Th17 .= LSeg ((f | (i + 1)),m) by A36, A38, Th17 ; then X in { (LSeg ((f | (i + 1)),k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len (f | (i + 1)) ) } by A31, A37; hence x in L~ (f | (i + 1)) by A28, TARSKI:def_4; ::_thesis: verum end; suppose x in LSeg ((f /. i),(f /. (i + 1))) ; ::_thesis: x in L~ (f | (i + 1)) hence x in L~ (f | (i + 1)) by A11; ::_thesis: verum end; end; end; theorem :: TOPREAL3:39 for p being Point of (TOP-REAL 2) for f being FinSequence of (TOP-REAL 2) st len f >= 2 & not p in L~ f holds for n being Element of NAT st 1 <= n & n <= len f holds f /. n <> p proof let p be Point of (TOP-REAL 2); ::_thesis: for f being FinSequence of (TOP-REAL 2) st len f >= 2 & not p in L~ f holds for n being Element of NAT st 1 <= n & n <= len f holds f /. n <> p let f be FinSequence of (TOP-REAL 2); ::_thesis: ( len f >= 2 & not p in L~ f implies for n being Element of NAT st 1 <= n & n <= len f holds f /. n <> p ) assume that A1: len f >= 2 and A2: not p in L~ f ; ::_thesis: for n being Element of NAT st 1 <= n & n <= len f holds f /. n <> p set Mf = { (LSeg (f,k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len f ) } ; given n being Element of NAT such that A3: 1 <= n and A4: n <= len f and A5: f /. n = p ; ::_thesis: contradiction percases ( n = len f or n < len f ) by A4, XXREAL_0:1; supposeA6: n = len f ; ::_thesis: contradiction reconsider j = (len f) - 1 as Element of NAT by A1, INT_1:5, XXREAL_0:2; 1 + 1 <= len f by A1; then A7: 1 <= j by XREAL_1:19; then A8: f /. (j + 1) in LSeg (f,j) by TOPREAL1:21; j + 1 <= len f ; then LSeg (f,j) in { (LSeg (f,k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len f ) } by A7; hence contradiction by A2, A5, A6, A8, TARSKI:def_4; ::_thesis: verum end; supposeA9: n < len f ; ::_thesis: contradiction then n + 1 <= len f by NAT_1:13; then A10: f /. n in LSeg (f,n) by A3, TOPREAL1:21; n + 1 <= len f by A9, NAT_1:13; then LSeg (f,n) in { (LSeg (f,k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len f ) } by A3; hence contradiction by A2, A5, A10, TARSKI:def_4; ::_thesis: verum end; end; end; theorem :: TOPREAL3:40 for q, p being Point of (TOP-REAL 2) for f being FinSequence of (TOP-REAL 2) st q <> p & (LSeg (q,p)) /\ (L~ f) = {q} holds not p in L~ f proof let q, p be Point of (TOP-REAL 2); ::_thesis: for f being FinSequence of (TOP-REAL 2) st q <> p & (LSeg (q,p)) /\ (L~ f) = {q} holds not p in L~ f let f be FinSequence of (TOP-REAL 2); ::_thesis: ( q <> p & (LSeg (q,p)) /\ (L~ f) = {q} implies not p in L~ f ) assume that A1: q <> p and A2: ( (LSeg (q,p)) /\ (L~ f) = {q} & p in L~ f ) ; ::_thesis: contradiction p in LSeg (q,p) by RLTOPSP1:68; then p in {q} by A2, XBOOLE_0:def_4; hence contradiction by A1, TARSKI:def_1; ::_thesis: verum end; theorem :: TOPREAL3:41 for f being FinSequence of (TOP-REAL 2) for m being Element of NAT st f is being_S-Seq & f /. (len f) in LSeg (f,m) & 1 <= m & m + 1 <= len f holds m + 1 = len f proof let f be FinSequence of (TOP-REAL 2); ::_thesis: for m being Element of NAT st f is being_S-Seq & f /. (len f) in LSeg (f,m) & 1 <= m & m + 1 <= len f holds m + 1 = len f let m be Element of NAT ; ::_thesis: ( f is being_S-Seq & f /. (len f) in LSeg (f,m) & 1 <= m & m + 1 <= len f implies m + 1 = len f ) assume that A1: f is being_S-Seq and A2: f /. (len f) in LSeg (f,m) and A3: 1 <= m and A4: m + 1 <= len f ; ::_thesis: m + 1 = len f A5: f is s.n.c. by A1, TOPREAL1:def_8; A6: f is one-to-one by A1, TOPREAL1:def_8; A7: f is unfolded by A1, TOPREAL1:def_8; set q = f /. (len f); A8: (m + 1) + 1 = m + (1 + 1) ; A9: len f >= 2 by A1, TOPREAL1:def_8; then reconsider k = (len f) - 1 as Element of NAT by INT_1:5, XXREAL_0:2; A10: k + 1 = len f ; assume m + 1 <> len f ; ::_thesis: contradiction then A11: m + 1 <= k by A4, A10, NAT_1:8; 1 <= len f by A9, XXREAL_0:2; then A12: len f in dom f by FINSEQ_3:25; percases ( m + 1 = k or m + 1 < k ) by A11, XXREAL_0:1; supposeA13: m + 1 = k ; ::_thesis: contradiction A14: 1 <= m + 1 by NAT_1:11; (m + 1) + 1 <= len f by A13; then A15: f /. (m + 2) in LSeg (f,(m + 1)) by A14, TOPREAL1:21; (LSeg (f,m)) /\ (LSeg (f,(m + 1))) = {(f /. (m + 1))} by A3, A7, A8, A13, TOPREAL1:def_6; then f /. (len f) in {(f /. (m + 1))} by A2, A13, A15, XBOOLE_0:def_4; then A16: f /. (len f) = f /. (m + 1) by TARSKI:def_1; m + 1 <= len f by A10, A13, NAT_1:11; then m + 1 in dom f by A14, FINSEQ_3:25; then len f = (len f) - 1 by A6, A12, A13, A16, PARTFUN2:10; hence contradiction ; ::_thesis: verum end; supposeA17: m + 1 < k ; ::_thesis: contradiction (1 + 1) - 1 = 1 ; then ( k + 1 = len f & 1 <= k ) by A9, XREAL_1:13; then A18: f /. (len f) in LSeg (f,k) by TOPREAL1:21; LSeg (f,m) misses LSeg (f,k) by A5, A17, TOPREAL1:def_7; then (LSeg (f,m)) /\ (LSeg (f,k)) = {} by XBOOLE_0:def_7; hence contradiction by A2, A18, XBOOLE_0:def_4; ::_thesis: verum end; end; end; theorem :: TOPREAL3:42 for p1, q, p being Point of (TOP-REAL 2) for r being real number for u being Point of (Euclid 2) st not p1 in Ball (u,r) & q in Ball (u,r) & p in Ball (u,r) & not p in LSeg (p1,q) & ( ( q `1 = p `1 & q `2 <> p `2 ) or ( q `1 <> p `1 & q `2 = p `2 ) ) & ( p1 `1 = q `1 or p1 `2 = q `2 ) holds (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} proof let p1, q, p be Point of (TOP-REAL 2); ::_thesis: for r being real number for u being Point of (Euclid 2) st not p1 in Ball (u,r) & q in Ball (u,r) & p in Ball (u,r) & not p in LSeg (p1,q) & ( ( q `1 = p `1 & q `2 <> p `2 ) or ( q `1 <> p `1 & q `2 = p `2 ) ) & ( p1 `1 = q `1 or p1 `2 = q `2 ) holds (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} let r be real number ; ::_thesis: for u being Point of (Euclid 2) st not p1 in Ball (u,r) & q in Ball (u,r) & p in Ball (u,r) & not p in LSeg (p1,q) & ( ( q `1 = p `1 & q `2 <> p `2 ) or ( q `1 <> p `1 & q `2 = p `2 ) ) & ( p1 `1 = q `1 or p1 `2 = q `2 ) holds (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} let u be Point of (Euclid 2); ::_thesis: ( not p1 in Ball (u,r) & q in Ball (u,r) & p in Ball (u,r) & not p in LSeg (p1,q) & ( ( q `1 = p `1 & q `2 <> p `2 ) or ( q `1 <> p `1 & q `2 = p `2 ) ) & ( p1 `1 = q `1 or p1 `2 = q `2 ) implies (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} ) assume that A1: not p1 in Ball (u,r) and A2: q in Ball (u,r) and A3: p in Ball (u,r) and A4: not p in LSeg (p1,q) ; ::_thesis: ( ( not ( q `1 = p `1 & q `2 <> p `2 ) & not ( q `1 <> p `1 & q `2 = p `2 ) ) or ( not p1 `1 = q `1 & not p1 `2 = q `2 ) or (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} ) assume A5: ( ( q `1 = p `1 & q `2 <> p `2 ) or ( q `1 <> p `1 & q `2 = p `2 ) ) ; ::_thesis: ( ( not p1 `1 = q `1 & not p1 `2 = q `2 ) or (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} ) assume A6: ( p1 `1 = q `1 or p1 `2 = q `2 ) ; ::_thesis: (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} A7: now__::_thesis:_(_(_p1_`1_=_q_`1_&_p1_`2_<>_q_`2_)_or_(_p1_`1_<>_q_`1_&_p1_`2_=_q_`2_)_) percases ( p1 `1 = q `1 or p1 `2 = q `2 ) by A6; suppose p1 `1 = q `1 ; ::_thesis: ( ( p1 `1 = q `1 & p1 `2 <> q `2 ) or ( p1 `1 <> q `1 & p1 `2 = q `2 ) ) hence ( ( p1 `1 = q `1 & p1 `2 <> q `2 ) or ( p1 `1 <> q `1 & p1 `2 = q `2 ) ) by A1, A2, Th6; ::_thesis: verum end; suppose p1 `2 = q `2 ; ::_thesis: ( ( p1 `1 = q `1 & p1 `2 <> q `2 ) or ( p1 `1 <> q `1 & p1 `2 = q `2 ) ) hence ( ( p1 `1 = q `1 & p1 `2 <> q `2 ) or ( p1 `1 <> q `1 & p1 `2 = q `2 ) ) by A1, A2, Th6; ::_thesis: verum end; end; end; A8: p = |[(p `1),(p `2)]| by EUCLID:53; A9: p1 = |[(p1 `1),(p1 `2)]| by EUCLID:53; A10: q = |[(q `1),(q `2)]| by EUCLID:53; A11: LSeg (p,q) c= Ball (u,r) by A2, A3, Th21; now__::_thesis:_(LSeg_(p1,q))_/\_(LSeg_(q,p))_=_{q} percases ( ( q `1 = p `1 & q `2 <> p `2 ) or ( q `1 <> p `1 & q `2 = p `2 ) ) by A5; supposeA12: ( q `1 = p `1 & q `2 <> p `2 ) ; ::_thesis: (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} set r = p `1 ; set pq = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = p `1 & p `2 <= p2 `2 & p2 `2 <= q `2 ) } ; set qp = { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `1 = p `1 & q `2 <= p3 `2 & p3 `2 <= p `2 ) } ; set pp1 = { p11 where p11 is Point of (TOP-REAL 2) : ( p11 `1 = p `1 & p `2 <= p11 `2 & p11 `2 <= p1 `2 ) } ; set p1p = { p22 where p22 is Point of (TOP-REAL 2) : ( p22 `1 = p `1 & p1 `2 <= p22 `2 & p22 `2 <= p `2 ) } ; set qp1 = { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 = p `1 & q `2 <= q1 `2 & q1 `2 <= p1 `2 ) } ; set p1q = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = p `1 & p1 `2 <= q2 `2 & q2 `2 <= q `2 ) } ; now__::_thesis:_(LSeg_(p1,q))_/\_(LSeg_(q,p))_=_{q} percases ( q `2 > p `2 or q `2 < p `2 ) by A12, XXREAL_0:1; supposeA13: q `2 > p `2 ; ::_thesis: (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} now__::_thesis:_(LSeg_(p1,q))_/\_(LSeg_(q,p))_=_{q} percases ( ( p1 `1 = q `1 & p1 `2 <> q `2 ) or ( p1 `1 <> q `1 & p1 `2 = q `2 ) ) by A7; supposeA14: ( p1 `1 = q `1 & p1 `2 <> q `2 ) ; ::_thesis: (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} now__::_thesis:_(_(_p1_`2_>_q_`2_&_(LSeg_(p1,q))_/\_(LSeg_(q,p))_=_{q}_)_or_(_p1_`2_<_q_`2_&_contradiction_)_) percases ( p1 `2 > q `2 or p1 `2 < q `2 ) by A14, XXREAL_0:1; caseA15: p1 `2 > q `2 ; ::_thesis: (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} then q in { p11 where p11 is Point of (TOP-REAL 2) : ( p11 `1 = p `1 & p `2 <= p11 `2 & p11 `2 <= p1 `2 ) } by A12, A13; then q in LSeg (p,p1) by A8, A9, A12, A13, A14, A15, Th9, XXREAL_0:2; hence (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} by TOPREAL1:8; ::_thesis: verum end; caseA16: p1 `2 < q `2 ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( p1 `2 > p `2 or p1 `2 = p `2 or p1 `2 < p `2 ) by XXREAL_0:1; supposeA17: p1 `2 > p `2 ; ::_thesis: contradiction then p1 in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = p `1 & p `2 <= p2 `2 & p2 `2 <= q `2 ) } by A12, A14, A16; then p1 in LSeg (p,q) by A8, A10, A12, A16, A17, Th9, XXREAL_0:2; hence contradiction by A1, A11; ::_thesis: verum end; suppose p1 `2 = p `2 ; ::_thesis: contradiction hence contradiction by A1, A3, A12, A14, Th6; ::_thesis: verum end; suppose p1 `2 < p `2 ; ::_thesis: contradiction then p in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = p `1 & p1 `2 <= q2 `2 & q2 `2 <= q `2 ) } by A13; hence contradiction by A4, A9, A10, A12, A14, A16, Th9; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; end; end; hence (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} ; ::_thesis: verum end; suppose ( p1 `1 <> q `1 & p1 `2 = q `2 ) ; ::_thesis: (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} hence (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} by A10, A12, Th30; ::_thesis: verum end; end; end; hence (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} ; ::_thesis: verum end; supposeA18: q `2 < p `2 ; ::_thesis: (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} now__::_thesis:_(LSeg_(p1,q))_/\_(LSeg_(q,p))_=_{q} percases ( ( p1 `1 = q `1 & p1 `2 <> q `2 ) or ( p1 `1 <> q `1 & p1 `2 = q `2 ) ) by A7; supposeA19: ( p1 `1 = q `1 & p1 `2 <> q `2 ) ; ::_thesis: (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} now__::_thesis:_(_(_p1_`2_>_q_`2_&_contradiction_)_or_(_p1_`2_<_q_`2_&_(LSeg_(p1,q))_/\_(LSeg_(q,p))_=_{q}_)_) percases ( p1 `2 > q `2 or p1 `2 < q `2 ) by A19, XXREAL_0:1; caseA20: p1 `2 > q `2 ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( p1 `2 > p `2 or p1 `2 = p `2 or p1 `2 < p `2 ) by XXREAL_0:1; suppose p1 `2 > p `2 ; ::_thesis: contradiction then p in { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 = p `1 & q `2 <= q1 `2 & q1 `2 <= p1 `2 ) } by A18; hence contradiction by A4, A9, A10, A12, A19, A20, Th9; ::_thesis: verum end; suppose p1 `2 = p `2 ; ::_thesis: contradiction hence contradiction by A1, A3, A12, A19, Th6; ::_thesis: verum end; suppose p1 `2 < p `2 ; ::_thesis: contradiction then p1 in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `1 = p `1 & q `2 <= p3 `2 & p3 `2 <= p `2 ) } by A12, A19, A20; then p1 in LSeg (p,q) by A8, A10, A12, A18, Th9; hence contradiction by A1, A11; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; caseA21: p1 `2 < q `2 ; ::_thesis: (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} then q in { p22 where p22 is Point of (TOP-REAL 2) : ( p22 `1 = p `1 & p1 `2 <= p22 `2 & p22 `2 <= p `2 ) } by A12, A18; then q in LSeg (p1,p) by A8, A9, A12, A18, A19, A21, Th9, XXREAL_0:2; hence (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} by TOPREAL1:8; ::_thesis: verum end; end; end; hence (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} ; ::_thesis: verum end; suppose ( p1 `1 <> q `1 & p1 `2 = q `2 ) ; ::_thesis: (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} hence (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} by A10, A12, Th30; ::_thesis: verum end; end; end; hence (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} ; ::_thesis: verum end; end; end; hence (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} ; ::_thesis: verum end; supposeA22: ( q `1 <> p `1 & q `2 = p `2 ) ; ::_thesis: (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} set r = p `2 ; set pq = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = p `2 & p `1 <= p2 `1 & p2 `1 <= q `1 ) } ; set qp = { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `2 = p `2 & q `1 <= p3 `1 & p3 `1 <= p `1 ) } ; set pp1 = { p11 where p11 is Point of (TOP-REAL 2) : ( p11 `2 = p `2 & p `1 <= p11 `1 & p11 `1 <= p1 `1 ) } ; set p1p = { p22 where p22 is Point of (TOP-REAL 2) : ( p22 `2 = p `2 & p1 `1 <= p22 `1 & p22 `1 <= p `1 ) } ; set qp1 = { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `2 = p `2 & q `1 <= q1 `1 & q1 `1 <= p1 `1 ) } ; set p1q = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `2 = p `2 & p1 `1 <= q2 `1 & q2 `1 <= q `1 ) } ; now__::_thesis:_(LSeg_(p1,q))_/\_(LSeg_(q,p))_=_{q} percases ( q `1 > p `1 or q `1 < p `1 ) by A22, XXREAL_0:1; supposeA23: q `1 > p `1 ; ::_thesis: (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} now__::_thesis:_(LSeg_(p1,q))_/\_(LSeg_(q,p))_=_{q} percases ( ( p1 `1 = q `1 & p1 `2 <> q `2 ) or ( p1 `1 <> q `1 & p1 `2 = q `2 ) ) by A7; suppose ( p1 `1 = q `1 & p1 `2 <> q `2 ) ; ::_thesis: (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} hence (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} by A10, A22, Th29; ::_thesis: verum end; supposeA24: ( p1 `1 <> q `1 & p1 `2 = q `2 ) ; ::_thesis: (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} now__::_thesis:_(_(_p1_`1_>_q_`1_&_(LSeg_(p1,q))_/\_(LSeg_(q,p))_=_{q}_)_or_(_p1_`1_<_q_`1_&_contradiction_)_) percases ( p1 `1 > q `1 or p1 `1 < q `1 ) by A24, XXREAL_0:1; caseA25: p1 `1 > q `1 ; ::_thesis: (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} then q in { p11 where p11 is Point of (TOP-REAL 2) : ( p11 `2 = p `2 & p `1 <= p11 `1 & p11 `1 <= p1 `1 ) } by A22, A23; then q in LSeg (p,p1) by A8, A9, A22, A23, A24, A25, Th10, XXREAL_0:2; hence (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} by TOPREAL1:8; ::_thesis: verum end; caseA26: p1 `1 < q `1 ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( p1 `1 > p `1 or p1 `1 = p `1 or p1 `1 < p `1 ) by XXREAL_0:1; supposeA27: p1 `1 > p `1 ; ::_thesis: contradiction then p1 in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = p `2 & p `1 <= p2 `1 & p2 `1 <= q `1 ) } by A22, A24, A26; then p1 in LSeg (p,q) by A8, A10, A22, A26, A27, Th10, XXREAL_0:2; hence contradiction by A1, A11; ::_thesis: verum end; suppose p1 `1 = p `1 ; ::_thesis: contradiction hence contradiction by A1, A3, A22, A24, Th6; ::_thesis: verum end; suppose p1 `1 < p `1 ; ::_thesis: contradiction then p in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `2 = p `2 & p1 `1 <= q2 `1 & q2 `1 <= q `1 ) } by A23; hence contradiction by A4, A9, A10, A22, A24, A26, Th10; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; end; end; hence (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} ; ::_thesis: verum end; end; end; hence (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} ; ::_thesis: verum end; supposeA28: q `1 < p `1 ; ::_thesis: (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} now__::_thesis:_(LSeg_(p1,q))_/\_(LSeg_(q,p))_=_{q} percases ( ( p1 `1 = q `1 & p1 `2 <> q `2 ) or ( p1 `1 <> q `1 & p1 `2 = q `2 ) ) by A7; suppose ( p1 `1 = q `1 & p1 `2 <> q `2 ) ; ::_thesis: (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} hence (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} by A10, A22, Th29; ::_thesis: verum end; supposeA29: ( p1 `1 <> q `1 & p1 `2 = q `2 ) ; ::_thesis: (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} now__::_thesis:_(_(_p1_`1_>_q_`1_&_contradiction_)_or_(_p1_`1_<_q_`1_&_(LSeg_(p1,q))_/\_(LSeg_(q,p))_=_{q}_)_) percases ( p1 `1 > q `1 or p1 `1 < q `1 ) by A29, XXREAL_0:1; caseA30: p1 `1 > q `1 ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( p1 `1 > p `1 or p1 `1 = p `1 or p1 `1 < p `1 ) by XXREAL_0:1; suppose p1 `1 > p `1 ; ::_thesis: contradiction then p in { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `2 = p `2 & q `1 <= q1 `1 & q1 `1 <= p1 `1 ) } by A28; hence contradiction by A4, A9, A10, A22, A29, A30, Th10; ::_thesis: verum end; suppose p1 `1 = p `1 ; ::_thesis: contradiction hence contradiction by A1, A3, A22, A29, Th6; ::_thesis: verum end; suppose p1 `1 < p `1 ; ::_thesis: contradiction then p1 in { p3 where p3 is Point of (TOP-REAL 2) : ( p3 `2 = p `2 & q `1 <= p3 `1 & p3 `1 <= p `1 ) } by A22, A29, A30; then p1 in LSeg (p,q) by A8, A10, A22, A28, Th10; hence contradiction by A1, A11; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; caseA31: p1 `1 < q `1 ; ::_thesis: (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} then q in { p22 where p22 is Point of (TOP-REAL 2) : ( p22 `2 = p `2 & p1 `1 <= p22 `1 & p22 `1 <= p `1 ) } by A22, A28; then q in LSeg (p1,p) by A8, A9, A22, A28, A29, A31, Th10, XXREAL_0:2; hence (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} by TOPREAL1:8; ::_thesis: verum end; end; end; hence (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} ; ::_thesis: verum end; end; end; hence (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} ; ::_thesis: verum end; end; end; hence (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} ; ::_thesis: verum end; end; end; hence (LSeg (p1,q)) /\ (LSeg (q,p)) = {q} ; ::_thesis: verum end; theorem :: TOPREAL3:43 for p1, p, q being Point of (TOP-REAL 2) for r being real number for u being Point of (Euclid 2) st not p1 in Ball (u,r) & p in Ball (u,r) & |[(p `1),(q `2)]| in Ball (u,r) & not |[(p `1),(q `2)]| in LSeg (p1,p) & p1 `1 = p `1 & p `1 <> q `1 & p `2 <> q `2 holds ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} proof let p1, p, q be Point of (TOP-REAL 2); ::_thesis: for r being real number for u being Point of (Euclid 2) st not p1 in Ball (u,r) & p in Ball (u,r) & |[(p `1),(q `2)]| in Ball (u,r) & not |[(p `1),(q `2)]| in LSeg (p1,p) & p1 `1 = p `1 & p `1 <> q `1 & p `2 <> q `2 holds ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} let r be real number ; ::_thesis: for u being Point of (Euclid 2) st not p1 in Ball (u,r) & p in Ball (u,r) & |[(p `1),(q `2)]| in Ball (u,r) & not |[(p `1),(q `2)]| in LSeg (p1,p) & p1 `1 = p `1 & p `1 <> q `1 & p `2 <> q `2 holds ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} let u be Point of (Euclid 2); ::_thesis: ( not p1 in Ball (u,r) & p in Ball (u,r) & |[(p `1),(q `2)]| in Ball (u,r) & not |[(p `1),(q `2)]| in LSeg (p1,p) & p1 `1 = p `1 & p `1 <> q `1 & p `2 <> q `2 implies ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} ) set v = |[(p `1),(q `2)]|; assume that A1: not p1 in Ball (u,r) and A2: p in Ball (u,r) and A3: |[(p `1),(q `2)]| in Ball (u,r) and A4: not |[(p `1),(q `2)]| in LSeg (p1,p) and A5: p1 `1 = p `1 and A6: p `1 <> q `1 and A7: p `2 <> q `2 ; ::_thesis: ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} A8: LSeg (p,|[(p `1),(q `2)]|) c= Ball (u,r) by A2, A3, Th21; p in LSeg (p,|[(p `1),(q `2)]|) by RLTOPSP1:68; then ( p in LSeg (p1,p) & p in (LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q)) ) by RLTOPSP1:68, XBOOLE_0:def_3; then p in ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) by XBOOLE_0:def_4; then A9: {p} c= ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) by ZFMISC_1:31; A10: ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = ((LSeg (p,|[(p `1),(q `2)]|)) /\ (LSeg (p1,p))) \/ ((LSeg (|[(p `1),(q `2)]|,q)) /\ (LSeg (p1,p))) by XBOOLE_1:23; A11: p1 = |[(p `1),(p1 `2)]| by A5, EUCLID:53; A12: q = |[(q `1),(q `2)]| by EUCLID:53; A13: p = |[(p `1),(p `2)]| by EUCLID:53; A14: |[(p `1),(q `2)]| `1 = p `1 by EUCLID:52; A15: |[(p `1),(q `2)]| `2 = q `2 by EUCLID:52; percases ( p1 `2 = p `2 or p1 `2 <> p `2 ) ; suppose p1 `2 = p `2 ; ::_thesis: ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} hence ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} by A1, A2, A5, Th6; ::_thesis: verum end; supposeA16: p1 `2 <> p `2 ; ::_thesis: ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} now__::_thesis:_((LSeg_(p,|[(p_`1),(q_`2)]|))_\/_(LSeg_(|[(p_`1),(q_`2)]|,q)))_/\_(LSeg_(p1,p))_=_{p} percases ( p1 `2 > p `2 or p1 `2 < p `2 ) by A16, XXREAL_0:1; supposeA17: p1 `2 > p `2 ; ::_thesis: ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} now__::_thesis:_((LSeg_(p,|[(p_`1),(q_`2)]|))_\/_(LSeg_(|[(p_`1),(q_`2)]|,q)))_/\_(LSeg_(p1,p))_=_{p} percases ( p `1 > q `1 or p `1 < q `1 ) by A6, XXREAL_0:1; supposeA18: p `1 > q `1 ; ::_thesis: ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} now__::_thesis:_(_(_p_`2_>_q_`2_&_((LSeg_(p,|[(p_`1),(q_`2)]|))_\/_(LSeg_(|[(p_`1),(q_`2)]|,q)))_/\_(LSeg_(p1,p))_=_{p}_)_or_(_p_`2_<_q_`2_&_contradiction_)_) percases ( p `2 > q `2 or p `2 < q `2 ) by A7, XXREAL_0:1; caseA19: p `2 > q `2 ; ::_thesis: ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} then A20: p `2 >= |[(p `1),(q `2)]| `2 by EUCLID:52; ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) c= {p} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) or x in {p} ) assume A21: x in ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) ; ::_thesis: x in {p} now__::_thesis:_(_(_x_in_(LSeg_(p,|[(p_`1),(q_`2)]|))_/\_(LSeg_(p1,p))_&_x_in_{p}_)_or_(_x_in_(LSeg_(|[(p_`1),(q_`2)]|,q))_/\_(LSeg_(p1,p))_&_contradiction_)_) percases ( x in (LSeg (p,|[(p `1),(q `2)]|)) /\ (LSeg (p1,p)) or x in (LSeg (|[(p `1),(q `2)]|,q)) /\ (LSeg (p1,p)) ) by A10, A21, XBOOLE_0:def_3; caseA22: x in (LSeg (p,|[(p `1),(q `2)]|)) /\ (LSeg (p1,p)) ; ::_thesis: x in {p} p in { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 = p `1 & |[(p `1),(q `2)]| `2 <= q1 `2 & q1 `2 <= p1 `2 ) } by A17, A20; then p in LSeg (p1,|[(p `1),(q `2)]|) by A11, A15, A17, A19, Th9, XXREAL_0:2; hence x in {p} by A22, TOPREAL1:8; ::_thesis: verum end; caseA23: x in (LSeg (|[(p `1),(q `2)]|,q)) /\ (LSeg (p1,p)) ; ::_thesis: contradiction then x in LSeg (|[(p `1),(q `2)]|,q) by XBOOLE_0:def_4; then x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = q `2 & q `1 <= p2 `1 & p2 `1 <= p `1 ) } by A12, A18, Th10; then A24: ex p2 being Point of (TOP-REAL 2) st ( p2 = x & p2 `2 = q `2 & q `1 <= p2 `1 & p2 `1 <= p `1 ) ; x in LSeg (p1,p) by A23, XBOOLE_0:def_4; then x in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = p `1 & p `2 <= q2 `2 & q2 `2 <= p1 `2 ) } by A11, A13, A17, Th9; then ex q2 being Point of (TOP-REAL 2) st ( q2 = x & q2 `1 = p `1 & p `2 <= q2 `2 & q2 `2 <= p1 `2 ) ; hence contradiction by A19, A24; ::_thesis: verum end; end; end; hence x in {p} ; ::_thesis: verum end; hence ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} by A9, XBOOLE_0:def_10; ::_thesis: verum end; caseA25: p `2 < q `2 ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( q `2 > p1 `2 or q `2 = p1 `2 or q `2 < p1 `2 ) by XXREAL_0:1; supposeA26: q `2 > p1 `2 ; ::_thesis: contradiction then p1 in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = p `1 & p `2 <= q2 `2 & q2 `2 <= |[(p `1),(q `2)]| `2 ) } by A5, A15, A17; then p1 in LSeg (p,|[(p `1),(q `2)]|) by A13, A15, A17, A26, Th9, XXREAL_0:2; hence contradiction by A1, A8; ::_thesis: verum end; suppose q `2 = p1 `2 ; ::_thesis: contradiction hence contradiction by A1, A3, A5, EUCLID:53; ::_thesis: verum end; supposeA27: q `2 < p1 `2 ; ::_thesis: contradiction then |[(p `1),(q `2)]| in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = p `1 & p `2 <= p2 `2 & p2 `2 <= p1 `2 ) } by A14, A15, A25; hence contradiction by A4, A11, A13, A25, A27, Th9, XXREAL_0:2; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; end; end; hence ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} ; ::_thesis: verum end; supposeA28: p `1 < q `1 ; ::_thesis: ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} now__::_thesis:_(_(_p_`2_>_q_`2_&_((LSeg_(p,|[(p_`1),(q_`2)]|))_\/_(LSeg_(|[(p_`1),(q_`2)]|,q)))_/\_(LSeg_(p1,p))_=_{p}_)_or_(_p_`2_<_q_`2_&_contradiction_)_) percases ( p `2 > q `2 or p `2 < q `2 ) by A7, XXREAL_0:1; caseA29: p `2 > q `2 ; ::_thesis: ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} then A30: p `2 >= |[(p `1),(q `2)]| `2 by EUCLID:52; ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) c= {p} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) or x in {p} ) assume A31: x in ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) ; ::_thesis: x in {p} now__::_thesis:_(_(_x_in_(LSeg_(p,|[(p_`1),(q_`2)]|))_/\_(LSeg_(p1,p))_&_x_in_{p}_)_or_(_x_in_(LSeg_(|[(p_`1),(q_`2)]|,q))_/\_(LSeg_(p1,p))_&_contradiction_)_) percases ( x in (LSeg (p,|[(p `1),(q `2)]|)) /\ (LSeg (p1,p)) or x in (LSeg (|[(p `1),(q `2)]|,q)) /\ (LSeg (p1,p)) ) by A10, A31, XBOOLE_0:def_3; caseA32: x in (LSeg (p,|[(p `1),(q `2)]|)) /\ (LSeg (p1,p)) ; ::_thesis: x in {p} p in { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 = p `1 & |[(p `1),(q `2)]| `2 <= q1 `2 & q1 `2 <= p1 `2 ) } by A17, A30; then p in LSeg (p1,|[(p `1),(q `2)]|) by A11, A15, A17, A29, Th9, XXREAL_0:2; hence x in {p} by A32, TOPREAL1:8; ::_thesis: verum end; caseA33: x in (LSeg (|[(p `1),(q `2)]|,q)) /\ (LSeg (p1,p)) ; ::_thesis: contradiction then x in LSeg (|[(p `1),(q `2)]|,q) by XBOOLE_0:def_4; then x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = q `2 & p `1 <= p2 `1 & p2 `1 <= q `1 ) } by A12, A28, Th10; then A34: ex p2 being Point of (TOP-REAL 2) st ( p2 = x & p2 `2 = q `2 & p `1 <= p2 `1 & p2 `1 <= q `1 ) ; x in LSeg (p1,p) by A33, XBOOLE_0:def_4; then x in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = p `1 & p `2 <= q2 `2 & q2 `2 <= p1 `2 ) } by A11, A13, A17, Th9; then ex q2 being Point of (TOP-REAL 2) st ( q2 = x & q2 `1 = p `1 & p `2 <= q2 `2 & q2 `2 <= p1 `2 ) ; hence contradiction by A29, A34; ::_thesis: verum end; end; end; hence x in {p} ; ::_thesis: verum end; hence ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} by A9, XBOOLE_0:def_10; ::_thesis: verum end; caseA35: p `2 < q `2 ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( q `2 > p1 `2 or q `2 = p1 `2 or q `2 < p1 `2 ) by XXREAL_0:1; supposeA36: q `2 > p1 `2 ; ::_thesis: contradiction then p1 in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = p `1 & p `2 <= q2 `2 & q2 `2 <= |[(p `1),(q `2)]| `2 ) } by A5, A15, A17; then p1 in LSeg (p,|[(p `1),(q `2)]|) by A13, A15, A17, A36, Th9, XXREAL_0:2; hence contradiction by A1, A8; ::_thesis: verum end; suppose q `2 = p1 `2 ; ::_thesis: contradiction hence contradiction by A1, A3, A5, EUCLID:53; ::_thesis: verum end; supposeA37: q `2 < p1 `2 ; ::_thesis: contradiction then |[(p `1),(q `2)]| in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = p `1 & p `2 <= p2 `2 & p2 `2 <= p1 `2 ) } by A14, A15, A35; hence contradiction by A4, A11, A13, A35, A37, Th9, XXREAL_0:2; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; end; end; hence ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} ; ::_thesis: verum end; end; end; hence ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} ; ::_thesis: verum end; supposeA38: p1 `2 < p `2 ; ::_thesis: ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} now__::_thesis:_((LSeg_(p,|[(p_`1),(q_`2)]|))_\/_(LSeg_(|[(p_`1),(q_`2)]|,q)))_/\_(LSeg_(p1,p))_=_{p} percases ( p `1 > q `1 or p `1 < q `1 ) by A6, XXREAL_0:1; supposeA39: p `1 > q `1 ; ::_thesis: ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} now__::_thesis:_(_(_p_`2_>_q_`2_&_contradiction_)_or_(_p_`2_<_q_`2_&_((LSeg_(p,|[(p_`1),(q_`2)]|))_\/_(LSeg_(|[(p_`1),(q_`2)]|,q)))_/\_(LSeg_(p1,p))_=_{p}_)_) percases ( p `2 > q `2 or p `2 < q `2 ) by A7, XXREAL_0:1; caseA40: p `2 > q `2 ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( q `2 > p1 `2 or q `2 = p1 `2 or q `2 < p1 `2 ) by XXREAL_0:1; supposeA41: q `2 > p1 `2 ; ::_thesis: contradiction then |[(p `1),(q `2)]| in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = p `1 & p1 `2 <= p2 `2 & p2 `2 <= p `2 ) } by A14, A15, A40; hence contradiction by A4, A11, A13, A40, A41, Th9, XXREAL_0:2; ::_thesis: verum end; suppose q `2 = p1 `2 ; ::_thesis: contradiction hence contradiction by A1, A3, A5, EUCLID:53; ::_thesis: verum end; supposeA42: q `2 < p1 `2 ; ::_thesis: contradiction then p1 in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = p `1 & |[(p `1),(q `2)]| `2 <= q2 `2 & q2 `2 <= p `2 ) } by A5, A15, A38; then p1 in LSeg (p,|[(p `1),(q `2)]|) by A13, A15, A38, A42, Th9, XXREAL_0:2; hence contradiction by A1, A8; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; caseA43: p `2 < q `2 ; ::_thesis: ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) c= {p} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) or x in {p} ) assume A44: x in ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) ; ::_thesis: x in {p} now__::_thesis:_(_(_x_in_(LSeg_(p,|[(p_`1),(q_`2)]|))_/\_(LSeg_(p1,p))_&_x_in_{p}_)_or_(_x_in_(LSeg_(|[(p_`1),(q_`2)]|,q))_/\_(LSeg_(p1,p))_&_contradiction_)_) percases ( x in (LSeg (p,|[(p `1),(q `2)]|)) /\ (LSeg (p1,p)) or x in (LSeg (|[(p `1),(q `2)]|,q)) /\ (LSeg (p1,p)) ) by A10, A44, XBOOLE_0:def_3; caseA45: x in (LSeg (p,|[(p `1),(q `2)]|)) /\ (LSeg (p1,p)) ; ::_thesis: x in {p} p in { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 = p `1 & p1 `2 <= q1 `2 & q1 `2 <= |[(p `1),(q `2)]| `2 ) } by A15, A38, A43; then p in LSeg (p1,|[(p `1),(q `2)]|) by A11, A15, A38, A43, Th9, XXREAL_0:2; hence x in {p} by A45, TOPREAL1:8; ::_thesis: verum end; caseA46: x in (LSeg (|[(p `1),(q `2)]|,q)) /\ (LSeg (p1,p)) ; ::_thesis: contradiction then x in LSeg (|[(p `1),(q `2)]|,q) by XBOOLE_0:def_4; then x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = q `2 & q `1 <= p2 `1 & p2 `1 <= p `1 ) } by A12, A39, Th10; then A47: ex p2 being Point of (TOP-REAL 2) st ( p2 = x & p2 `2 = q `2 & q `1 <= p2 `1 & p2 `1 <= p `1 ) ; x in LSeg (p1,p) by A46, XBOOLE_0:def_4; then x in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = p `1 & p1 `2 <= q2 `2 & q2 `2 <= p `2 ) } by A11, A13, A38, Th9; then ex q2 being Point of (TOP-REAL 2) st ( q2 = x & q2 `1 = p `1 & p1 `2 <= q2 `2 & q2 `2 <= p `2 ) ; hence contradiction by A43, A47; ::_thesis: verum end; end; end; hence x in {p} ; ::_thesis: verum end; hence ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} by A9, XBOOLE_0:def_10; ::_thesis: verum end; end; end; hence ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} ; ::_thesis: verum end; supposeA48: p `1 < q `1 ; ::_thesis: ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} now__::_thesis:_(_(_p_`2_>_q_`2_&_contradiction_)_or_(_p_`2_<_q_`2_&_((LSeg_(p,|[(p_`1),(q_`2)]|))_\/_(LSeg_(|[(p_`1),(q_`2)]|,q)))_/\_(LSeg_(p1,p))_=_{p}_)_) percases ( p `2 > q `2 or p `2 < q `2 ) by A7, XXREAL_0:1; caseA49: p `2 > q `2 ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( q `2 > p1 `2 or q `2 = p1 `2 or q `2 < p1 `2 ) by XXREAL_0:1; supposeA50: q `2 > p1 `2 ; ::_thesis: contradiction then |[(p `1),(q `2)]| in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = p `1 & p1 `2 <= p2 `2 & p2 `2 <= p `2 ) } by A14, A15, A49; hence contradiction by A4, A11, A13, A49, A50, Th9, XXREAL_0:2; ::_thesis: verum end; suppose q `2 = p1 `2 ; ::_thesis: contradiction hence contradiction by A1, A3, A5, EUCLID:53; ::_thesis: verum end; supposeA51: q `2 < p1 `2 ; ::_thesis: contradiction then p1 in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = p `1 & |[(p `1),(q `2)]| `2 <= q2 `2 & q2 `2 <= p `2 ) } by A5, A15, A38; then p1 in LSeg (p,|[(p `1),(q `2)]|) by A13, A15, A38, A51, Th9, XXREAL_0:2; hence contradiction by A1, A8; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; caseA52: p `2 < q `2 ; ::_thesis: ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) c= {p} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) or x in {p} ) assume A53: x in ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) ; ::_thesis: x in {p} now__::_thesis:_(_(_x_in_(LSeg_(p,|[(p_`1),(q_`2)]|))_/\_(LSeg_(p1,p))_&_x_in_{p}_)_or_(_x_in_(LSeg_(|[(p_`1),(q_`2)]|,q))_/\_(LSeg_(p1,p))_&_contradiction_)_) percases ( x in (LSeg (p,|[(p `1),(q `2)]|)) /\ (LSeg (p1,p)) or x in (LSeg (|[(p `1),(q `2)]|,q)) /\ (LSeg (p1,p)) ) by A10, A53, XBOOLE_0:def_3; caseA54: x in (LSeg (p,|[(p `1),(q `2)]|)) /\ (LSeg (p1,p)) ; ::_thesis: x in {p} p in { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 = p `1 & p1 `2 <= q1 `2 & q1 `2 <= |[(p `1),(q `2)]| `2 ) } by A15, A38, A52; then p in LSeg (p1,|[(p `1),(q `2)]|) by A11, A15, A38, A52, Th9, XXREAL_0:2; hence x in {p} by A54, TOPREAL1:8; ::_thesis: verum end; caseA55: x in (LSeg (|[(p `1),(q `2)]|,q)) /\ (LSeg (p1,p)) ; ::_thesis: contradiction then x in LSeg (|[(p `1),(q `2)]|,q) by XBOOLE_0:def_4; then x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = q `2 & p `1 <= p2 `1 & p2 `1 <= q `1 ) } by A12, A48, Th10; then A56: ex p2 being Point of (TOP-REAL 2) st ( p2 = x & p2 `2 = q `2 & p `1 <= p2 `1 & p2 `1 <= q `1 ) ; x in LSeg (p1,p) by A55, XBOOLE_0:def_4; then x in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = p `1 & p1 `2 <= q2 `2 & q2 `2 <= p `2 ) } by A11, A13, A38, Th9; then ex q2 being Point of (TOP-REAL 2) st ( q2 = x & q2 `1 = p `1 & p1 `2 <= q2 `2 & q2 `2 <= p `2 ) ; hence contradiction by A52, A56; ::_thesis: verum end; end; end; hence x in {p} ; ::_thesis: verum end; hence ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} by A9, XBOOLE_0:def_10; ::_thesis: verum end; end; end; hence ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} ; ::_thesis: verum end; end; end; hence ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} ; ::_thesis: verum end; end; end; hence ((LSeg (p,|[(p `1),(q `2)]|)) \/ (LSeg (|[(p `1),(q `2)]|,q))) /\ (LSeg (p1,p)) = {p} ; ::_thesis: verum end; end; end; theorem :: TOPREAL3:44 for p1, p, q being Point of (TOP-REAL 2) for r being real number for u being Point of (Euclid 2) st not p1 in Ball (u,r) & p in Ball (u,r) & |[(q `1),(p `2)]| in Ball (u,r) & not |[(q `1),(p `2)]| in LSeg (p1,p) & p1 `2 = p `2 & p `1 <> q `1 & p `2 <> q `2 holds ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p} proof let p1, p, q be Point of (TOP-REAL 2); ::_thesis: for r being real number for u being Point of (Euclid 2) st not p1 in Ball (u,r) & p in Ball (u,r) & |[(q `1),(p `2)]| in Ball (u,r) & not |[(q `1),(p `2)]| in LSeg (p1,p) & p1 `2 = p `2 & p `1 <> q `1 & p `2 <> q `2 holds ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p} let r be real number ; ::_thesis: for u being Point of (Euclid 2) st not p1 in Ball (u,r) & p in Ball (u,r) & |[(q `1),(p `2)]| in Ball (u,r) & not |[(q `1),(p `2)]| in LSeg (p1,p) & p1 `2 = p `2 & p `1 <> q `1 & p `2 <> q `2 holds ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p} let u be Point of (Euclid 2); ::_thesis: ( not p1 in Ball (u,r) & p in Ball (u,r) & |[(q `1),(p `2)]| in Ball (u,r) & not |[(q `1),(p `2)]| in LSeg (p1,p) & p1 `2 = p `2 & p `1 <> q `1 & p `2 <> q `2 implies ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p} ) set v = |[(q `1),(p `2)]|; assume that A1: not p1 in Ball (u,r) and A2: p in Ball (u,r) and A3: |[(q `1),(p `2)]| in Ball (u,r) and A4: not |[(q `1),(p `2)]| in LSeg (p1,p) and A5: p1 `2 = p `2 and A6: p `1 <> q `1 and A7: p `2 <> q `2 ; ::_thesis: ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p} A8: LSeg (p,|[(q `1),(p `2)]|) c= Ball (u,r) by A2, A3, Th21; A9: p1 = |[(p1 `1),(p `2)]| by A5, EUCLID:53; p in LSeg (p,|[(q `1),(p `2)]|) by RLTOPSP1:68; then ( p in LSeg (p1,p) & p in (LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q)) ) by RLTOPSP1:68, XBOOLE_0:def_3; then p in ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) by XBOOLE_0:def_4; then A10: {p} c= ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) by ZFMISC_1:31; A11: ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = ((LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (p1,p))) \/ ((LSeg (|[(q `1),(p `2)]|,q)) /\ (LSeg (p1,p))) by XBOOLE_1:23; A12: q = |[(q `1),(q `2)]| by EUCLID:53; A13: p = |[(p `1),(p `2)]| by EUCLID:53; A14: |[(q `1),(p `2)]| `2 = p `2 by EUCLID:52; A15: |[(q `1),(p `2)]| `1 = q `1 by EUCLID:52; percases ( p1 `1 = p `1 or p1 `1 <> p `1 ) ; suppose p1 `1 = p `1 ; ::_thesis: ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p} hence ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p} by A1, A2, A5, Th6; ::_thesis: verum end; supposeA16: p1 `1 <> p `1 ; ::_thesis: ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p} now__::_thesis:_((LSeg_(p,|[(q_`1),(p_`2)]|))_\/_(LSeg_(|[(q_`1),(p_`2)]|,q)))_/\_(LSeg_(p1,p))_=_{p} percases ( p1 `1 > p `1 or p1 `1 < p `1 ) by A16, XXREAL_0:1; supposeA17: p1 `1 > p `1 ; ::_thesis: ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p} now__::_thesis:_(_(_p_`1_>_q_`1_&_((LSeg_(p,|[(q_`1),(p_`2)]|))_\/_(LSeg_(|[(q_`1),(p_`2)]|,q)))_/\_(LSeg_(p1,p))_=_{p}_)_or_(_p_`1_<_q_`1_&_contradiction_)_) percases ( p `1 > q `1 or p `1 < q `1 ) by A6, XXREAL_0:1; caseA18: p `1 > q `1 ; ::_thesis: ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p} then A19: p `1 >= |[(q `1),(p `2)]| `1 by EUCLID:52; now__::_thesis:_((LSeg_(p,|[(q_`1),(p_`2)]|))_\/_(LSeg_(|[(q_`1),(p_`2)]|,q)))_/\_(LSeg_(p1,p))_=_{p} percases ( p `2 > q `2 or p `2 < q `2 ) by A7, XXREAL_0:1; supposeA20: p `2 > q `2 ; ::_thesis: ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p} ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) c= {p} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) or x in {p} ) assume A21: x in ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) ; ::_thesis: x in {p} now__::_thesis:_(_(_x_in_(LSeg_(p,|[(q_`1),(p_`2)]|))_/\_(LSeg_(p1,p))_&_x_in_{p}_)_or_(_x_in_(LSeg_(|[(q_`1),(p_`2)]|,q))_/\_(LSeg_(p1,p))_&_contradiction_)_) percases ( x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (p1,p)) or x in (LSeg (|[(q `1),(p `2)]|,q)) /\ (LSeg (p1,p)) ) by A11, A21, XBOOLE_0:def_3; caseA22: x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (p1,p)) ; ::_thesis: x in {p} p in { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `2 = p `2 & |[(q `1),(p `2)]| `1 <= q1 `1 & q1 `1 <= p1 `1 ) } by A17, A19; then p in LSeg (p1,|[(q `1),(p `2)]|) by A9, A15, A17, A18, Th10, XXREAL_0:2; hence x in {p} by A22, TOPREAL1:8; ::_thesis: verum end; caseA23: x in (LSeg (|[(q `1),(p `2)]|,q)) /\ (LSeg (p1,p)) ; ::_thesis: contradiction then x in LSeg (q,|[(q `1),(p `2)]|) by XBOOLE_0:def_4; then x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = q `1 & q `2 <= p2 `2 & p2 `2 <= p `2 ) } by A12, A20, Th9; then A24: ex p2 being Point of (TOP-REAL 2) st ( p2 = x & p2 `1 = q `1 & q `2 <= p2 `2 & p2 `2 <= p `2 ) ; x in LSeg (p,p1) by A23, XBOOLE_0:def_4; then x in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `2 = p `2 & p `1 <= q2 `1 & q2 `1 <= p1 `1 ) } by A9, A13, A17, Th10; then ex q2 being Point of (TOP-REAL 2) st ( q2 = x & q2 `2 = p `2 & p `1 <= q2 `1 & q2 `1 <= p1 `1 ) ; hence contradiction by A18, A24; ::_thesis: verum end; end; end; hence x in {p} ; ::_thesis: verum end; hence ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p} by A10, XBOOLE_0:def_10; ::_thesis: verum end; supposeA25: p `2 < q `2 ; ::_thesis: ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p} ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) c= {p} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) or x in {p} ) assume A26: x in ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) ; ::_thesis: x in {p} now__::_thesis:_(_(_x_in_(LSeg_(p,|[(q_`1),(p_`2)]|))_/\_(LSeg_(p1,p))_&_x_in_{p}_)_or_(_x_in_(LSeg_(|[(q_`1),(p_`2)]|,q))_/\_(LSeg_(p1,p))_&_contradiction_)_) percases ( x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (p1,p)) or x in (LSeg (|[(q `1),(p `2)]|,q)) /\ (LSeg (p1,p)) ) by A11, A26, XBOOLE_0:def_3; caseA27: x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (p1,p)) ; ::_thesis: x in {p} p in { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `2 = p `2 & |[(q `1),(p `2)]| `1 <= q1 `1 & q1 `1 <= p1 `1 ) } by A17, A19; then p in LSeg (p1,|[(q `1),(p `2)]|) by A9, A15, A17, A18, Th10, XXREAL_0:2; hence x in {p} by A27, TOPREAL1:8; ::_thesis: verum end; caseA28: x in (LSeg (|[(q `1),(p `2)]|,q)) /\ (LSeg (p1,p)) ; ::_thesis: contradiction then x in LSeg (p1,p) by XBOOLE_0:def_4; then x in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `2 = p `2 & p `1 <= q2 `1 & q2 `1 <= p1 `1 ) } by A9, A13, A17, Th10; then A29: ex q2 being Point of (TOP-REAL 2) st ( q2 = x & q2 `2 = p `2 & p `1 <= q2 `1 & q2 `1 <= p1 `1 ) ; x in LSeg (|[(q `1),(p `2)]|,q) by A28, XBOOLE_0:def_4; then x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = q `1 & |[(q `1),(p `2)]| `2 <= p2 `2 & p2 `2 <= q `2 ) } by A12, A14, A25, Th9; then ex p2 being Point of (TOP-REAL 2) st ( p2 = x & p2 `1 = q `1 & |[(q `1),(p `2)]| `2 <= p2 `2 & p2 `2 <= q `2 ) ; hence contradiction by A18, A29; ::_thesis: verum end; end; end; hence x in {p} ; ::_thesis: verum end; hence ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p} by A10, XBOOLE_0:def_10; ::_thesis: verum end; end; end; hence ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p} ; ::_thesis: verum end; caseA30: p `1 < q `1 ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( q `1 > p1 `1 or q `1 = p1 `1 or q `1 < p1 `1 ) by XXREAL_0:1; supposeA31: q `1 > p1 `1 ; ::_thesis: contradiction then p1 in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `2 = p `2 & p `1 <= q2 `1 & q2 `1 <= |[(q `1),(p `2)]| `1 ) } by A5, A15, A17; then p1 in LSeg (p,|[(q `1),(p `2)]|) by A13, A15, A17, A31, Th10, XXREAL_0:2; hence contradiction by A1, A8; ::_thesis: verum end; suppose q `1 = p1 `1 ; ::_thesis: contradiction hence contradiction by A1, A3, A5, EUCLID:53; ::_thesis: verum end; suppose q `1 < p1 `1 ; ::_thesis: contradiction then |[(q `1),(p `2)]| in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = p `2 & p `1 <= p2 `1 & p2 `1 <= p1 `1 ) } by A15, A14, A30; hence contradiction by A4, A9, A13, A17, Th10; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; end; end; hence ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p} ; ::_thesis: verum end; supposeA32: p1 `1 < p `1 ; ::_thesis: ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p} now__::_thesis:_(_(_p_`1_>_q_`1_&_contradiction_)_or_(_p_`1_<_q_`1_&_((LSeg_(p,|[(q_`1),(p_`2)]|))_\/_(LSeg_(|[(q_`1),(p_`2)]|,q)))_/\_(LSeg_(p1,p))_=_{p}_)_) percases ( p `1 > q `1 or p `1 < q `1 ) by A6, XXREAL_0:1; caseA33: p `1 > q `1 ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( q `1 > p1 `1 or q `1 = p1 `1 or q `1 < p1 `1 ) by XXREAL_0:1; suppose q `1 > p1 `1 ; ::_thesis: contradiction then |[(q `1),(p `2)]| in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `2 = p `2 & p1 `1 <= q2 `1 & q2 `1 <= p `1 ) } by A15, A14, A33; hence contradiction by A4, A9, A13, A32, Th10; ::_thesis: verum end; suppose q `1 = p1 `1 ; ::_thesis: contradiction hence contradiction by A1, A3, A5, EUCLID:53; ::_thesis: verum end; supposeA34: q `1 < p1 `1 ; ::_thesis: contradiction then p1 in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `2 = p `2 & |[(q `1),(p `2)]| `1 <= p2 `1 & p2 `1 <= p `1 ) } by A5, A15, A32; then p1 in LSeg (p,|[(q `1),(p `2)]|) by A13, A15, A32, A34, Th10, XXREAL_0:2; hence contradiction by A1, A8; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; caseA35: p `1 < q `1 ; ::_thesis: ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p} then A36: p `1 <= |[(q `1),(p `2)]| `1 by EUCLID:52; now__::_thesis:_((LSeg_(p,|[(q_`1),(p_`2)]|))_\/_(LSeg_(|[(q_`1),(p_`2)]|,q)))_/\_(LSeg_(p1,p))_=_{p} percases ( p `2 > q `2 or p `2 < q `2 ) by A7, XXREAL_0:1; supposeA37: p `2 > q `2 ; ::_thesis: ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p} ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) c= {p} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) or x in {p} ) assume A38: x in ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) ; ::_thesis: x in {p} now__::_thesis:_(_(_x_in_(LSeg_(p,|[(q_`1),(p_`2)]|))_/\_(LSeg_(p1,p))_&_x_in_{p}_)_or_(_x_in_(LSeg_(|[(q_`1),(p_`2)]|,q))_/\_(LSeg_(p1,p))_&_contradiction_)_) percases ( x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (p1,p)) or x in (LSeg (|[(q `1),(p `2)]|,q)) /\ (LSeg (p1,p)) ) by A11, A38, XBOOLE_0:def_3; caseA39: x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (p1,p)) ; ::_thesis: x in {p} p in { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `2 = p `2 & p1 `1 <= q1 `1 & q1 `1 <= |[(q `1),(p `2)]| `1 ) } by A32, A36; then p in LSeg (p1,|[(q `1),(p `2)]|) by A9, A15, A32, A35, Th10, XXREAL_0:2; hence x in {p} by A39, TOPREAL1:8; ::_thesis: verum end; caseA40: x in (LSeg (|[(q `1),(p `2)]|,q)) /\ (LSeg (p1,p)) ; ::_thesis: contradiction then x in LSeg (|[(q `1),(p `2)]|,q) by XBOOLE_0:def_4; then x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = q `1 & q `2 <= p2 `2 & p2 `2 <= p `2 ) } by A12, A37, Th9; then A41: ex p2 being Point of (TOP-REAL 2) st ( p2 = x & p2 `1 = q `1 & q `2 <= p2 `2 & p2 `2 <= p `2 ) ; x in LSeg (p1,p) by A40, XBOOLE_0:def_4; then x in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `2 = p `2 & p1 `1 <= q2 `1 & q2 `1 <= p `1 ) } by A9, A13, A32, Th10; then ex q2 being Point of (TOP-REAL 2) st ( q2 = x & q2 `2 = p `2 & p1 `1 <= q2 `1 & q2 `1 <= p `1 ) ; hence contradiction by A35, A41; ::_thesis: verum end; end; end; hence x in {p} ; ::_thesis: verum end; hence ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p} by A10, XBOOLE_0:def_10; ::_thesis: verum end; supposeA42: p `2 < q `2 ; ::_thesis: ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p} ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) c= {p} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) or x in {p} ) assume A43: x in ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) ; ::_thesis: x in {p} now__::_thesis:_(_(_x_in_(LSeg_(p,|[(q_`1),(p_`2)]|))_/\_(LSeg_(p1,p))_&_x_in_{p}_)_or_(_x_in_(LSeg_(|[(q_`1),(p_`2)]|,q))_/\_(LSeg_(p1,p))_&_contradiction_)_) percases ( x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (p1,p)) or x in (LSeg (|[(q `1),(p `2)]|,q)) /\ (LSeg (p1,p)) ) by A11, A43, XBOOLE_0:def_3; caseA44: x in (LSeg (p,|[(q `1),(p `2)]|)) /\ (LSeg (p1,p)) ; ::_thesis: x in {p} p in { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `2 = p `2 & p1 `1 <= q1 `1 & q1 `1 <= |[(q `1),(p `2)]| `1 ) } by A32, A36; then p in LSeg (p1,|[(q `1),(p `2)]|) by A9, A15, A32, A35, Th10, XXREAL_0:2; hence x in {p} by A44, TOPREAL1:8; ::_thesis: verum end; caseA45: x in (LSeg (|[(q `1),(p `2)]|,q)) /\ (LSeg (p1,p)) ; ::_thesis: contradiction then x in LSeg (p1,p) by XBOOLE_0:def_4; then x in { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `2 = p `2 & p1 `1 <= q2 `1 & q2 `1 <= p `1 ) } by A9, A13, A32, Th10; then A46: ex q2 being Point of (TOP-REAL 2) st ( q2 = x & q2 `2 = p `2 & p1 `1 <= q2 `1 & q2 `1 <= p `1 ) ; x in LSeg (|[(q `1),(p `2)]|,q) by A45, XBOOLE_0:def_4; then x in { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 = q `1 & |[(q `1),(p `2)]| `2 <= p2 `2 & p2 `2 <= q `2 ) } by A12, A14, A42, Th9; then ex p2 being Point of (TOP-REAL 2) st ( p2 = x & p2 `1 = q `1 & |[(q `1),(p `2)]| `2 <= p2 `2 & p2 `2 <= q `2 ) ; hence contradiction by A35, A46; ::_thesis: verum end; end; end; hence x in {p} ; ::_thesis: verum end; hence ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p} by A10, XBOOLE_0:def_10; ::_thesis: verum end; end; end; hence ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p} ; ::_thesis: verum end; end; end; hence ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p} ; ::_thesis: verum end; end; end; hence ((LSeg (p,|[(q `1),(p `2)]|)) \/ (LSeg (|[(q `1),(p `2)]|,q))) /\ (LSeg (p1,p)) = {p} ; ::_thesis: verum end; end; end; theorem Th45: :: TOPREAL3:45 for n being Element of NAT for f being FinSequence of REAL st len f = n holds f in the carrier of (Euclid n) proof let n be Element of NAT ; ::_thesis: for f being FinSequence of REAL st len f = n holds f in the carrier of (Euclid n) let f be FinSequence of REAL ; ::_thesis: ( len f = n implies f in the carrier of (Euclid n) ) ( f in REAL * & n -tuples_on REAL = { s where s is Element of REAL * : len s = n } ) by FINSEQ_1:def_11, FINSEQ_2:def_4; hence ( len f = n implies f in the carrier of (Euclid n) ) ; ::_thesis: verum end; theorem :: TOPREAL3:46 for n being Element of NAT for f being FinSequence of REAL st len f = n holds f in the carrier of (TOP-REAL n) proof let n be Element of NAT ; ::_thesis: for f being FinSequence of REAL st len f = n holds f in the carrier of (TOP-REAL n) let f be FinSequence of REAL ; ::_thesis: ( len f = n implies f in the carrier of (TOP-REAL n) ) assume len f = n ; ::_thesis: f in the carrier of (TOP-REAL n) then f in the carrier of (Euclid n) by Th45; hence f in the carrier of (TOP-REAL n) by Th8; ::_thesis: verum end;