:: SPPOL_1 semantic presentation begin theorem :: SPPOL_1:1 for n, k being Nat st n < k holds n <= k - 1 proof let n, k be Nat; ::_thesis: ( n < k implies n <= k - 1 ) assume n < k ; ::_thesis: n <= k - 1 then n + 1 <= k by NAT_1:13; then (n + 1) - 1 <= k - 1 by XREAL_1:9; hence n <= k - 1 ; ::_thesis: verum end; theorem :: SPPOL_1:2 for k, m, n being Element of NAT st 1 <= k - m & k - m <= n holds ( k - m in Seg n & k - m is Element of NAT ) proof let k, m, n be Element of NAT ; ::_thesis: ( 1 <= k - m & k - m <= n implies ( k - m in Seg n & k - m is Element of NAT ) ) assume that A1: 1 <= k - m and A2: k - m <= n ; ::_thesis: ( k - m in Seg n & k - m is Element of NAT ) k - m is Element of NAT by A1, INT_1:3; hence ( k - m in Seg n & k - m is Element of NAT ) by A1, A2, FINSEQ_1:1; ::_thesis: verum end; scheme :: SPPOL_1:sch 1 FinSeqFam{ F1() -> non empty set , F2() -> FinSequence of F1(), F3( FinSequence of F1(), Element of NAT ) -> set , P1[ Nat] } : { F3(F2(),i) where i is Element of NAT : ( i in dom F2() & P1[i] ) } is finite proof deffunc H1( Element of NAT ) -> set = F3(F2(),$1); set F = { H1(i) where i is Element of NAT : ( i in dom F2() & P1[i] ) } ; set F9 = { H1(i) where i is Element of NAT : i in dom F2() } ; A1: { H1(i) where i is Element of NAT : ( i in dom F2() & P1[i] ) } c= { H1(i) where i is Element of NAT : i in dom F2() } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { H1(i) where i is Element of NAT : ( i in dom F2() & P1[i] ) } or x in { H1(i) where i is Element of NAT : i in dom F2() } ) assume x in { H1(i) where i is Element of NAT : ( i in dom F2() & P1[i] ) } ; ::_thesis: x in { H1(i) where i is Element of NAT : i in dom F2() } then ex i being Element of NAT st ( x = F3(F2(),i) & i in dom F2() & P1[i] ) ; hence x in { H1(i) where i is Element of NAT : i in dom F2() } ; ::_thesis: verum end; A2: dom F2() is finite ; { H1(i) where i is Element of NAT : i in dom F2() } is finite from FRAENKEL:sch_21(A2); hence { F3(F2(),i) where i is Element of NAT : ( i in dom F2() & P1[i] ) } is finite by A1; ::_thesis: verum end; scheme :: SPPOL_1:sch 2 FinSeqFam9{ F1() -> non empty set , F2() -> FinSequence of F1(), F3( FinSequence of F1(), Element of NAT ) -> set , P1[ set ] } : { F3(F2(),i) where i is Element of NAT : ( 1 <= i & i <= len F2() & P1[i] ) } is finite proof deffunc H1( Element of NAT ) -> set = F3(F2(),$1); set F = { H1(i) where i is Element of NAT : ( 1 <= i & i <= len F2() & P1[i] ) } ; set F9 = { H1(i) where i is Element of NAT : i in dom F2() } ; A1: { H1(i) where i is Element of NAT : ( 1 <= i & i <= len F2() & P1[i] ) } c= { H1(i) where i is Element of NAT : i in dom F2() } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { H1(i) where i is Element of NAT : ( 1 <= i & i <= len F2() & P1[i] ) } or x in { H1(i) where i is Element of NAT : i in dom F2() } ) assume x in { H1(i) where i is Element of NAT : ( 1 <= i & i <= len F2() & P1[i] ) } ; ::_thesis: x in { H1(i) where i is Element of NAT : i in dom F2() } then consider i being Element of NAT such that A2: x = F3(F2(),i) and A3: ( 1 <= i & i <= len F2() ) and P1[i] ; i in dom F2() by A3, FINSEQ_3:25; hence x in { H1(i) where i is Element of NAT : i in dom F2() } by A2; ::_thesis: verum end; A4: dom F2() is finite ; { H1(i) where i is Element of NAT : i in dom F2() } is finite from FRAENKEL:sch_21(A4); hence { F3(F2(),i) where i is Element of NAT : ( 1 <= i & i <= len F2() & P1[i] ) } is finite by A1; ::_thesis: verum end; theorem Th3: :: SPPOL_1:3 for n being Element of NAT for x1, x2, x3 being Element of REAL n holds |.(x1 - x2).| - |.(x2 - x3).| <= |.(x1 - x3).| proof let n be Element of NAT ; ::_thesis: for x1, x2, x3 being Element of REAL n holds |.(x1 - x2).| - |.(x2 - x3).| <= |.(x1 - x3).| let x1, x2, x3 be Element of REAL n; ::_thesis: |.(x1 - x2).| - |.(x2 - x3).| <= |.(x1 - x3).| |.(x1 - x2).| <= |.(x1 - x3).| + |.(x3 - x2).| by EUCLID:19; then |.(x1 - x2).| <= |.(x1 - x3).| + |.(x2 - x3).| by EUCLID:18; then |.(x1 - x2).| - |.(x2 - x3).| <= (|.(x1 - x3).| + |.(x2 - x3).|) - |.(x2 - x3).| by XREAL_1:9; hence |.(x1 - x2).| - |.(x2 - x3).| <= |.(x1 - x3).| ; ::_thesis: verum end; theorem :: SPPOL_1:4 for n being Element of NAT for x1, x2, x3 being Element of REAL n holds |.(x2 - x1).| - |.(x2 - x3).| <= |.(x3 - x1).| proof let n be Element of NAT ; ::_thesis: for x1, x2, x3 being Element of REAL n holds |.(x2 - x1).| - |.(x2 - x3).| <= |.(x3 - x1).| let x1, x2, x3 be Element of REAL n; ::_thesis: |.(x2 - x1).| - |.(x2 - x3).| <= |.(x3 - x1).| |.(x2 - x1).| = |.(x1 - x2).| by EUCLID:18; then |.(x2 - x1).| - |.(x2 - x3).| <= |.(x1 - x3).| by Th3; hence |.(x2 - x1).| - |.(x2 - x3).| <= |.(x3 - x1).| by EUCLID:18; ::_thesis: verum end; begin theorem Th5: :: SPPOL_1:5 for n being Element of NAT for u1, u2 being Point of (Euclid n) for v1, v2 being Element of REAL n st v1 = u1 & v2 = u2 holds dist (u1,u2) = |.(v1 - v2).| proof let n be Element of NAT ; ::_thesis: for u1, u2 being Point of (Euclid n) for v1, v2 being Element of REAL n st v1 = u1 & v2 = u2 holds dist (u1,u2) = |.(v1 - v2).| let u1, u2 be Point of (Euclid n); ::_thesis: for v1, v2 being Element of REAL n st v1 = u1 & v2 = u2 holds dist (u1,u2) = |.(v1 - v2).| let v1, v2 be Element of REAL n; ::_thesis: ( v1 = u1 & v2 = u2 implies dist (u1,u2) = |.(v1 - v2).| ) assume ( v1 = u1 & v2 = u2 ) ; ::_thesis: dist (u1,u2) = |.(v1 - v2).| hence dist (u1,u2) = (Pitag_dist n) . (v1,v2) by METRIC_1:def_1 .= |.(v1 - v2).| by EUCLID:def_6 ; ::_thesis: verum end; theorem :: SPPOL_1:6 for n being Element of NAT for p1, p2 being Point of (TOP-REAL n) for P being non empty Subset of (TOP-REAL n) st P is closed & P c= LSeg (p1,p2) holds ex s being Real st ( ((1 - s) * p1) + (s * p2) in P & ( for r being Real st 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P holds s <= r ) ) proof let n be Element of NAT ; ::_thesis: for p1, p2 being Point of (TOP-REAL n) for P being non empty Subset of (TOP-REAL n) st P is closed & P c= LSeg (p1,p2) holds ex s being Real st ( ((1 - s) * p1) + (s * p2) in P & ( for r being Real st 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P holds s <= r ) ) let p1, p2 be Point of (TOP-REAL n); ::_thesis: for P being non empty Subset of (TOP-REAL n) st P is closed & P c= LSeg (p1,p2) holds ex s being Real st ( ((1 - s) * p1) + (s * p2) in P & ( for r being Real st 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P holds s <= r ) ) let P be non empty Subset of (TOP-REAL n); ::_thesis: ( P is closed & P c= LSeg (p1,p2) implies ex s being Real st ( ((1 - s) * p1) + (s * p2) in P & ( for r being Real st 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P holds s <= r ) ) ) set W = { r where r is Real : ( 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P ) } ; { r where r is Real : ( 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P ) } c= REAL proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { r where r is Real : ( 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P ) } or x in REAL ) assume x in { r where r is Real : ( 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P ) } ; ::_thesis: x in REAL then ex r being Real st ( r = x & 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P ) ; hence x in REAL ; ::_thesis: verum end; then reconsider W = { r where r is Real : ( 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P ) } as Subset of REAL ; assume that A1: P is closed and A2: P c= LSeg (p1,p2) ; ::_thesis: ex s being Real st ( ((1 - s) * p1) + (s * p2) in P & ( for r being Real st 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P holds s <= r ) ) take r2 = lower_bound W; ::_thesis: ( ((1 - r2) * p1) + (r2 * p2) in P & ( for r being Real st 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P holds r2 <= r ) ) A3: W is bounded_below proof take 0 ; :: according to XXREAL_2:def_9 ::_thesis: 0 is LowerBound of W let r be ext-real number ; :: according to XXREAL_2:def_2 ::_thesis: ( not r in W or 0 <= r ) assume r in W ; ::_thesis: 0 <= r then ex s being Real st ( s = r & 0 <= s & s <= 1 & ((1 - s) * p1) + (s * p2) in P ) ; hence 0 <= r ; ::_thesis: verum end; hereby ::_thesis: for r being Real st 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P holds r2 <= r set p = ((1 - r2) * p1) + (r2 * p2); reconsider u = ((1 - r2) * p1) + (r2 * p2) as Point of (Euclid n) by EUCLID:22; A4: TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def_8; then reconsider Q = P ` as Subset of (TopSpaceMetr (Euclid n)) ; P ` is open by A1, TOPS_1:3; then A5: Q is open by A4, PRE_TOPC:30; A6: ex r0 being Real st r0 in W proof consider v being Element of (TOP-REAL n) such that A7: v in P by SUBSET_1:4; v in LSeg (p1,p2) by A2, A7; then consider s being Real such that A8: ( v = ((1 - s) * p1) + (s * p2) & 0 <= s & s <= 1 ) ; s in { r where r is Real : ( 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P ) } by A7, A8; hence ex r0 being Real st r0 in W ; ::_thesis: verum end; assume A9: not ((1 - r2) * p1) + (r2 * p2) in P ; ::_thesis: contradiction then ((1 - r2) * p1) + (r2 * p2) in the carrier of (TOP-REAL n) \ P by XBOOLE_0:def_5; then consider r0 being real number such that A10: r0 > 0 and A11: Ball (u,r0) c= Q by A5, TOPMETR:15; percases ( p1 <> p2 or p1 = p2 ) ; supposeA12: p1 <> p2 ; ::_thesis: contradiction reconsider v2 = p2 as Element of REAL n by EUCLID:22; reconsider v1 = p1 as Element of REAL n by EUCLID:22; A13: |.(v2 - v1).| > 0 by A12, EUCLID:17; then r0 / |.(v2 - v1).| > 0 by A10, XREAL_1:139; then consider r4 being real number such that A14: r4 in W and A15: r4 < r2 + (r0 / |.(v2 - v1).|) by A3, A6, SEQ_4:def_2; reconsider r4 = r4 as Real by XREAL_0:def_1; r4 + 0 < r2 + (r0 / |.(v2 - v1).|) by A15; then A16: r4 - r2 < (r0 / |.(v2 - v1).|) - 0 by XREAL_1:21; set p3 = ((1 - r4) * p1) + (r4 * p2); reconsider u3 = ((1 - r4) * p1) + (r4 * p2) as Point of (Euclid n) by EUCLID:22; reconsider v3 = ((1 - r4) * p1) + (r4 * p2), v4 = ((1 - r2) * p1) + (r2 * p2) as Element of REAL n by EUCLID:22; A17: (((1 - r4) * p1) + (r4 * p2)) - (((1 - r2) * p1) + (r2 * p2)) = (((1 - r4) * p1) + (r4 * p2)) + ((- ((1 - r2) * p1)) - (r2 * p2)) by EUCLID:38 .= ((((1 - r4) * p1) + (r4 * p2)) + (- ((1 - r2) * p1))) + (- (r2 * p2)) by EUCLID:26 .= ((r4 * p2) + (((1 - r4) * p1) + (- ((1 - r2) * p1)))) + (- (r2 * p2)) by EUCLID:26 .= ((((1 - r4) * p1) + (- ((1 - r2) * p1))) + (r4 * p2)) + ((- r2) * p2) by EUCLID:40 .= ((((1 - r4) * p1) + ((- (1 - r2)) * p1)) + (r4 * p2)) + ((- r2) * p2) by EUCLID:40 .= (((1 - r4) * p1) + ((- (1 - r2)) * p1)) + ((r4 * p2) + ((- r2) * p2)) by EUCLID:26 .= (((1 - r4) * p1) + ((- (1 - r2)) * p1)) + ((r4 + (- r2)) * p2) by EUCLID:33 .= (((1 - r4) + (- (1 - r2))) * p1) + ((r4 - r2) * p2) by EUCLID:33 .= ((- (r4 - r2)) * p1) + ((r4 - r2) * p2) .= ((r4 - r2) * p2) - ((r4 - r2) * p1) by EUCLID:40 .= (r4 - r2) * (p2 - p1) by EUCLID:49 .= (r4 - r2) * (v2 - v1) ; r2 <= r4 by A3, A14, SEQ_4:def_2; then A18: r4 - r2 >= 0 by XREAL_1:48; dist (u3,u) = |.(v3 - v4).| by Th5 .= |.((((1 - r4) * p1) + (r4 * p2)) - (((1 - r2) * p1) + (r2 * p2))).| .= |.((r4 - r2) * (v2 - v1)).| by A17 .= (abs (r4 - r2)) * |.(v2 - v1).| by EUCLID:11 .= (r4 - r2) * |.(v2 - v1).| by A18, ABSVALUE:def_1 ; then dist (u3,u) < (r0 / |.(v2 - v1).|) * |.(v2 - v1).| by A13, A16, XREAL_1:68; then dist (u,u3) < r0 by A13, XCMPLX_1:87; then u3 in { u0 where u0 is Point of (Euclid n) : dist (u,u0) < r0 } ; then A19: u3 in Ball (u,r0) by METRIC_1:17; ex r being Real st ( r = r4 & 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P ) by A14; hence contradiction by A11, A19, XBOOLE_0:def_5; ::_thesis: verum end; supposeA20: p1 = p2 ; ::_thesis: contradiction then A21: LSeg (p1,p2) = {p1} by RLTOPSP1:70; A22: ex q1 being Point of (TOP-REAL n) st q1 in P by SUBSET_1:4; ((1 - r2) * p1) + (r2 * p2) = ((1 - r2) + r2) * p1 by A20, EUCLID:33 .= p1 by EUCLID:29 ; hence contradiction by A2, A9, A21, A22, TARSKI:def_1; ::_thesis: verum end; end; end; let r be Real; ::_thesis: ( 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P implies r2 <= r ) assume ( 0 <= r & r <= 1 & ((1 - r) * p1) + (r * p2) in P ) ; ::_thesis: r2 <= r then r in W ; hence r2 <= r by A3, SEQ_4:def_2; ::_thesis: verum end; theorem Th7: :: SPPOL_1:7 for n being Element of NAT for p1, p2, q1, q2 being Point of (TOP-REAL n) st LSeg (q1,q2) c= LSeg (p1,p2) & p1 in LSeg (q1,q2) & not p1 = q1 holds p1 = q2 proof let n be Element of NAT ; ::_thesis: for p1, p2, q1, q2 being Point of (TOP-REAL n) st LSeg (q1,q2) c= LSeg (p1,p2) & p1 in LSeg (q1,q2) & not p1 = q1 holds p1 = q2 let p1, p2, q1, q2 be Point of (TOP-REAL n); ::_thesis: ( LSeg (q1,q2) c= LSeg (p1,p2) & p1 in LSeg (q1,q2) & not p1 = q1 implies p1 = q2 ) assume A1: LSeg (q1,q2) c= LSeg (p1,p2) ; ::_thesis: ( not p1 in LSeg (q1,q2) or p1 = q1 or p1 = q2 ) q2 in LSeg (q1,q2) by RLTOPSP1:68; then q2 in LSeg (p1,p2) by A1; then consider s2 being Real such that A2: q2 = ((1 - s2) * p1) + (s2 * p2) and A3: 0 <= s2 and s2 <= 1 ; assume p1 in LSeg (q1,q2) ; ::_thesis: ( p1 = q1 or p1 = q2 ) then consider r1 being Real such that A4: p1 = ((1 - r1) * q1) + (r1 * q2) and A5: ( 0 <= r1 & r1 <= 1 ) ; A6: q1 in LSeg (q1,q2) by RLTOPSP1:68; then q1 in LSeg (p1,p2) by A1; then consider s1 being Real such that A7: q1 = ((1 - s1) * p1) + (s1 * p2) and A8: 0 <= s1 and s1 <= 1 ; p1 = ((1 - r1) * (((1 - s1) * p1) + (s1 * p2))) + ((r1 * ((1 - s2) * p1)) + (r1 * (s2 * p2))) by A4, A7, A2, EUCLID:32 .= (((1 - r1) * ((1 - s1) * p1)) + ((1 - r1) * (s1 * p2))) + ((r1 * ((1 - s2) * p1)) + (r1 * (s2 * p2))) by EUCLID:32 .= ((((1 - r1) * ((1 - s1) * p1)) + ((1 - r1) * (s1 * p2))) + (r1 * ((1 - s2) * p1))) + (r1 * (s2 * p2)) by EUCLID:26 .= (((((1 - r1) * (1 - s1)) * p1) + ((1 - r1) * (s1 * p2))) + (r1 * ((1 - s2) * p1))) + (r1 * (s2 * p2)) by EUCLID:30 .= (((((1 - r1) * (1 - s1)) * p1) + (((1 - r1) * s1) * p2)) + (r1 * ((1 - s2) * p1))) + (r1 * (s2 * p2)) by EUCLID:30 .= (((((1 - r1) * (1 - s1)) * p1) + (((1 - r1) * s1) * p2)) + ((r1 * (1 - s2)) * p1)) + (r1 * (s2 * p2)) by EUCLID:30 .= (((((1 - r1) * (1 - s1)) * p1) + (((1 - r1) * s1) * p2)) + ((r1 * (1 - s2)) * p1)) + ((r1 * s2) * p2) by EUCLID:30 .= (((r1 * s2) * p2) + ((((1 - r1) * s1) * p2) + (((1 - r1) * (1 - s1)) * p1))) + ((r1 * (1 - s2)) * p1) by EUCLID:26 .= ((((r1 * s2) * p2) + (((1 - r1) * s1) * p2)) + (((1 - r1) * (1 - s1)) * p1)) + ((r1 * (1 - s2)) * p1) by EUCLID:26 .= ((((r1 * s2) + ((1 - r1) * s1)) * p2) + (((1 - r1) * (1 - s1)) * p1)) + ((r1 * (1 - s2)) * p1) by EUCLID:33 .= (((r1 * s2) + ((1 - r1) * s1)) * p2) + ((((1 - r1) * (1 - s1)) * p1) + ((r1 * (1 - s2)) * p1)) by EUCLID:26 .= (((r1 * s2) + ((1 - r1) * s1)) * p2) + ((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) * p1) by EUCLID:33 ; then 0. (TOP-REAL n) = ((((r1 * s2) + ((1 - r1) * s1)) * p2) + ((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) * p1)) - p1 by EUCLID:42 .= (((r1 * s2) + ((1 - r1) * s1)) * p2) + (((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) * p1) - p1) by EUCLID:45 .= (((r1 * s2) + ((1 - r1) * s1)) * p2) + (((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) * p1) - (1 * p1)) by EUCLID:29 .= (((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) - 1) * p1) + (((r1 * s2) + ((1 - r1) * s1)) * p2) by EUCLID:50 .= (((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) - 1) * p1) - (- (((r1 * s2) + ((1 - r1) * s1)) * p2)) ; then ((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) - 1) * p1 = - (((r1 * s2) + ((1 - r1) * s1)) * p2) by EUCLID:43; then ((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) - 1) * p1 = (- ((r1 * s2) + ((1 - r1) * s1))) * p2 by EUCLID:40; then A9: ( - ((r1 * s2) + ((1 - r1) * s1)) = - 0 or p1 = p2 ) by EUCLID:34; percases ( (r1 * s2) + ((1 - r1) * s1) = 0 or p1 = p2 ) by A9; supposeA10: (r1 * s2) + ((1 - r1) * s1) = 0 ; ::_thesis: ( p1 = q1 or p1 = q2 ) now__::_thesis:_(_p1_=_q1_or_p1_=_q2_) percases ( ( r1 = 0 & s1 = 0 ) or ( r1 = 1 & s2 = 0 ) or ( s2 = 0 & s1 = 0 ) ) by A5, A8, A3, A10, XREAL_1:170; suppose ( r1 = 0 & s1 = 0 ) ; ::_thesis: ( p1 = q1 or p1 = q2 ) then p1 = (1 * q1) + (0. (TOP-REAL n)) by A4, EUCLID:29 .= q1 + (0. (TOP-REAL n)) by EUCLID:29 .= q1 by EUCLID:27 ; hence ( p1 = q1 or p1 = q2 ) ; ::_thesis: verum end; suppose ( r1 = 1 & s2 = 0 ) ; ::_thesis: ( p1 = q1 or p1 = q2 ) then p1 = (0. (TOP-REAL n)) + (1 * q2) by A4, EUCLID:29 .= 1 * q2 by EUCLID:27 .= q2 by EUCLID:29 ; hence ( p1 = q1 or p1 = q2 ) ; ::_thesis: verum end; suppose ( s2 = 0 & s1 = 0 ) ; ::_thesis: ( p1 = q1 or p1 = q2 ) then q1 = (1 * p1) + (0. (TOP-REAL n)) by A7, EUCLID:29 .= p1 + (0. (TOP-REAL n)) by EUCLID:29 .= p1 by EUCLID:27 ; hence ( p1 = q1 or p1 = q2 ) ; ::_thesis: verum end; end; end; hence ( p1 = q1 or p1 = q2 ) ; ::_thesis: verum end; suppose p1 = p2 ; ::_thesis: ( p1 = q1 or p1 = q2 ) then LSeg (q1,q2) c= {p1} by A1, RLTOPSP1:70; hence ( p1 = q1 or p1 = q2 ) by A6, TARSKI:def_1; ::_thesis: verum end; end; end; theorem :: SPPOL_1:8 for n being Element of NAT for p1, p2, q1, q2 being Point of (TOP-REAL n) holds ( not LSeg (p1,p2) = LSeg (q1,q2) or ( p1 = q1 & p2 = q2 ) or ( p1 = q2 & p2 = q1 ) ) proof let n be Element of NAT ; ::_thesis: for p1, p2, q1, q2 being Point of (TOP-REAL n) holds ( not LSeg (p1,p2) = LSeg (q1,q2) or ( p1 = q1 & p2 = q2 ) or ( p1 = q2 & p2 = q1 ) ) let p1, p2, q1, q2 be Point of (TOP-REAL n); ::_thesis: ( not LSeg (p1,p2) = LSeg (q1,q2) or ( p1 = q1 & p2 = q2 ) or ( p1 = q2 & p2 = q1 ) ) A1: q1 in LSeg (q1,q2) by RLTOPSP1:68; A2: q2 in LSeg (q1,q2) by RLTOPSP1:68; assume A3: LSeg (p1,p2) = LSeg (q1,q2) ; ::_thesis: ( ( p1 = q1 & p2 = q2 ) or ( p1 = q2 & p2 = q1 ) ) percases ( ( p1 = q1 & p2 = q1 ) or ( p1 = q2 & p2 = q2 ) or ( p1 = q1 & p2 = q2 ) or ( p1 = q2 & p2 = q1 ) ) by A3, Th7, RLTOPSP1:68; supposeA4: ( p1 = q1 & p2 = q1 ) ; ::_thesis: ( ( p1 = q1 & p2 = q2 ) or ( p1 = q2 & p2 = q1 ) ) then LSeg (p1,p2) = {q1} by RLTOPSP1:70; hence ( ( p1 = q1 & p2 = q2 ) or ( p1 = q2 & p2 = q1 ) ) by A3, A2, A4, TARSKI:def_1; ::_thesis: verum end; supposeA5: ( p1 = q2 & p2 = q2 ) ; ::_thesis: ( ( p1 = q1 & p2 = q2 ) or ( p1 = q2 & p2 = q1 ) ) then LSeg (p1,p2) = {q2} by RLTOPSP1:70; hence ( ( p1 = q1 & p2 = q2 ) or ( p1 = q2 & p2 = q1 ) ) by A3, A1, A5, TARSKI:def_1; ::_thesis: verum end; suppose ( ( p1 = q1 & p2 = q2 ) or ( p1 = q2 & p2 = q1 ) ) ; ::_thesis: ( ( p1 = q1 & p2 = q2 ) or ( p1 = q2 & p2 = q1 ) ) hence ( ( p1 = q1 & p2 = q2 ) or ( p1 = q2 & p2 = q1 ) ) ; ::_thesis: verum end; end; end; registration let n be Element of NAT ; let p1, p2 be Point of (TOP-REAL n); cluster LSeg (p1,p2) -> compact ; coherence LSeg (p1,p2) is compact proof set P = LSeg (p1,p2); set T = (TOP-REAL n) | (LSeg (p1,p2)); now__::_thesis:_(TOP-REAL_n)_|_(LSeg_(p1,p2))_is_compact percases ( p1 = p2 or p1 <> p2 ) ; suppose p1 = p2 ; ::_thesis: (TOP-REAL n) | (LSeg (p1,p2)) is compact then LSeg (p1,p2) = {p1} by RLTOPSP1:70; then A1: {p1} = [#] ((TOP-REAL n) | (LSeg (p1,p2))) by PRE_TOPC:def_5 .= the carrier of ((TOP-REAL n) | (LSeg (p1,p2))) ; then Sspace p1 = (TOP-REAL n) | (LSeg (p1,p2)) by TEX_2:def_2; then (TOP-REAL n) | (LSeg (p1,p2)) = 1TopSp {p1} by A1, TDLAT_3:def_1; hence (TOP-REAL n) | (LSeg (p1,p2)) is compact by PCOMPS_1:6; ::_thesis: verum end; suppose p1 <> p2 ; ::_thesis: (TOP-REAL n) | (LSeg (p1,p2)) is compact then LSeg (p1,p2) is_an_arc_of p1,p2 by TOPREAL1:9; then consider f being Function of I[01],((TOP-REAL n) | (LSeg (p1,p2))) such that A2: f is being_homeomorphism and f . 0 = p1 and f . 1 = p2 by TOPREAL1:def_1; A3: I[01] is compact by HEINE:4, TOPMETR:20; ( f is continuous & rng f = [#] ((TOP-REAL n) | (LSeg (p1,p2))) ) by A2, TOPS_2:def_5; hence (TOP-REAL n) | (LSeg (p1,p2)) is compact by A3, COMPTS_1:14; ::_thesis: verum end; end; end; hence LSeg (p1,p2) is compact by COMPTS_1:3; ::_thesis: verum end; cluster LSeg (p1,p2) -> closed ; coherence LSeg (p1,p2) is closed by COMPTS_1:7; end; definition let n be Element of NAT ; let p be Point of (TOP-REAL n); let P be Subset of (TOP-REAL n); predp is_extremal_in P means :Def1: :: SPPOL_1:def 1 ( p in P & ( for p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) & LSeg (p1,p2) c= P & not p = p1 holds p = p2 ) ); end; :: deftheorem Def1 defines is_extremal_in SPPOL_1:def_1_:_ for n being Element of NAT for p being Point of (TOP-REAL n) for P being Subset of (TOP-REAL n) holds ( p is_extremal_in P iff ( p in P & ( for p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) & LSeg (p1,p2) c= P & not p = p1 holds p = p2 ) ) ); theorem :: SPPOL_1:9 for n being Element of NAT for p being Point of (TOP-REAL n) for P, Q being Subset of (TOP-REAL n) st p is_extremal_in P & Q c= P & p in Q holds p is_extremal_in Q proof let n be Element of NAT ; ::_thesis: for p being Point of (TOP-REAL n) for P, Q being Subset of (TOP-REAL n) st p is_extremal_in P & Q c= P & p in Q holds p is_extremal_in Q let p be Point of (TOP-REAL n); ::_thesis: for P, Q being Subset of (TOP-REAL n) st p is_extremal_in P & Q c= P & p in Q holds p is_extremal_in Q let P, Q be Subset of (TOP-REAL n); ::_thesis: ( p is_extremal_in P & Q c= P & p in Q implies p is_extremal_in Q ) assume that A1: p is_extremal_in P and A2: Q c= P ; ::_thesis: ( not p in Q or p is_extremal_in Q ) assume p in Q ; ::_thesis: p is_extremal_in Q hence p in Q ; :: according to SPPOL_1:def_1 ::_thesis: for p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) & LSeg (p1,p2) c= Q & not p = p1 holds p = p2 let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( p in LSeg (p1,p2) & LSeg (p1,p2) c= Q & not p = p1 implies p = p2 ) assume A3: p in LSeg (p1,p2) ; ::_thesis: ( not LSeg (p1,p2) c= Q or p = p1 or p = p2 ) assume LSeg (p1,p2) c= Q ; ::_thesis: ( p = p1 or p = p2 ) then LSeg (p1,p2) c= P by A2, XBOOLE_1:1; hence ( p = p1 or p = p2 ) by A1, A3, Def1; ::_thesis: verum end; theorem :: SPPOL_1:10 for n being Element of NAT for p being Point of (TOP-REAL n) holds p is_extremal_in {p} proof let n be Element of NAT ; ::_thesis: for p being Point of (TOP-REAL n) holds p is_extremal_in {p} let p be Point of (TOP-REAL n); ::_thesis: p is_extremal_in {p} thus p in {p} by TARSKI:def_1; :: according to SPPOL_1:def_1 ::_thesis: for p1, p2 being Point of (TOP-REAL n) st p in LSeg (p1,p2) & LSeg (p1,p2) c= {p} & not p = p1 holds p = p2 let p1, p2 be Point of (TOP-REAL n); ::_thesis: ( p in LSeg (p1,p2) & LSeg (p1,p2) c= {p} & not p = p1 implies p = p2 ) assume that p in LSeg (p1,p2) and A1: LSeg (p1,p2) c= {p} ; ::_thesis: ( p = p1 or p = p2 ) p2 in LSeg (p1,p2) by RLTOPSP1:68; hence ( p = p1 or p = p2 ) by A1, TARSKI:def_1; ::_thesis: verum end; theorem Th11: :: SPPOL_1:11 for n being Element of NAT for p1, p2 being Point of (TOP-REAL n) holds p1 is_extremal_in LSeg (p1,p2) proof let n be Element of NAT ; ::_thesis: for p1, p2 being Point of (TOP-REAL n) holds p1 is_extremal_in LSeg (p1,p2) let p1, p2 be Point of (TOP-REAL n); ::_thesis: p1 is_extremal_in LSeg (p1,p2) thus p1 in LSeg (p1,p2) by RLTOPSP1:68; :: according to SPPOL_1:def_1 ::_thesis: for p1, p2 being Point of (TOP-REAL n) st p1 in LSeg (p1,p2) & LSeg (p1,p2) c= LSeg (p1,p2) & not p1 = p1 holds p1 = p2 let q1, q2 be Point of (TOP-REAL n); ::_thesis: ( p1 in LSeg (q1,q2) & LSeg (q1,q2) c= LSeg (p1,p2) & not p1 = q1 implies p1 = q2 ) thus ( p1 in LSeg (q1,q2) & LSeg (q1,q2) c= LSeg (p1,p2) & not p1 = q1 implies p1 = q2 ) by Th7; ::_thesis: verum end; theorem :: SPPOL_1:12 for n being Element of NAT for p2, p1 being Point of (TOP-REAL n) holds p2 is_extremal_in LSeg (p1,p2) by Th11; theorem :: SPPOL_1:13 for n being Element of NAT for p, p1, p2 being Point of (TOP-REAL n) holds ( not p is_extremal_in LSeg (p1,p2) or p = p1 or p = p2 ) proof let n be Element of NAT ; ::_thesis: for p, p1, p2 being Point of (TOP-REAL n) holds ( not p is_extremal_in LSeg (p1,p2) or p = p1 or p = p2 ) let p, p1, p2 be Point of (TOP-REAL n); ::_thesis: ( not p is_extremal_in LSeg (p1,p2) or p = p1 or p = p2 ) assume A1: p is_extremal_in LSeg (p1,p2) ; ::_thesis: ( p = p1 or p = p2 ) thus ( p = p1 or p = p2 ) by A1, Def1; ::_thesis: verum end; begin theorem Th14: :: SPPOL_1:14 for p1, p2 being Point of (TOP-REAL 2) st p1 `1 <> p2 `1 & p1 `2 <> p2 `2 holds ex p being Point of (TOP-REAL 2) st ( p in LSeg (p1,p2) & p `1 <> p1 `1 & p `1 <> p2 `1 & p `2 <> p1 `2 & p `2 <> p2 `2 ) proof let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( p1 `1 <> p2 `1 & p1 `2 <> p2 `2 implies ex p being Point of (TOP-REAL 2) st ( p in LSeg (p1,p2) & p `1 <> p1 `1 & p `1 <> p2 `1 & p `2 <> p1 `2 & p `2 <> p2 `2 ) ) assume that A1: p1 `1 <> p2 `1 and A2: p1 `2 <> p2 `2 ; ::_thesis: ex p being Point of (TOP-REAL 2) st ( p in LSeg (p1,p2) & p `1 <> p1 `1 & p `1 <> p2 `1 & p `2 <> p1 `2 & p `2 <> p2 `2 ) take p = (1 / 2) * (p1 + p2); ::_thesis: ( p in LSeg (p1,p2) & p `1 <> p1 `1 & p `1 <> p2 `1 & p `2 <> p1 `2 & p `2 <> p2 `2 ) A3: p = ((1 - (1 / 2)) * p1) + ((1 / 2) * p2) by EUCLID:32; hence p in LSeg (p1,p2) ; ::_thesis: ( p `1 <> p1 `1 & p `1 <> p2 `1 & p `2 <> p1 `2 & p `2 <> p2 `2 ) hereby ::_thesis: ( p `1 <> p2 `1 & p `2 <> p1 `2 & p `2 <> p2 `2 ) assume A4: p `1 = p1 `1 ; ::_thesis: contradiction p `1 = (((1 - (1 / 2)) * p1) `1) + (((1 / 2) * p2) `1) by A3, TOPREAL3:2 .= ((1 - (1 / 2)) * (p1 `1)) + (((1 / 2) * p2) `1) by TOPREAL3:4 .= ((1 - (1 / 2)) * (p `1)) + ((1 / 2) * (p2 `1)) by A4, TOPREAL3:4 ; hence contradiction by A1, A4; ::_thesis: verum end; hereby ::_thesis: ( p `2 <> p1 `2 & p `2 <> p2 `2 ) assume A5: p `1 = p2 `1 ; ::_thesis: contradiction p `1 = (((1 - (1 / 2)) * p1) `1) + (((1 / 2) * p2) `1) by A3, TOPREAL3:2 .= ((1 - (1 / 2)) * (p1 `1)) + (((1 / 2) * p2) `1) by TOPREAL3:4 .= ((1 - (1 / 2)) * (p1 `1)) + ((1 / 2) * (p `1)) by A5, TOPREAL3:4 ; hence contradiction by A1, A5; ::_thesis: verum end; hereby ::_thesis: p `2 <> p2 `2 assume A6: p `2 = p1 `2 ; ::_thesis: contradiction p `2 = (((1 - (1 / 2)) * p1) `2) + (((1 / 2) * p2) `2) by A3, TOPREAL3:2 .= ((1 - (1 / 2)) * (p1 `2)) + (((1 / 2) * p2) `2) by TOPREAL3:4 .= ((1 - (1 / 2)) * (p `2)) + ((1 / 2) * (p2 `2)) by A6, TOPREAL3:4 ; hence contradiction by A2, A6; ::_thesis: verum end; hereby ::_thesis: verum assume A7: p `2 = p2 `2 ; ::_thesis: contradiction p `2 = (((1 - (1 / 2)) * p1) `2) + (((1 / 2) * p2) `2) by A3, TOPREAL3:2 .= ((1 - (1 / 2)) * (p1 `2)) + (((1 / 2) * p2) `2) by TOPREAL3:4 .= ((1 - (1 / 2)) * (p1 `2)) + ((1 / 2) * (p `2)) by A7, TOPREAL3:4 ; hence contradiction by A2, A7; ::_thesis: verum end; end; definition let P be Subset of (TOP-REAL 2); attrP is horizontal means :Def2: :: SPPOL_1:def 2 for p, q being Point of (TOP-REAL 2) st p in P & q in P holds p `2 = q `2 ; attrP is vertical means :Def3: :: SPPOL_1:def 3 for p, q being Point of (TOP-REAL 2) st p in P & q in P holds p `1 = q `1 ; end; :: deftheorem Def2 defines horizontal SPPOL_1:def_2_:_ for P being Subset of (TOP-REAL 2) holds ( P is horizontal iff for p, q being Point of (TOP-REAL 2) st p in P & q in P holds p `2 = q `2 ); :: deftheorem Def3 defines vertical SPPOL_1:def_3_:_ for P being Subset of (TOP-REAL 2) holds ( P is vertical iff for p, q being Point of (TOP-REAL 2) st p in P & q in P holds p `1 = q `1 ); Lm1: for P being Subset of (TOP-REAL 2) st not P is trivial & P is horizontal holds not P is vertical proof let P be Subset of (TOP-REAL 2); ::_thesis: ( not P is trivial & P is horizontal implies not P is vertical ) assume that A1: not P is trivial and A2: ( ( for p, q being Point of (TOP-REAL 2) st p in P & q in P holds p `2 = q `2 ) & ( for p, q being Point of (TOP-REAL 2) st p in P & q in P holds p `1 = q `1 ) ) ; :: according to SPPOL_1:def_2,SPPOL_1:def_3 ::_thesis: contradiction consider p, q being Point of (TOP-REAL 2) such that A3: ( p in P & q in P ) and A4: p <> q by A1, SUBSET_1:45; ( p `2 = q `2 & p `1 = q `1 ) by A2, A3; hence contradiction by A4, TOPREAL3:6; ::_thesis: verum end; registration cluster non trivial horizontal -> non vertical for Element of bool the carrier of (TOP-REAL 2); coherence for b1 being Subset of (TOP-REAL 2) st not b1 is trivial & b1 is horizontal holds not b1 is vertical by Lm1; cluster non trivial vertical -> non horizontal for Element of bool the carrier of (TOP-REAL 2); coherence for b1 being Subset of (TOP-REAL 2) st not b1 is trivial & b1 is vertical holds not b1 is horizontal ; end; theorem Th15: :: SPPOL_1:15 for p, q being Point of (TOP-REAL 2) holds ( p `2 = q `2 iff LSeg (p,q) is horizontal ) proof let p, q be Point of (TOP-REAL 2); ::_thesis: ( p `2 = q `2 iff LSeg (p,q) is horizontal ) set P = LSeg (p,q); thus ( p `2 = q `2 implies LSeg (p,q) is horizontal ) ::_thesis: ( LSeg (p,q) is horizontal implies p `2 = q `2 ) proof assume A1: p `2 = q `2 ; ::_thesis: LSeg (p,q) is horizontal let p1 be Point of (TOP-REAL 2); :: according to SPPOL_1:def_2 ::_thesis: for q being Point of (TOP-REAL 2) st p1 in LSeg (p,q) & q in LSeg (p,q) holds p1 `2 = q `2 let p2 be Point of (TOP-REAL 2); ::_thesis: ( p1 in LSeg (p,q) & p2 in LSeg (p,q) implies p1 `2 = p2 `2 ) assume A2: p1 in LSeg (p,q) ; ::_thesis: ( not p2 in LSeg (p,q) or p1 `2 = p2 `2 ) assume p2 in LSeg (p,q) ; ::_thesis: p1 `2 = p2 `2 then A3: ( p `2 <= p2 `2 & p2 `2 <= p `2 ) by A1, TOPREAL1:4; ( p `2 <= p1 `2 & p1 `2 <= p `2 ) by A1, A2, TOPREAL1:4; then p `2 = p1 `2 by XXREAL_0:1; hence p1 `2 = p2 `2 by A3, XXREAL_0:1; ::_thesis: verum end; ( p in LSeg (p,q) & q in LSeg (p,q) ) by RLTOPSP1:68; hence ( LSeg (p,q) is horizontal implies p `2 = q `2 ) by Def2; ::_thesis: verum end; theorem Th16: :: SPPOL_1:16 for p, q being Point of (TOP-REAL 2) holds ( p `1 = q `1 iff LSeg (p,q) is vertical ) proof let p, q be Point of (TOP-REAL 2); ::_thesis: ( p `1 = q `1 iff LSeg (p,q) is vertical ) set P = LSeg (p,q); thus ( p `1 = q `1 implies LSeg (p,q) is vertical ) ::_thesis: ( LSeg (p,q) is vertical implies p `1 = q `1 ) proof assume A1: p `1 = q `1 ; ::_thesis: LSeg (p,q) is vertical let p1 be Point of (TOP-REAL 2); :: according to SPPOL_1:def_3 ::_thesis: for q being Point of (TOP-REAL 2) st p1 in LSeg (p,q) & q in LSeg (p,q) holds p1 `1 = q `1 let p2 be Point of (TOP-REAL 2); ::_thesis: ( p1 in LSeg (p,q) & p2 in LSeg (p,q) implies p1 `1 = p2 `1 ) assume A2: p1 in LSeg (p,q) ; ::_thesis: ( not p2 in LSeg (p,q) or p1 `1 = p2 `1 ) assume p2 in LSeg (p,q) ; ::_thesis: p1 `1 = p2 `1 then A3: ( p `1 <= p2 `1 & p2 `1 <= p `1 ) by A1, TOPREAL1:3; ( p `1 <= p1 `1 & p1 `1 <= p `1 ) by A1, A2, TOPREAL1:3; then p `1 = p1 `1 by XXREAL_0:1; hence p1 `1 = p2 `1 by A3, XXREAL_0:1; ::_thesis: verum end; ( p in LSeg (p,q) & q in LSeg (p,q) ) by RLTOPSP1:68; hence ( LSeg (p,q) is vertical implies p `1 = q `1 ) by Def3; ::_thesis: verum end; theorem :: SPPOL_1:17 for p1, p, q, p2 being Point of (TOP-REAL 2) st p1 in LSeg (p,q) & p2 in LSeg (p,q) & p1 `1 <> p2 `1 & p1 `2 = p2 `2 holds LSeg (p,q) is horizontal proof let p1, p, q, p2 be Point of (TOP-REAL 2); ::_thesis: ( p1 in LSeg (p,q) & p2 in LSeg (p,q) & p1 `1 <> p2 `1 & p1 `2 = p2 `2 implies LSeg (p,q) is horizontal ) assume p1 in LSeg (p,q) ; ::_thesis: ( not p2 in LSeg (p,q) or not p1 `1 <> p2 `1 or not p1 `2 = p2 `2 or LSeg (p,q) is horizontal ) then consider r1 being Real such that A1: p1 = ((1 - r1) * p) + (r1 * q) and 0 <= r1 and r1 <= 1 ; assume p2 in LSeg (p,q) ; ::_thesis: ( not p1 `1 <> p2 `1 or not p1 `2 = p2 `2 or LSeg (p,q) is horizontal ) then consider r2 being Real such that A2: p2 = ((1 - r2) * p) + (r2 * q) and 0 <= r2 and r2 <= 1 ; assume that A3: p1 `1 <> p2 `1 and A4: p1 `2 = p2 `2 ; ::_thesis: LSeg (p,q) is horizontal (p `2) - ((r1 * (p `2)) - (r1 * (q `2))) = ((1 - r1) * (p `2)) + (r1 * (q `2)) .= ((1 - r1) * (p `2)) + ((r1 * q) `2) by TOPREAL3:4 .= (((1 - r1) * p) `2) + ((r1 * q) `2) by TOPREAL3:4 .= p1 `2 by A1, TOPREAL3:2 .= (((1 - r2) * p) `2) + ((r2 * q) `2) by A2, A4, TOPREAL3:2 .= ((1 - r2) * (p `2)) + ((r2 * q) `2) by TOPREAL3:4 .= ((1 * (p `2)) - (r2 * (p `2))) + (r2 * (q `2)) by TOPREAL3:4 .= (p `2) - ((r2 * (p `2)) - (r2 * (q `2))) ; then A5: (r1 - r2) * (p `2) = (r1 - r2) * (q `2) ; r1 - r2 <> 0 by A1, A2, A3; then p `2 = q `2 by A5, XCMPLX_1:5; hence LSeg (p,q) is horizontal by Th15; ::_thesis: verum end; theorem :: SPPOL_1:18 for p1, p, q, p2 being Point of (TOP-REAL 2) st p1 in LSeg (p,q) & p2 in LSeg (p,q) & p1 `2 <> p2 `2 & p1 `1 = p2 `1 holds LSeg (p,q) is vertical proof let p1, p, q, p2 be Point of (TOP-REAL 2); ::_thesis: ( p1 in LSeg (p,q) & p2 in LSeg (p,q) & p1 `2 <> p2 `2 & p1 `1 = p2 `1 implies LSeg (p,q) is vertical ) assume p1 in LSeg (p,q) ; ::_thesis: ( not p2 in LSeg (p,q) or not p1 `2 <> p2 `2 or not p1 `1 = p2 `1 or LSeg (p,q) is vertical ) then consider r1 being Real such that A1: p1 = ((1 - r1) * p) + (r1 * q) and 0 <= r1 and r1 <= 1 ; assume p2 in LSeg (p,q) ; ::_thesis: ( not p1 `2 <> p2 `2 or not p1 `1 = p2 `1 or LSeg (p,q) is vertical ) then consider r2 being Real such that A2: p2 = ((1 - r2) * p) + (r2 * q) and 0 <= r2 and r2 <= 1 ; assume that A3: p1 `2 <> p2 `2 and A4: p1 `1 = p2 `1 ; ::_thesis: LSeg (p,q) is vertical (p `1) - ((r1 * (p `1)) - (r1 * (q `1))) = ((1 - r1) * (p `1)) + (r1 * (q `1)) .= ((1 - r1) * (p `1)) + ((r1 * q) `1) by TOPREAL3:4 .= (((1 - r1) * p) `1) + ((r1 * q) `1) by TOPREAL3:4 .= p1 `1 by A1, TOPREAL3:2 .= (((1 - r2) * p) `1) + ((r2 * q) `1) by A2, A4, TOPREAL3:2 .= ((1 - r2) * (p `1)) + ((r2 * q) `1) by TOPREAL3:4 .= ((1 * (p `1)) - (r2 * (p `1))) + (r2 * (q `1)) by TOPREAL3:4 .= (p `1) - ((r2 * (p `1)) - (r2 * (q `1))) ; then A5: (r1 - r2) * (p `1) = (r1 - r2) * (q `1) ; r1 - r2 <> 0 by A1, A2, A3; then p `1 = q `1 by A5, XCMPLX_1:5; hence LSeg (p,q) is vertical by Th16; ::_thesis: verum end; registration let f be FinSequence of the carrier of (TOP-REAL 2); let i be Element of NAT ; cluster LSeg (f,i) -> closed ; coherence LSeg (f,i) is closed proof percases ( ( 1 <= i & i + 1 <= len f ) or not 1 <= i or not i + 1 <= len f ) ; suppose ( 1 <= i & i + 1 <= len f ) ; ::_thesis: LSeg (f,i) is closed then LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by TOPREAL1:def_3; hence LSeg (f,i) is closed ; ::_thesis: verum end; supposeA1: ( not 1 <= i or not i + 1 <= len f ) ; ::_thesis: LSeg (f,i) is closed {} (TOP-REAL 2) is closed ; hence LSeg (f,i) is closed by A1, TOPREAL1:def_3; ::_thesis: verum end; end; end; end; theorem Th19: :: SPPOL_1:19 for i being Element of NAT for f being FinSequence of the carrier of (TOP-REAL 2) holds ( not f is special or LSeg (f,i) is vertical or LSeg (f,i) is horizontal ) proof let i be Element of NAT ; ::_thesis: for f being FinSequence of the carrier of (TOP-REAL 2) holds ( not f is special or LSeg (f,i) is vertical or LSeg (f,i) is horizontal ) let f be FinSequence of the carrier of (TOP-REAL 2); ::_thesis: ( not f is special or LSeg (f,i) is vertical or LSeg (f,i) is horizontal ) assume A1: for j being Nat st 1 <= j & j + 1 <= len f & not (f /. j) `1 = (f /. (j + 1)) `1 holds (f /. j) `2 = (f /. (j + 1)) `2 ; :: according to TOPREAL1:def_5 ::_thesis: ( LSeg (f,i) is vertical or LSeg (f,i) is horizontal ) set p1 = f /. i; set p2 = f /. (i + 1); percases ( ( 1 <= i & i + 1 <= len f ) or not 1 <= i or not i + 1 <= len f ) ; supposeA2: ( 1 <= i & i + 1 <= len f ) ; ::_thesis: ( LSeg (f,i) is vertical or LSeg (f,i) is horizontal ) A3: ( (f /. i) `2 = (f /. (i + 1)) `2 implies LSeg ((f /. i),(f /. (i + 1))) is horizontal ) by Th15; ( (f /. i) `1 = (f /. (i + 1)) `1 implies LSeg ((f /. i),(f /. (i + 1))) is vertical ) by Th16; hence ( LSeg (f,i) is vertical or LSeg (f,i) is horizontal ) by A1, A2, A3, TOPREAL1:def_3; ::_thesis: verum end; suppose ( not 1 <= i or not i + 1 <= len f ) ; ::_thesis: ( LSeg (f,i) is vertical or LSeg (f,i) is horizontal ) then for p, q being Point of (TOP-REAL 2) st p in LSeg (f,i) & q in LSeg (f,i) holds p `2 = q `2 by TOPREAL1:def_3; hence ( LSeg (f,i) is vertical or LSeg (f,i) is horizontal ) by Def2; ::_thesis: verum end; end; end; theorem Th20: :: SPPOL_1:20 for i being Element of NAT for f being FinSequence of the carrier of (TOP-REAL 2) st f is one-to-one & 1 <= i & i + 1 <= len f holds not LSeg (f,i) is trivial proof let i be Element of NAT ; ::_thesis: for f being FinSequence of the carrier of (TOP-REAL 2) st f is one-to-one & 1 <= i & i + 1 <= len f holds not LSeg (f,i) is trivial let f be FinSequence of the carrier of (TOP-REAL 2); ::_thesis: ( f is one-to-one & 1 <= i & i + 1 <= len f implies not LSeg (f,i) is trivial ) assume A1: f is one-to-one ; ::_thesis: ( not 1 <= i or not i + 1 <= len f or not LSeg (f,i) is trivial ) A2: i <> i + 1 ; assume A3: ( 1 <= i & i + 1 <= len f ) ; ::_thesis: not LSeg (f,i) is trivial then ( i in dom f & i + 1 in dom f ) by SEQ_4:134; then A4: f /. i <> f /. (i + 1) by A1, A2, PARTFUN2:10; A5: ( f /. i in LSeg ((f /. i),(f /. (i + 1))) & f /. (i + 1) in LSeg ((f /. i),(f /. (i + 1))) ) by RLTOPSP1:68; LSeg ((f /. i),(f /. (i + 1))) = LSeg (f,i) by A3, TOPREAL1:def_3; hence not LSeg (f,i) is trivial by A4, A5, ZFMISC_1:def_10; ::_thesis: verum end; theorem :: SPPOL_1:21 for i being Element of NAT for f being FinSequence of the carrier of (TOP-REAL 2) st f is one-to-one & 1 <= i & i + 1 <= len f & LSeg (f,i) is vertical holds not LSeg (f,i) is horizontal by Lm1, Th20; theorem Th22: :: SPPOL_1:22 for f being FinSequence of the carrier of (TOP-REAL 2) holds { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i <= len f ) } is finite proof defpred S1[ set ] means verum; deffunc H1( FinSequence of (TOP-REAL 2), Element of NAT ) -> Element of bool the carrier of (TOP-REAL 2) = LSeg ($1,$2); let f be FinSequence of the carrier of (TOP-REAL 2); ::_thesis: { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i <= len f ) } is finite set Y = { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i <= len f ) } ; set X = { H1(f,i) where i is Element of NAT : ( 1 <= i & i <= len f & S1[i] ) } ; A1: for e being set holds ( e in { H1(f,i) where i is Element of NAT : ( 1 <= i & i <= len f & S1[i] ) } iff e in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i <= len f ) } ) proof let e be set ; ::_thesis: ( e in { H1(f,i) where i is Element of NAT : ( 1 <= i & i <= len f & S1[i] ) } iff e in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i <= len f ) } ) thus ( e in { H1(f,i) where i is Element of NAT : ( 1 <= i & i <= len f & S1[i] ) } implies e in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i <= len f ) } ) ::_thesis: ( e in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i <= len f ) } implies e in { H1(f,i) where i is Element of NAT : ( 1 <= i & i <= len f & S1[i] ) } ) proof assume e in { H1(f,i) where i is Element of NAT : ( 1 <= i & i <= len f & S1[i] ) } ; ::_thesis: e in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i <= len f ) } then ex i being Element of NAT st ( e = H1(f,i) & 1 <= i & i <= len f & S1[i] ) ; hence e in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i <= len f ) } ; ::_thesis: verum end; assume e in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i <= len f ) } ; ::_thesis: e in { H1(f,i) where i is Element of NAT : ( 1 <= i & i <= len f & S1[i] ) } then ex i being Element of NAT st ( e = LSeg (f,i) & 1 <= i & i <= len f ) ; hence e in { H1(f,i) where i is Element of NAT : ( 1 <= i & i <= len f & S1[i] ) } ; ::_thesis: verum end; { H1(f,i) where i is Element of NAT : ( 1 <= i & i <= len f & S1[i] ) } is finite from SPPOL_1:sch_2(); hence { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i <= len f ) } is finite by A1, TARSKI:1; ::_thesis: verum end; theorem Th23: :: SPPOL_1:23 for f being FinSequence of the carrier of (TOP-REAL 2) holds { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } is finite proof let f be FinSequence of the carrier of (TOP-REAL 2); ::_thesis: { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } is finite set F = { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ; set F9 = { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i <= len f ) } ; { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } c= { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i <= 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 (f,i)) where i is Element of NAT : ( 1 <= i & i <= len f ) } ) assume x in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ; ::_thesis: x in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i <= len f ) } then consider i being Element of NAT such that A1: ( x = LSeg (f,i) & 1 <= i ) and A2: i + 1 <= len f ; i <= i + 1 by NAT_1:11; then i <= len f by A2, XXREAL_0:2; hence x in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i <= len f ) } by A1; ::_thesis: verum end; hence { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } is finite by Th22, FINSET_1:1; ::_thesis: verum end; Lm2: for f being FinSequence of the carrier of (TOP-REAL 2) for k being Element of NAT holds { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } is finite proof let f be FinSequence of the carrier of (TOP-REAL 2); ::_thesis: for k being Element of NAT holds { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } is finite let k be Element of NAT ; ::_thesis: { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } is finite set F = { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } ; set F1 = { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ; { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } 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 & i <> k & i <> k + 1 ) } or x in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ) assume x in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } ; ::_thesis: x in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } then ex i being Element of NAT st ( LSeg (f,i) = x & 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) ; hence x in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ; ::_thesis: verum end; hence { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } is finite by Th23, FINSET_1:1; ::_thesis: verum end; theorem :: SPPOL_1:24 for f being FinSequence of the carrier of (TOP-REAL 2) holds { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i <= len f ) } is Subset-Family of (TOP-REAL 2) proof let f be FinSequence of the carrier of (TOP-REAL 2); ::_thesis: { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i <= len f ) } is Subset-Family of (TOP-REAL 2) set F = { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i <= len f ) } ; { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i <= len f ) } c= bool (REAL 2) 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 <= len f ) } or x in bool (REAL 2) ) assume x in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i <= len f ) } ; ::_thesis: x in bool (REAL 2) then ex i being Element of NAT st ( LSeg (f,i) = x & 1 <= i & i <= len f ) ; then x is Subset of (REAL 2) by EUCLID:22; hence x in bool (REAL 2) ; ::_thesis: verum end; hence { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i <= len f ) } is Subset-Family of (TOP-REAL 2) by EUCLID:22; ::_thesis: verum end; theorem Th25: :: SPPOL_1:25 for f being FinSequence of the carrier of (TOP-REAL 2) holds { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } is Subset-Family of (TOP-REAL 2) proof let f be FinSequence of the carrier of (TOP-REAL 2); ::_thesis: { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } is Subset-Family of (TOP-REAL 2) set F = { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ; { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } c= bool (REAL 2) 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 bool (REAL 2) ) assume x in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ; ::_thesis: x in bool (REAL 2) then ex i being Element of NAT st ( LSeg (f,i) = x & 1 <= i & i + 1 <= len f ) ; then x is Subset of (REAL 2) by EUCLID:22; hence x in bool (REAL 2) ; ::_thesis: verum end; hence { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } is Subset-Family of (TOP-REAL 2) by EUCLID:22; ::_thesis: verum end; Lm3: for f being FinSequence of the carrier of (TOP-REAL 2) for k being Element of NAT holds { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } is Subset-Family of (TOP-REAL 2) proof let f be FinSequence of the carrier of (TOP-REAL 2); ::_thesis: for k being Element of NAT holds { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } is Subset-Family of (TOP-REAL 2) let k be Element of NAT ; ::_thesis: { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } is Subset-Family of (TOP-REAL 2) set F = { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } ; { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } c= bool (REAL 2) 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 & i <> k & i <> k + 1 ) } or x in bool (REAL 2) ) assume x in { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } ; ::_thesis: x in bool (REAL 2) then ex i being Element of NAT st ( LSeg (f,i) = x & 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) ; then x is Subset of (REAL 2) by EUCLID:22; hence x in bool (REAL 2) ; ::_thesis: verum end; hence { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } is Subset-Family of (TOP-REAL 2) by EUCLID:22; ::_thesis: verum end; theorem Th26: :: SPPOL_1:26 for Q being Subset of (TOP-REAL 2) for f being FinSequence of the carrier of (TOP-REAL 2) st Q = union { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } holds Q is closed proof let Q be Subset of (TOP-REAL 2); ::_thesis: for f being FinSequence of the carrier of (TOP-REAL 2) st Q = union { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } holds Q is closed let f be FinSequence of the carrier of (TOP-REAL 2); ::_thesis: ( Q = union { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } implies Q is closed ) reconsider F = { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } as Subset-Family of (TOP-REAL 2) by Th25; now__::_thesis:_for_P_being_Subset_of_(TOP-REAL_2)_st_P_in_F_holds_ P_is_closed let P be Subset of (TOP-REAL 2); ::_thesis: ( P in F implies P is closed ) assume P in F ; ::_thesis: P is closed then ex i being Element of NAT st ( LSeg (f,i) = P & 1 <= i & i + 1 <= len f ) ; hence P is closed ; ::_thesis: verum end; then A1: F is closed by TOPS_2:def_2; F is finite by Th23; hence ( Q = union { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } implies Q is closed ) by A1, TOPS_2:21; ::_thesis: verum end; registration let f be FinSequence of the carrier of (TOP-REAL 2); cluster L~ f -> closed ; coherence L~ f is closed by Th26; end; Lm4: for f being FinSequence of the carrier of (TOP-REAL 2) for Q being Subset of (TOP-REAL 2) for k being Element of NAT st Q = union { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } holds Q is closed proof let f be FinSequence of the carrier of (TOP-REAL 2); ::_thesis: for Q being Subset of (TOP-REAL 2) for k being Element of NAT st Q = union { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } holds Q is closed let Q be Subset of (TOP-REAL 2); ::_thesis: for k being Element of NAT st Q = union { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } holds Q is closed let k be Element of NAT ; ::_thesis: ( Q = union { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } implies Q is closed ) reconsider F = { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } as Subset-Family of (TOP-REAL 2) by Lm3; now__::_thesis:_for_P_being_Subset_of_(TOP-REAL_2)_st_P_in_F_holds_ P_is_closed let P be Subset of (TOP-REAL 2); ::_thesis: ( P in F implies P is closed ) assume P in F ; ::_thesis: P is closed then ex i being Element of NAT st ( LSeg (f,i) = P & 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) ; hence P is closed ; ::_thesis: verum end; then A1: F is closed by TOPS_2:def_2; F is finite by Lm2; hence ( Q = union { (LSeg (f,i)) where i is Element of NAT : ( 1 <= i & i + 1 <= len f & i <> k & i <> k + 1 ) } implies Q is closed ) by A1, TOPS_2:21; ::_thesis: verum end; definition let IT be FinSequence of (TOP-REAL 2); attrIT is alternating means :Def4: :: SPPOL_1:def 4 for i being Element of NAT st 1 <= i & i + 2 <= len IT holds ( (IT /. i) `1 <> (IT /. (i + 2)) `1 & (IT /. i) `2 <> (IT /. (i + 2)) `2 ); end; :: deftheorem Def4 defines alternating SPPOL_1:def_4_:_ for IT being FinSequence of (TOP-REAL 2) holds ( IT is alternating iff for i being Element of NAT st 1 <= i & i + 2 <= len IT holds ( (IT /. i) `1 <> (IT /. (i + 2)) `1 & (IT /. i) `2 <> (IT /. (i + 2)) `2 ) ); theorem Th27: :: SPPOL_1:27 for i being Element of NAT for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & (f /. i) `1 = (f /. (i + 1)) `1 holds (f /. (i + 1)) `2 = (f /. (i + 2)) `2 proof let i be Element of NAT ; ::_thesis: for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & (f /. i) `1 = (f /. (i + 1)) `1 holds (f /. (i + 1)) `2 = (f /. (i + 2)) `2 let f be FinSequence of the carrier of (TOP-REAL 2); ::_thesis: ( f is special & f is alternating & 1 <= i & i + 2 <= len f & (f /. i) `1 = (f /. (i + 1)) `1 implies (f /. (i + 1)) `2 = (f /. (i + 2)) `2 ) assume that A1: f is special and A2: ( f is alternating & 1 <= i ) and A3: i + 2 <= len f ; ::_thesis: ( not (f /. i) `1 = (f /. (i + 1)) `1 or (f /. (i + 1)) `2 = (f /. (i + 2)) `2 ) set p2 = f /. (i + 1); set p3 = f /. (i + 2); ( 1 <= i + 1 & (i + 1) + 1 = i + (1 + 1) ) by NAT_1:11; then ( (f /. (i + 1)) `1 = (f /. (i + 2)) `1 or (f /. (i + 1)) `2 = (f /. (i + 2)) `2 ) by A1, A3, TOPREAL1:def_5; hence ( not (f /. i) `1 = (f /. (i + 1)) `1 or (f /. (i + 1)) `2 = (f /. (i + 2)) `2 ) by A2, A3, Def4; ::_thesis: verum end; theorem Th28: :: SPPOL_1:28 for i being Element of NAT for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & (f /. i) `2 = (f /. (i + 1)) `2 holds (f /. (i + 1)) `1 = (f /. (i + 2)) `1 proof let i be Element of NAT ; ::_thesis: for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & (f /. i) `2 = (f /. (i + 1)) `2 holds (f /. (i + 1)) `1 = (f /. (i + 2)) `1 let f be FinSequence of the carrier of (TOP-REAL 2); ::_thesis: ( f is special & f is alternating & 1 <= i & i + 2 <= len f & (f /. i) `2 = (f /. (i + 1)) `2 implies (f /. (i + 1)) `1 = (f /. (i + 2)) `1 ) assume that A1: f is special and A2: ( f is alternating & 1 <= i ) and A3: i + 2 <= len f ; ::_thesis: ( not (f /. i) `2 = (f /. (i + 1)) `2 or (f /. (i + 1)) `1 = (f /. (i + 2)) `1 ) set p2 = f /. (i + 1); set p3 = f /. (i + 2); ( 1 <= i + 1 & (i + 1) + 1 = i + (1 + 1) ) by NAT_1:11; then ( (f /. (i + 1)) `1 = (f /. (i + 2)) `1 or (f /. (i + 1)) `2 = (f /. (i + 2)) `2 ) by A1, A3, TOPREAL1:def_5; hence ( not (f /. i) `2 = (f /. (i + 1)) `2 or (f /. (i + 1)) `1 = (f /. (i + 2)) `1 ) by A2, A3, Def4; ::_thesis: verum end; theorem Th29: :: SPPOL_1:29 for i being Element of NAT for f being FinSequence of the carrier of (TOP-REAL 2) for p1, p2, p3 being Point of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 1) & p3 = f /. (i + 2) & not ( p1 `1 = p2 `1 & p3 `1 <> p2 `1 ) holds ( p1 `2 = p2 `2 & p3 `2 <> p2 `2 ) proof let i be Element of NAT ; ::_thesis: for f being FinSequence of the carrier of (TOP-REAL 2) for p1, p2, p3 being Point of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 1) & p3 = f /. (i + 2) & not ( p1 `1 = p2 `1 & p3 `1 <> p2 `1 ) holds ( p1 `2 = p2 `2 & p3 `2 <> p2 `2 ) let f be FinSequence of the carrier of (TOP-REAL 2); ::_thesis: for p1, p2, p3 being Point of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 1) & p3 = f /. (i + 2) & not ( p1 `1 = p2 `1 & p3 `1 <> p2 `1 ) holds ( p1 `2 = p2 `2 & p3 `2 <> p2 `2 ) let p1, p2, p3 be Point of (TOP-REAL 2); ::_thesis: ( f is special & f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 1) & p3 = f /. (i + 2) & not ( p1 `1 = p2 `1 & p3 `1 <> p2 `1 ) implies ( p1 `2 = p2 `2 & p3 `2 <> p2 `2 ) ) assume that A1: f is special and A2: f is alternating and A3: 1 <= i and A4: i + 2 <= len f and A5: p1 = f /. i and A6: p2 = f /. (i + 1) and A7: p3 = f /. (i + 2) ; ::_thesis: ( ( p1 `1 = p2 `1 & p3 `1 <> p2 `1 ) or ( p1 `2 = p2 `2 & p3 `2 <> p2 `2 ) ) i + 1 <= i + 2 by XREAL_1:6; then i + 1 <= len f by A4, XXREAL_0:2; then ( p1 `1 = p2 `1 or p1 `2 = p2 `2 ) by A1, A3, A5, A6, TOPREAL1:def_5; hence ( ( p1 `1 = p2 `1 & p3 `1 <> p2 `1 ) or ( p1 `2 = p2 `2 & p3 `2 <> p2 `2 ) ) by A2, A3, A4, A5, A7, Def4; ::_thesis: verum end; theorem :: SPPOL_1:30 for i being Element of NAT for f being FinSequence of the carrier of (TOP-REAL 2) for p1, p2, p3 being Point of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 1) & p3 = f /. (i + 2) & not ( p2 `1 = p3 `1 & p1 `1 <> p2 `1 ) holds ( p2 `2 = p3 `2 & p1 `2 <> p2 `2 ) proof let i be Element of NAT ; ::_thesis: for f being FinSequence of the carrier of (TOP-REAL 2) for p1, p2, p3 being Point of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 1) & p3 = f /. (i + 2) & not ( p2 `1 = p3 `1 & p1 `1 <> p2 `1 ) holds ( p2 `2 = p3 `2 & p1 `2 <> p2 `2 ) let f be FinSequence of the carrier of (TOP-REAL 2); ::_thesis: for p1, p2, p3 being Point of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 1) & p3 = f /. (i + 2) & not ( p2 `1 = p3 `1 & p1 `1 <> p2 `1 ) holds ( p2 `2 = p3 `2 & p1 `2 <> p2 `2 ) let p1, p2, p3 be Point of (TOP-REAL 2); ::_thesis: ( f is special & f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 1) & p3 = f /. (i + 2) & not ( p2 `1 = p3 `1 & p1 `1 <> p2 `1 ) implies ( p2 `2 = p3 `2 & p1 `2 <> p2 `2 ) ) assume that A1: f is special and A2: ( f is alternating & 1 <= i ) and A3: i + 2 <= len f and A4: p1 = f /. i and A5: p2 = f /. (i + 1) and A6: p3 = f /. (i + 2) ; ::_thesis: ( ( p2 `1 = p3 `1 & p1 `1 <> p2 `1 ) or ( p2 `2 = p3 `2 & p1 `2 <> p2 `2 ) ) ( 1 <= i + 1 & i + (1 + 1) = (i + 1) + 1 ) by NAT_1:11; then ( p2 `1 = p3 `1 or p2 `2 = p3 `2 ) by A1, A3, A5, A6, TOPREAL1:def_5; hence ( ( p2 `1 = p3 `1 & p1 `1 <> p2 `1 ) or ( p2 `2 = p3 `2 & p1 `2 <> p2 `2 ) ) by A2, A3, A4, A6, Def4; ::_thesis: verum end; Lm5: for f being FinSequence of the carrier of (TOP-REAL 2) for i being Element of NAT for p1, p2 being Point of (TOP-REAL 2) st f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 2) holds ex p being Point of (TOP-REAL 2) st ( p in LSeg (p1,p2) & p `1 <> p1 `1 & p `1 <> p2 `1 & p `2 <> p1 `2 & p `2 <> p2 `2 ) proof let f be FinSequence of the carrier of (TOP-REAL 2); ::_thesis: for i being Element of NAT for p1, p2 being Point of (TOP-REAL 2) st f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 2) holds ex p being Point of (TOP-REAL 2) st ( p in LSeg (p1,p2) & p `1 <> p1 `1 & p `1 <> p2 `1 & p `2 <> p1 `2 & p `2 <> p2 `2 ) let i be Element of NAT ; ::_thesis: for p1, p2 being Point of (TOP-REAL 2) st f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 2) holds ex p being Point of (TOP-REAL 2) st ( p in LSeg (p1,p2) & p `1 <> p1 `1 & p `1 <> p2 `1 & p `2 <> p1 `2 & p `2 <> p2 `2 ) let p1, p2 be Point of (TOP-REAL 2); ::_thesis: ( f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 2) implies ex p being Point of (TOP-REAL 2) st ( p in LSeg (p1,p2) & p `1 <> p1 `1 & p `1 <> p2 `1 & p `2 <> p1 `2 & p `2 <> p2 `2 ) ) assume ( f is alternating & 1 <= i & i + 2 <= len f & p1 = f /. i & p2 = f /. (i + 2) ) ; ::_thesis: ex p being Point of (TOP-REAL 2) st ( p in LSeg (p1,p2) & p `1 <> p1 `1 & p `1 <> p2 `1 & p `2 <> p1 `2 & p `2 <> p2 `2 ) then ( p1 `1 <> p2 `1 & p1 `2 <> p2 `2 ) by Def4; hence ex p being Point of (TOP-REAL 2) st ( p in LSeg (p1,p2) & p `1 <> p1 `1 & p `1 <> p2 `1 & p `2 <> p1 `2 & p `2 <> p2 `2 ) by Th14; ::_thesis: verum end; theorem :: SPPOL_1:31 for i being Element of NAT for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f holds not LSeg ((f /. i),(f /. (i + 2))) c= (LSeg (f,i)) \/ (LSeg (f,(i + 1))) proof let i be Element of NAT ; ::_thesis: for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f holds not LSeg ((f /. i),(f /. (i + 2))) c= (LSeg (f,i)) \/ (LSeg (f,(i + 1))) let f be FinSequence of the carrier of (TOP-REAL 2); ::_thesis: ( f is special & f is alternating & 1 <= i & i + 2 <= len f implies not LSeg ((f /. i),(f /. (i + 2))) c= (LSeg (f,i)) \/ (LSeg (f,(i + 1))) ) set p1 = f /. i; set p2 = f /. (i + 2); assume that A1: f is special and A2: f is alternating and A3: 1 <= i and A4: i + 2 <= len f ; ::_thesis: not LSeg ((f /. i),(f /. (i + 2))) c= (LSeg (f,i)) \/ (LSeg (f,(i + 1))) set p0 = f /. (i + 1); i + 1 <= i + 2 by XREAL_1:6; then i + 1 <= len f by A4, XXREAL_0:2; then A5: LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A3, TOPREAL1:def_3; ( 1 <= i + 1 & i + (1 + 1) = (i + 1) + 1 ) by NAT_1:11; then A6: LSeg (f,(i + 1)) = LSeg ((f /. (i + 1)),(f /. (i + 2))) by A4, TOPREAL1:def_3; consider p being Point of (TOP-REAL 2) such that A7: p in LSeg ((f /. i),(f /. (i + 2))) and A8: p `1 <> (f /. i) `1 and A9: p `1 <> (f /. (i + 2)) `1 and A10: p `2 <> (f /. i) `2 and A11: p `2 <> (f /. (i + 2)) `2 by A2, A3, A4, Lm5; assume A12: LSeg ((f /. i),(f /. (i + 2))) c= (LSeg (f,i)) \/ (LSeg (f,(i + 1))) ; ::_thesis: contradiction percases ( p in LSeg ((f /. i),(f /. (i + 1))) or p in LSeg ((f /. (i + 1)),(f /. (i + 2))) ) by A7, A5, A6, A12, XBOOLE_0:def_3; supposeA13: p in LSeg ((f /. i),(f /. (i + 1))) ; ::_thesis: contradiction A14: f /. i in LSeg ((f /. i),(f /. (i + 1))) by RLTOPSP1:68; ( LSeg ((f /. i),(f /. (i + 1))) is vertical or LSeg ((f /. i),(f /. (i + 1))) is horizontal ) by A1, A5, Th19; hence contradiction by A8, A10, A13, A14, Def2, Def3; ::_thesis: verum end; supposeA15: p in LSeg ((f /. (i + 1)),(f /. (i + 2))) ; ::_thesis: contradiction A16: f /. (i + 2) in LSeg ((f /. (i + 1)),(f /. (i + 2))) by RLTOPSP1:68; ( LSeg ((f /. (i + 1)),(f /. (i + 2))) is vertical or LSeg ((f /. (i + 1)),(f /. (i + 2))) is horizontal ) by A1, A6, Th19; hence contradiction by A9, A11, A15, A16, Def2, Def3; ::_thesis: verum end; end; end; theorem Th32: :: SPPOL_1:32 for i being Element of NAT for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & LSeg (f,i) is vertical holds LSeg (f,(i + 1)) is horizontal proof let i be Element of NAT ; ::_thesis: for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & LSeg (f,i) is vertical holds LSeg (f,(i + 1)) is horizontal let f be FinSequence of the carrier of (TOP-REAL 2); ::_thesis: ( f is special & f is alternating & 1 <= i & i + 2 <= len f & LSeg (f,i) is vertical implies LSeg (f,(i + 1)) is horizontal ) assume that A1: ( f is special & f is alternating ) and A2: 1 <= i and A3: i + 2 <= len f and A4: LSeg (f,i) is vertical ; ::_thesis: LSeg (f,(i + 1)) is horizontal i + 1 <= i + 2 by XREAL_1:6; then i + 1 <= len f by A3, XXREAL_0:2; then LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A2, TOPREAL1:def_3; then (f /. i) `1 = (f /. (i + 1)) `1 by A4, Th16; then (f /. (i + 1)) `2 = (f /. (i + 2)) `2 by A1, A2, A3, Th27; then A5: LSeg ((f /. (i + 1)),(f /. (i + 2))) is horizontal by Th15; ( 1 <= i + 1 & (i + 1) + 1 = i + (1 + 1) ) by NAT_1:11; hence LSeg (f,(i + 1)) is horizontal by A3, A5, TOPREAL1:def_3; ::_thesis: verum end; theorem Th33: :: SPPOL_1:33 for i being Element of NAT for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & LSeg (f,i) is horizontal holds LSeg (f,(i + 1)) is vertical proof let i be Element of NAT ; ::_thesis: for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & LSeg (f,i) is horizontal holds LSeg (f,(i + 1)) is vertical let f be FinSequence of the carrier of (TOP-REAL 2); ::_thesis: ( f is special & f is alternating & 1 <= i & i + 2 <= len f & LSeg (f,i) is horizontal implies LSeg (f,(i + 1)) is vertical ) assume that A1: ( f is special & f is alternating ) and A2: 1 <= i and A3: i + 2 <= len f and A4: LSeg (f,i) is horizontal ; ::_thesis: LSeg (f,(i + 1)) is vertical i + 1 <= i + 2 by XREAL_1:6; then i + 1 <= len f by A3, XXREAL_0:2; then LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A2, TOPREAL1:def_3; then (f /. i) `2 = (f /. (i + 1)) `2 by A4, Th15; then (f /. (i + 1)) `1 = (f /. (i + 2)) `1 by A1, A2, A3, Th28; then A5: LSeg ((f /. (i + 1)),(f /. (i + 2))) is vertical by Th16; ( 1 <= i + 1 & (i + 1) + 1 = i + (1 + 1) ) by NAT_1:11; hence LSeg (f,(i + 1)) is vertical by A3, A5, TOPREAL1:def_3; ::_thesis: verum end; theorem :: SPPOL_1:34 for i being Element of NAT for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & not ( LSeg (f,i) is vertical & LSeg (f,(i + 1)) is horizontal ) holds ( LSeg (f,i) is horizontal & LSeg (f,(i + 1)) is vertical ) proof let i be Element of NAT ; ::_thesis: for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & not ( LSeg (f,i) is vertical & LSeg (f,(i + 1)) is horizontal ) holds ( LSeg (f,i) is horizontal & LSeg (f,(i + 1)) is vertical ) let f be FinSequence of the carrier of (TOP-REAL 2); ::_thesis: ( f is special & f is alternating & 1 <= i & i + 2 <= len f & not ( LSeg (f,i) is vertical & LSeg (f,(i + 1)) is horizontal ) implies ( LSeg (f,i) is horizontal & LSeg (f,(i + 1)) is vertical ) ) assume A1: ( f is special & f is alternating & 1 <= i & i + 2 <= len f ) ; ::_thesis: ( ( LSeg (f,i) is vertical & LSeg (f,(i + 1)) is horizontal ) or ( LSeg (f,i) is horizontal & LSeg (f,(i + 1)) is vertical ) ) then ( LSeg (f,i) is vertical & not ( LSeg (f,i) is vertical & LSeg (f,(i + 1)) is horizontal ) implies ( LSeg (f,i) is horizontal & LSeg (f,(i + 1)) is vertical ) ) by Th32; hence ( ( LSeg (f,i) is vertical & LSeg (f,(i + 1)) is horizontal ) or ( LSeg (f,i) is horizontal & LSeg (f,(i + 1)) is vertical ) ) by A1, Th19, Th33; ::_thesis: verum end; theorem Th35: :: SPPOL_1:35 for i being Element of NAT for f being FinSequence of the carrier of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & f /. (i + 1) in LSeg (p,q) & LSeg (p,q) c= (LSeg (f,i)) \/ (LSeg (f,(i + 1))) & not f /. (i + 1) = p holds f /. (i + 1) = q proof let i be Element of NAT ; ::_thesis: for f being FinSequence of the carrier of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & f /. (i + 1) in LSeg (p,q) & LSeg (p,q) c= (LSeg (f,i)) \/ (LSeg (f,(i + 1))) & not f /. (i + 1) = p holds f /. (i + 1) = q let f be FinSequence of the carrier of (TOP-REAL 2); ::_thesis: for p, q being Point of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & f /. (i + 1) in LSeg (p,q) & LSeg (p,q) c= (LSeg (f,i)) \/ (LSeg (f,(i + 1))) & not f /. (i + 1) = p holds f /. (i + 1) = q let p, q be Point of (TOP-REAL 2); ::_thesis: ( f is special & f is alternating & 1 <= i & i + 2 <= len f & f /. (i + 1) in LSeg (p,q) & LSeg (p,q) c= (LSeg (f,i)) \/ (LSeg (f,(i + 1))) & not f /. (i + 1) = p implies f /. (i + 1) = q ) assume that A1: ( f is special & f is alternating ) and A2: 1 <= i and A3: i + 2 <= len f ; ::_thesis: ( not f /. (i + 1) in LSeg (p,q) or not LSeg (p,q) c= (LSeg (f,i)) \/ (LSeg (f,(i + 1))) or f /. (i + 1) = p or f /. (i + 1) = q ) i + 1 <= i + 2 by XREAL_1:6; then A4: i + 1 <= len f by A3, XXREAL_0:2; set p1 = f /. i; set p0 = f /. (i + 1); set p2 = f /. (i + 2); A5: ( i + (1 + 1) = (i + 1) + 1 & 1 <= i + 1 ) by NAT_1:11; assume that A6: f /. (i + 1) in LSeg (p,q) and A7: LSeg (p,q) c= (LSeg (f,i)) \/ (LSeg (f,(i + 1))) ; ::_thesis: ( f /. (i + 1) = p or f /. (i + 1) = q ) A8: ( p in LSeg (p,q) & q in LSeg (p,q) ) by RLTOPSP1:68; now__::_thesis:_(_(_p_in_LSeg_(f,i)_&_q_in_LSeg_(f,i)_&_(_f_/._(i_+_1)_=_p_or_f_/._(i_+_1)_=_q_)_)_or_(_p_in_LSeg_(f,i)_&_q_in_LSeg_(f,(i_+_1))_&_(_f_/._(i_+_1)_=_p_or_f_/._(i_+_1)_=_q_)_)_or_(_p_in_LSeg_(f,(i_+_1))_&_q_in_LSeg_(f,i)_&_(_f_/._(i_+_1)_=_p_or_f_/._(i_+_1)_=_q_)_)_or_(_p_in_LSeg_(f,(i_+_1))_&_q_in_LSeg_(f,(i_+_1))_&_(_f_/._(i_+_1)_=_p_or_f_/._(i_+_1)_=_q_)_)_) percases ( ( p in LSeg (f,i) & q in LSeg (f,i) ) or ( p in LSeg (f,i) & q in LSeg (f,(i + 1)) ) or ( p in LSeg (f,(i + 1)) & q in LSeg (f,i) ) or ( p in LSeg (f,(i + 1)) & q in LSeg (f,(i + 1)) ) ) by A7, A8, XBOOLE_0:def_3; case ( p in LSeg (f,i) & q in LSeg (f,i) ) ; ::_thesis: ( f /. (i + 1) = p or f /. (i + 1) = q ) then ( p in LSeg ((f /. i),(f /. (i + 1))) & q in LSeg ((f /. i),(f /. (i + 1))) ) by A2, A4, TOPREAL1:def_3; then A9: LSeg (p,q) c= LSeg ((f /. i),(f /. (i + 1))) by TOPREAL1:6; f /. (i + 1) is_extremal_in LSeg ((f /. i),(f /. (i + 1))) by Th11; hence ( f /. (i + 1) = p or f /. (i + 1) = q ) by A6, A9, Def1; ::_thesis: verum end; caseA10: ( p in LSeg (f,i) & q in LSeg (f,(i + 1)) ) ; ::_thesis: ( f /. (i + 1) = p or f /. (i + 1) = q ) then p in LSeg ((f /. i),(f /. (i + 1))) by A2, A4, TOPREAL1:def_3; then consider s being Real such that A11: p = ((1 - s) * (f /. i)) + (s * (f /. (i + 1))) and 0 <= s and s <= 1 ; A12: p `1 = (((1 - s) * (f /. i)) `1) + ((s * (f /. (i + 1))) `1) by A11, TOPREAL3:2 .= ((1 - s) * ((f /. i) `1)) + ((s * (f /. (i + 1))) `1) by TOPREAL3:4 .= ((1 - s) * ((f /. i) `1)) + (s * ((f /. (i + 1)) `1)) by TOPREAL3:4 ; q in LSeg ((f /. (i + 1)),(f /. (i + 2))) by A3, A5, A10, TOPREAL1:def_3; then consider s1 being Real such that A13: q = ((1 - s1) * (f /. (i + 1))) + (s1 * (f /. (i + 2))) and 0 <= s1 and s1 <= 1 ; A14: q `2 = (((1 - s1) * (f /. (i + 1))) `2) + ((s1 * (f /. (i + 2))) `2) by A13, TOPREAL3:2 .= ((1 - s1) * ((f /. (i + 1)) `2)) + ((s1 * (f /. (i + 2))) `2) by TOPREAL3:4 .= ((1 - s1) * ((f /. (i + 1)) `2)) + (s1 * ((f /. (i + 2)) `2)) by TOPREAL3:4 ; A15: p `2 = (((1 - s) * (f /. i)) `2) + ((s * (f /. (i + 1))) `2) by A11, TOPREAL3:2 .= ((1 - s) * ((f /. i) `2)) + ((s * (f /. (i + 1))) `2) by TOPREAL3:4 .= ((1 - s) * ((f /. i) `2)) + (s * ((f /. (i + 1)) `2)) by TOPREAL3:4 ; A16: q `1 = (((1 - s1) * (f /. (i + 1))) `1) + ((s1 * (f /. (i + 2))) `1) by A13, TOPREAL3:2 .= ((1 - s1) * ((f /. (i + 1)) `1)) + ((s1 * (f /. (i + 2))) `1) by TOPREAL3:4 .= ((1 - s1) * ((f /. (i + 1)) `1)) + (s1 * ((f /. (i + 2)) `1)) by TOPREAL3:4 ; now__::_thesis:_(_(_(f_/._i)_`1_=_(f_/._(i_+_1))_`1_&_(f_/._(i_+_2))_`1_<>_(f_/._(i_+_1))_`1_&_(_f_/._(i_+_1)_=_p_or_f_/._(i_+_1)_=_q_)_)_or_(_(f_/._i)_`2_=_(f_/._(i_+_1))_`2_&_(f_/._(i_+_2))_`2_<>_(f_/._(i_+_1))_`2_&_(_f_/._(i_+_1)_=_p_or_f_/._(i_+_1)_=_q_)_)_) A17: ( f /. (i + 2) = f /. (i + 2) & f /. i = f /. i ) ; percases ( ( (f /. i) `1 = (f /. (i + 1)) `1 & (f /. (i + 2)) `1 <> (f /. (i + 1)) `1 ) or ( (f /. i) `2 = (f /. (i + 1)) `2 & (f /. (i + 2)) `2 <> (f /. (i + 1)) `2 ) ) by A1, A2, A3, A17, Th29; caseA18: ( (f /. i) `1 = (f /. (i + 1)) `1 & (f /. (i + 2)) `1 <> (f /. (i + 1)) `1 ) ; ::_thesis: ( f /. (i + 1) = p or f /. (i + 1) = q ) consider r being Real such that A19: f /. (i + 1) = ((1 - r) * p) + (r * q) and 0 <= r and r <= 1 by A6; (f /. (i + 1)) `1 = (((1 - r) * p) `1) + ((r * q) `1) by A19, TOPREAL3:2 .= ((1 - r) * (p `1)) + ((r * q) `1) by TOPREAL3:4 .= ((1 - r) * ((f /. (i + 1)) `1)) + (r * (q `1)) by A12, A18, TOPREAL3:4 ; then r * (((f /. (i + 1)) `1) - (q `1)) = 0 ; then A20: ( r = 0 or ((f /. (i + 1)) `1) - (q `1) = 0 ) by XCMPLX_1:6; now__::_thesis:_(_(_r_=_0_&_(_f_/._(i_+_1)_=_p_or_f_/._(i_+_1)_=_q_)_)_or_(_(f_/._(i_+_1))_`1_=_q_`1_&_(_f_/._(i_+_1)_=_p_or_f_/._(i_+_1)_=_q_)_)_) percases ( r = 0 or (f /. (i + 1)) `1 = q `1 ) by A20; case r = 0 ; ::_thesis: ( f /. (i + 1) = p or f /. (i + 1) = q ) then f /. (i + 1) = ((1 - 0) * p) + (0. (TOP-REAL 2)) by A19, EUCLID:29 .= 1 * p by EUCLID:27 .= p by EUCLID:29 ; hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; ::_thesis: verum end; case (f /. (i + 1)) `1 = q `1 ; ::_thesis: ( f /. (i + 1) = p or f /. (i + 1) = q ) then s1 * (((f /. (i + 1)) `1) - ((f /. (i + 2)) `1)) = 0 by A16; then A21: ( s1 = 0 or ((f /. (i + 1)) `1) - ((f /. (i + 2)) `1) = 0 ) by XCMPLX_1:6; now__::_thesis:_(_(_s1_=_0_&_(_f_/._(i_+_1)_=_p_or_f_/._(i_+_1)_=_q_)_)_or_(_(f_/._(i_+_1))_`1_=_(f_/._(i_+_2))_`1_&_contradiction_)_) percases ( s1 = 0 or (f /. (i + 1)) `1 = (f /. (i + 2)) `1 ) by A21; case s1 = 0 ; ::_thesis: ( f /. (i + 1) = p or f /. (i + 1) = q ) then q = ((1 - 0) * (f /. (i + 1))) + (0. (TOP-REAL 2)) by A13, EUCLID:29 .= 1 * (f /. (i + 1)) by EUCLID:27 .= f /. (i + 1) by EUCLID:29 ; hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; ::_thesis: verum end; case (f /. (i + 1)) `1 = (f /. (i + 2)) `1 ; ::_thesis: contradiction hence contradiction by A18; ::_thesis: verum end; end; end; hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; ::_thesis: verum end; end; end; hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; ::_thesis: verum end; caseA22: ( (f /. i) `2 = (f /. (i + 1)) `2 & (f /. (i + 2)) `2 <> (f /. (i + 1)) `2 ) ; ::_thesis: ( f /. (i + 1) = p or f /. (i + 1) = q ) consider r being Real such that A23: f /. (i + 1) = ((1 - r) * p) + (r * q) and 0 <= r and r <= 1 by A6; (f /. (i + 1)) `2 = (((1 - r) * p) `2) + ((r * q) `2) by A23, TOPREAL3:2 .= ((1 - r) * (p `2)) + ((r * q) `2) by TOPREAL3:4 .= ((1 - r) * ((f /. (i + 1)) `2)) + (r * (q `2)) by A15, A22, TOPREAL3:4 ; then r * (((f /. (i + 1)) `2) - (q `2)) = 0 ; then A24: ( r = 0 or ((f /. (i + 1)) `2) - (q `2) = 0 ) by XCMPLX_1:6; now__::_thesis:_(_(_r_=_0_&_(_f_/._(i_+_1)_=_p_or_f_/._(i_+_1)_=_q_)_)_or_(_(f_/._(i_+_1))_`2_=_q_`2_&_(_f_/._(i_+_1)_=_p_or_f_/._(i_+_1)_=_q_)_)_) percases ( r = 0 or (f /. (i + 1)) `2 = q `2 ) by A24; case r = 0 ; ::_thesis: ( f /. (i + 1) = p or f /. (i + 1) = q ) then f /. (i + 1) = ((1 - 0) * p) + (0. (TOP-REAL 2)) by A23, EUCLID:29 .= 1 * p by EUCLID:27 .= p by EUCLID:29 ; hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; ::_thesis: verum end; case (f /. (i + 1)) `2 = q `2 ; ::_thesis: ( f /. (i + 1) = p or f /. (i + 1) = q ) then s1 * (((f /. (i + 1)) `2) - ((f /. (i + 2)) `2)) = 0 by A14; then A25: ( s1 = 0 or ((f /. (i + 1)) `2) - ((f /. (i + 2)) `2) = 0 ) by XCMPLX_1:6; now__::_thesis:_(_(_s1_=_0_&_(_f_/._(i_+_1)_=_p_or_f_/._(i_+_1)_=_q_)_)_or_(_(f_/._(i_+_1))_`2_=_(f_/._(i_+_2))_`2_&_contradiction_)_) percases ( s1 = 0 or (f /. (i + 1)) `2 = (f /. (i + 2)) `2 ) by A25; case s1 = 0 ; ::_thesis: ( f /. (i + 1) = p or f /. (i + 1) = q ) then q = ((1 - 0) * (f /. (i + 1))) + (0. (TOP-REAL 2)) by A13, EUCLID:29 .= 1 * (f /. (i + 1)) by EUCLID:27 .= f /. (i + 1) by EUCLID:29 ; hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; ::_thesis: verum end; case (f /. (i + 1)) `2 = (f /. (i + 2)) `2 ; ::_thesis: contradiction hence contradiction by A22; ::_thesis: verum end; end; end; hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; ::_thesis: verum end; end; end; hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; ::_thesis: verum end; end; end; hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; ::_thesis: verum end; caseA26: ( p in LSeg (f,(i + 1)) & q in LSeg (f,i) ) ; ::_thesis: ( f /. (i + 1) = p or f /. (i + 1) = q ) then q in LSeg ((f /. i),(f /. (i + 1))) by A2, A4, TOPREAL1:def_3; then consider s being Real such that A27: q = ((1 - s) * (f /. i)) + (s * (f /. (i + 1))) and 0 <= s and s <= 1 ; A28: q `1 = (((1 - s) * (f /. i)) `1) + ((s * (f /. (i + 1))) `1) by A27, TOPREAL3:2 .= ((1 - s) * ((f /. i) `1)) + ((s * (f /. (i + 1))) `1) by TOPREAL3:4 .= ((1 - s) * ((f /. i) `1)) + (s * ((f /. (i + 1)) `1)) by TOPREAL3:4 ; p in LSeg ((f /. (i + 1)),(f /. (i + 2))) by A3, A5, A26, TOPREAL1:def_3; then consider s1 being Real such that A29: p = ((1 - s1) * (f /. (i + 1))) + (s1 * (f /. (i + 2))) and 0 <= s1 and s1 <= 1 ; A30: p `2 = (((1 - s1) * (f /. (i + 1))) `2) + ((s1 * (f /. (i + 2))) `2) by A29, TOPREAL3:2 .= ((1 - s1) * ((f /. (i + 1)) `2)) + ((s1 * (f /. (i + 2))) `2) by TOPREAL3:4 .= ((1 - s1) * ((f /. (i + 1)) `2)) + (s1 * ((f /. (i + 2)) `2)) by TOPREAL3:4 ; A31: q `2 = (((1 - s) * (f /. i)) `2) + ((s * (f /. (i + 1))) `2) by A27, TOPREAL3:2 .= ((1 - s) * ((f /. i) `2)) + ((s * (f /. (i + 1))) `2) by TOPREAL3:4 .= ((1 - s) * ((f /. i) `2)) + (s * ((f /. (i + 1)) `2)) by TOPREAL3:4 ; A32: p `1 = (((1 - s1) * (f /. (i + 1))) `1) + ((s1 * (f /. (i + 2))) `1) by A29, TOPREAL3:2 .= ((1 - s1) * ((f /. (i + 1)) `1)) + ((s1 * (f /. (i + 2))) `1) by TOPREAL3:4 .= ((1 - s1) * ((f /. (i + 1)) `1)) + (s1 * ((f /. (i + 2)) `1)) by TOPREAL3:4 ; now__::_thesis:_(_(_(f_/._i)_`1_=_(f_/._(i_+_1))_`1_&_(f_/._(i_+_2))_`1_<>_(f_/._(i_+_1))_`1_&_(_f_/._(i_+_1)_=_p_or_f_/._(i_+_1)_=_q_)_)_or_(_(f_/._i)_`2_=_(f_/._(i_+_1))_`2_&_(f_/._(i_+_2))_`2_<>_(f_/._(i_+_1))_`2_&_(_f_/._(i_+_1)_=_p_or_f_/._(i_+_1)_=_q_)_)_) A33: ( f /. (i + 2) = f /. (i + 2) & f /. i = f /. i ) ; percases ( ( (f /. i) `1 = (f /. (i + 1)) `1 & (f /. (i + 2)) `1 <> (f /. (i + 1)) `1 ) or ( (f /. i) `2 = (f /. (i + 1)) `2 & (f /. (i + 2)) `2 <> (f /. (i + 1)) `2 ) ) by A1, A2, A3, A33, Th29; caseA34: ( (f /. i) `1 = (f /. (i + 1)) `1 & (f /. (i + 2)) `1 <> (f /. (i + 1)) `1 ) ; ::_thesis: ( f /. (i + 1) = p or f /. (i + 1) = q ) f /. (i + 1) in LSeg (q,p) by A6; then consider r being Real such that A35: f /. (i + 1) = ((1 - r) * q) + (r * p) and 0 <= r and r <= 1 ; (f /. (i + 1)) `1 = (((1 - r) * q) `1) + ((r * p) `1) by A35, TOPREAL3:2 .= ((1 - r) * (q `1)) + ((r * p) `1) by TOPREAL3:4 .= ((1 - r) * ((f /. (i + 1)) `1)) + (r * (p `1)) by A28, A34, TOPREAL3:4 ; then r * (((f /. (i + 1)) `1) - (p `1)) = 0 ; then A36: ( r = 0 or ((f /. (i + 1)) `1) - (p `1) = 0 ) by XCMPLX_1:6; now__::_thesis:_(_(_r_=_0_&_(_f_/._(i_+_1)_=_p_or_f_/._(i_+_1)_=_q_)_)_or_(_(f_/._(i_+_1))_`1_=_p_`1_&_(_f_/._(i_+_1)_=_p_or_f_/._(i_+_1)_=_q_)_)_) percases ( r = 0 or (f /. (i + 1)) `1 = p `1 ) by A36; case r = 0 ; ::_thesis: ( f /. (i + 1) = p or f /. (i + 1) = q ) then f /. (i + 1) = ((1 - 0) * q) + (0. (TOP-REAL 2)) by A35, EUCLID:29 .= 1 * q by EUCLID:27 .= q by EUCLID:29 ; hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; ::_thesis: verum end; case (f /. (i + 1)) `1 = p `1 ; ::_thesis: ( f /. (i + 1) = p or f /. (i + 1) = q ) then s1 * (((f /. (i + 1)) `1) - ((f /. (i + 2)) `1)) = 0 by A32; then A37: ( s1 = 0 or ((f /. (i + 1)) `1) - ((f /. (i + 2)) `1) = 0 ) by XCMPLX_1:6; now__::_thesis:_(_(_s1_=_0_&_(_f_/._(i_+_1)_=_p_or_f_/._(i_+_1)_=_q_)_)_or_(_(f_/._(i_+_1))_`1_=_(f_/._(i_+_2))_`1_&_contradiction_)_) percases ( s1 = 0 or (f /. (i + 1)) `1 = (f /. (i + 2)) `1 ) by A37; case s1 = 0 ; ::_thesis: ( f /. (i + 1) = p or f /. (i + 1) = q ) then p = ((1 - 0) * (f /. (i + 1))) + (0. (TOP-REAL 2)) by A29, EUCLID:29 .= 1 * (f /. (i + 1)) by EUCLID:27 .= f /. (i + 1) by EUCLID:29 ; hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; ::_thesis: verum end; case (f /. (i + 1)) `1 = (f /. (i + 2)) `1 ; ::_thesis: contradiction hence contradiction by A34; ::_thesis: verum end; end; end; hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; ::_thesis: verum end; end; end; hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; ::_thesis: verum end; caseA38: ( (f /. i) `2 = (f /. (i + 1)) `2 & (f /. (i + 2)) `2 <> (f /. (i + 1)) `2 ) ; ::_thesis: ( f /. (i + 1) = p or f /. (i + 1) = q ) f /. (i + 1) in LSeg (q,p) by A6; then consider r being Real such that A39: f /. (i + 1) = ((1 - r) * q) + (r * p) and 0 <= r and r <= 1 ; (f /. (i + 1)) `2 = (((1 - r) * q) `2) + ((r * p) `2) by A39, TOPREAL3:2 .= ((1 - r) * (q `2)) + ((r * p) `2) by TOPREAL3:4 .= ((1 - r) * ((f /. (i + 1)) `2)) + (r * (p `2)) by A31, A38, TOPREAL3:4 ; then r * (((f /. (i + 1)) `2) - (p `2)) = 0 ; then A40: ( r = 0 or ((f /. (i + 1)) `2) - (p `2) = 0 ) by XCMPLX_1:6; now__::_thesis:_(_(_r_=_0_&_(_f_/._(i_+_1)_=_p_or_f_/._(i_+_1)_=_q_)_)_or_(_(f_/._(i_+_1))_`2_=_p_`2_&_(_f_/._(i_+_1)_=_p_or_f_/._(i_+_1)_=_q_)_)_) percases ( r = 0 or (f /. (i + 1)) `2 = p `2 ) by A40; case r = 0 ; ::_thesis: ( f /. (i + 1) = p or f /. (i + 1) = q ) then f /. (i + 1) = ((1 - 0) * q) + (0. (TOP-REAL 2)) by A39, EUCLID:29 .= 1 * q by EUCLID:27 .= q by EUCLID:29 ; hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; ::_thesis: verum end; case (f /. (i + 1)) `2 = p `2 ; ::_thesis: ( f /. (i + 1) = p or f /. (i + 1) = q ) then s1 * (((f /. (i + 1)) `2) - ((f /. (i + 2)) `2)) = 0 by A30; then A41: ( s1 = 0 or ((f /. (i + 1)) `2) - ((f /. (i + 2)) `2) = 0 ) by XCMPLX_1:6; now__::_thesis:_(_(_s1_=_0_&_(_f_/._(i_+_1)_=_p_or_f_/._(i_+_1)_=_q_)_)_or_(_(f_/._(i_+_1))_`2_=_(f_/._(i_+_2))_`2_&_contradiction_)_) percases ( s1 = 0 or (f /. (i + 1)) `2 = (f /. (i + 2)) `2 ) by A41; case s1 = 0 ; ::_thesis: ( f /. (i + 1) = p or f /. (i + 1) = q ) then p = ((1 - 0) * (f /. (i + 1))) + (0. (TOP-REAL 2)) by A29, EUCLID:29 .= 1 * (f /. (i + 1)) by EUCLID:27 .= f /. (i + 1) by EUCLID:29 ; hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; ::_thesis: verum end; case (f /. (i + 1)) `2 = (f /. (i + 2)) `2 ; ::_thesis: contradiction hence contradiction by A38; ::_thesis: verum end; end; end; hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; ::_thesis: verum end; end; end; hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; ::_thesis: verum end; end; end; hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; ::_thesis: verum end; case ( p in LSeg (f,(i + 1)) & q in LSeg (f,(i + 1)) ) ; ::_thesis: ( f /. (i + 1) = p or f /. (i + 1) = q ) then ( p in LSeg ((f /. (i + 1)),(f /. (i + 2))) & q in LSeg ((f /. (i + 1)),(f /. (i + 2))) ) by A3, A5, TOPREAL1:def_3; then A42: LSeg (p,q) c= LSeg ((f /. (i + 1)),(f /. (i + 2))) by TOPREAL1:6; f /. (i + 1) is_extremal_in LSeg ((f /. (i + 1)),(f /. (i + 2))) by Th11; hence ( f /. (i + 1) = p or f /. (i + 1) = q ) by A6, A42, Def1; ::_thesis: verum end; end; end; hence ( f /. (i + 1) = p or f /. (i + 1) = q ) ; ::_thesis: verum end; theorem Th36: :: SPPOL_1:36 for i being Element of NAT for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f holds f /. (i + 1) is_extremal_in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) proof let i be Element of NAT ; ::_thesis: for f being FinSequence of the carrier of (TOP-REAL 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f holds f /. (i + 1) is_extremal_in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) let f be FinSequence of the carrier of (TOP-REAL 2); ::_thesis: ( f is special & f is alternating & 1 <= i & i + 2 <= len f implies f /. (i + 1) is_extremal_in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) ) assume that A1: ( f is special & f is alternating ) and A2: 1 <= i and A3: i + 2 <= len f ; ::_thesis: f /. (i + 1) is_extremal_in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) set p2 = f /. (i + 1); i + 1 <= i + 2 by XREAL_1:6; then i + 1 <= len f by A3, XXREAL_0:2; then LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A2, TOPREAL1:def_3; then f /. (i + 1) in LSeg (f,i) by RLTOPSP1:68; then A4: f /. (i + 1) in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) by XBOOLE_0:def_3; for p, q being Point of (TOP-REAL 2) st f /. (i + 1) in LSeg (p,q) & LSeg (p,q) c= (LSeg (f,i)) \/ (LSeg (f,(i + 1))) & not f /. (i + 1) = p holds f /. (i + 1) = q by A1, A2, A3, Th35; hence f /. (i + 1) is_extremal_in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) by A4, Def1; ::_thesis: verum end; theorem Th37: :: SPPOL_1:37 for i being Element of NAT for f being FinSequence of the carrier of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) for u being Point of (Euclid 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & u = f /. (i + 1) & f /. (i + 1) in LSeg (p,q) & f /. (i + 1) <> q & not p in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) holds for s being Real st s > 0 holds ex p3 being Point of (TOP-REAL 2) st ( not p3 in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) & p3 in LSeg (p,q) & p3 in Ball (u,s) ) proof let i be Element of NAT ; ::_thesis: for f being FinSequence of the carrier of (TOP-REAL 2) for p, q being Point of (TOP-REAL 2) for u being Point of (Euclid 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & u = f /. (i + 1) & f /. (i + 1) in LSeg (p,q) & f /. (i + 1) <> q & not p in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) holds for s being Real st s > 0 holds ex p3 being Point of (TOP-REAL 2) st ( not p3 in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) & p3 in LSeg (p,q) & p3 in Ball (u,s) ) let f be FinSequence of the carrier of (TOP-REAL 2); ::_thesis: for p, q being Point of (TOP-REAL 2) for u being Point of (Euclid 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & u = f /. (i + 1) & f /. (i + 1) in LSeg (p,q) & f /. (i + 1) <> q & not p in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) holds for s being Real st s > 0 holds ex p3 being Point of (TOP-REAL 2) st ( not p3 in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) & p3 in LSeg (p,q) & p3 in Ball (u,s) ) let p, q be Point of (TOP-REAL 2); ::_thesis: for u being Point of (Euclid 2) st f is special & f is alternating & 1 <= i & i + 2 <= len f & u = f /. (i + 1) & f /. (i + 1) in LSeg (p,q) & f /. (i + 1) <> q & not p in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) holds for s being Real st s > 0 holds ex p3 being Point of (TOP-REAL 2) st ( not p3 in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) & p3 in LSeg (p,q) & p3 in Ball (u,s) ) let u be Point of (Euclid 2); ::_thesis: ( f is special & f is alternating & 1 <= i & i + 2 <= len f & u = f /. (i + 1) & f /. (i + 1) in LSeg (p,q) & f /. (i + 1) <> q & not p in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) implies for s being Real st s > 0 holds ex p3 being Point of (TOP-REAL 2) st ( not p3 in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) & p3 in LSeg (p,q) & p3 in Ball (u,s) ) ) assume that A1: ( f is special & f is alternating ) and A2: 1 <= i and A3: i + 2 <= len f and A4: u = f /. (i + 1) and A5: f /. (i + 1) in LSeg (p,q) and A6: f /. (i + 1) <> q and A7: not p in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) ; ::_thesis: for s being Real st s > 0 holds ex p3 being Point of (TOP-REAL 2) st ( not p3 in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) & p3 in LSeg (p,q) & p3 in Ball (u,s) ) set p0 = f /. (i + 1); i + 1 <= i + 2 by XREAL_1:6; then i + 1 <= len f by A3, XXREAL_0:2; then LSeg (f,i) = LSeg ((f /. i),(f /. (i + 1))) by A2, TOPREAL1:def_3; then A8: f /. (i + 1) in LSeg (f,i) by RLTOPSP1:68; let s be Real; ::_thesis: ( s > 0 implies ex p3 being Point of (TOP-REAL 2) st ( not p3 in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) & p3 in LSeg (p,q) & p3 in Ball (u,s) ) ) assume A9: s > 0 ; ::_thesis: ex p3 being Point of (TOP-REAL 2) st ( not p3 in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) & p3 in LSeg (p,q) & p3 in Ball (u,s) ) percases ( p = q or p <> q ) ; suppose p = q ; ::_thesis: ex p3 being Point of (TOP-REAL 2) st ( not p3 in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) & p3 in LSeg (p,q) & p3 in Ball (u,s) ) then f /. (i + 1) in {p} by A5, RLTOPSP1:70; then p in LSeg (f,i) by A8, TARSKI:def_1; hence ex p3 being Point of (TOP-REAL 2) st ( not p3 in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) & p3 in LSeg (p,q) & p3 in Ball (u,s) ) by A7, XBOOLE_0:def_3; ::_thesis: verum end; supposeA10: p <> q ; ::_thesis: ex p3 being Point of (TOP-REAL 2) st ( not p3 in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) & p3 in LSeg (p,q) & p3 in Ball (u,s) ) reconsider v2 = q as Element of REAL 2 by EUCLID:22; reconsider v1 = p as Element of REAL 2 by EUCLID:22; A11: |.(v2 - v1).| > 0 by A10, EUCLID:17; reconsider r0 = s / 2 as Real ; consider s0 being Real such that A12: f /. (i + 1) = ((1 - s0) * p) + (s0 * q) and A13: 0 <= s0 and A14: s0 <= 1 by A5; set r3 = min ((s0 + (r0 / |.(v2 - v1).|)),1); set r4 = max ((s0 + ((- r0) / |.(v2 - v1).|)),0); set p4 = ((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q); set p3 = ((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q); A15: r0 > 0 by A9, XREAL_1:139; then A16: s0 <= s0 + (r0 / |.(v2 - v1).|) by A11, XREAL_1:29, XREAL_1:139; A17: r0 / |.(v2 - v1).| > 0 by A15, A11, XREAL_1:139; then A18: - (r0 / |.(v2 - v1).|) < - 0 by XREAL_1:24; then A19: (- r0) / |.(v2 - v1).| < 0 by XCMPLX_1:187; then A20: s0 + 0 > s0 + ((- r0) / |.(v2 - v1).|) by XREAL_1:6; then A21: s0 + ((- r0) / |.(v2 - v1).|) <= 1 by A14, XXREAL_0:2; then ( 0 <= max ((s0 + ((- r0) / |.(v2 - v1).|)),0) & max ((s0 + ((- r0) / |.(v2 - v1).|)),0) <= 1 ) by XXREAL_0:28, XXREAL_0:30; then A22: ((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q) in LSeg (p,q) ; A23: s0 < s0 + (r0 / |.(v2 - v1).|) by A15, A11, XREAL_1:29, XREAL_1:139; not LSeg ((((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)),(((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q))) c= (LSeg (f,i)) \/ (LSeg (f,(i + 1))) proof A24: f /. (i + 1) in LSeg ((((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)),(((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q))) proof s0 + ((- r0) / |.(v2 - v1).|) < s0 + (r0 / |.(v2 - v1).|) by A9, A19, XREAL_1:6; then A25: max ((s0 + ((- r0) / |.(v2 - v1).|)),0) < s0 + (r0 / |.(v2 - v1).|) by A17, A13, XXREAL_0:29; A26: max ((s0 + ((- r0) / |.(v2 - v1).|)),0) <= 1 by A21, XXREAL_0:28; percases ( max ((s0 + ((- r0) / |.(v2 - v1).|)),0) < 1 or max ((s0 + ((- r0) / |.(v2 - v1).|)),0) = 1 ) by A26, XXREAL_0:1; suppose max ((s0 + ((- r0) / |.(v2 - v1).|)),0) < 1 ; ::_thesis: f /. (i + 1) in LSeg ((((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)),(((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q))) then max ((s0 + ((- r0) / |.(v2 - v1).|)),0) < min ((s0 + (r0 / |.(v2 - v1).|)),1) by A25, XXREAL_0:21; then A27: (min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) > 0 by XREAL_1:50; set r5 = ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))); min ((s0 + (r0 / |.(v2 - v1).|)),1) >= s0 by A14, A16, XXREAL_0:20; then A28: (min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0 >= 0 by XREAL_1:48; max ((s0 + ((- r0) / |.(v2 - v1).|)),0) <= s0 by A13, A20, XXREAL_0:28; then (min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0 <= (min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) by XREAL_1:10; then ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) <= ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) by A27, XREAL_1:72; then A29: ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) <= 1 by A27, XCMPLX_1:60; A30: ((1 - (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))))) * (min ((s0 + (r0 / |.(v2 - v1).|)),1))) + ((((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) = (min ((s0 + (r0 / |.(v2 - v1).|)),1)) - ((((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) .= (min ((s0 + (r0 / |.(v2 - v1).|)),1)) - ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) by A27, XCMPLX_1:87 .= s0 ; ((1 - (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))))) * (((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q))) + ((((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * (((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q))) = (((1 - (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))))) * ((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p)) + ((1 - (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))))) * ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q))) + ((((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * (((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q))) by EUCLID:32 .= (((1 - (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))))) * ((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p)) + ((1 - (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))))) * ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q))) + (((((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * ((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p)) + ((((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q))) by EUCLID:32 .= ((((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * ((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p)) + ((((1 - (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))))) * ((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p)) + ((1 - (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))))) * ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q))) + ((((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q))) by EUCLID:26 ; then ((1 - (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))))) * (((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q))) + ((((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * (((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q))) = (((((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * ((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p)) + (((1 - (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))))) * ((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p)) + ((1 - (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))))) * ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)))) + ((((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q)) by EUCLID:26 .= ((((((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * ((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p)) + ((1 - (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))))) * ((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p))) + ((1 - (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))))) * ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q))) + ((((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q)) by EUCLID:26 .= (((((((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * (1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * p) + ((1 - (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))))) * ((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p))) + ((1 - (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))))) * ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q))) + ((((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q)) by EUCLID:30 ; then ((1 - (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))))) * (((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q))) + ((((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * (((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q))) = (((((((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * (1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * p) + (((1 - (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))))) * (1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1)))) * p)) + ((1 - (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))))) * ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q))) + ((((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q)) by EUCLID:30 .= (((((((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * (1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * p) + (((1 - (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))))) * (1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1)))) * p)) + (((1 - (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))))) * (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * q)) + ((((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q)) by EUCLID:30 ; then ((1 - (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))))) * (((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q))) + ((((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * (((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q))) = (((((((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * (1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * p) + (((1 - (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))))) * (1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1)))) * p)) + (((1 - (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))))) * (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * q)) + (((((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * q) by EUCLID:30; then ((1 - (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))))) * (((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q))) + ((((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * (((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q))) = (((((((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * (1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) + ((1 - (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))))) * (1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))))) * p) + (((1 - (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))))) * (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * q)) + (((((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * q) by EUCLID:33 .= ((((((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * (1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) + ((1 - (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))))) * (1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))))) * p) + ((((1 - (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))))) * (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * q) + (((((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) / ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * q)) by EUCLID:26 .= f /. (i + 1) by A12, A30, EUCLID:33 ; hence f /. (i + 1) in LSeg ((((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)),(((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q))) by A27, A28, A29; ::_thesis: verum end; suppose max ((s0 + ((- r0) / |.(v2 - v1).|)),0) = 1 ; ::_thesis: f /. (i + 1) in LSeg ((((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)),(((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q))) then ( s0 + ((- r0) / |.(v2 - v1).|) = 1 or 0 = 1 ) by XXREAL_0:16; then (s0 + ((- r0) / |.(v2 - v1).|)) - s0 >= s0 - s0 by A14, XREAL_1:9; hence f /. (i + 1) in LSeg ((((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)),(((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q))) by A18, XCMPLX_1:187; ::_thesis: verum end; end; end; A31: f /. (i + 1) is_extremal_in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) by A1, A2, A3, Th36; assume A32: LSeg ((((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)),(((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q))) c= (LSeg (f,i)) \/ (LSeg (f,(i + 1))) ; ::_thesis: contradiction percases ( f /. (i + 1) = ((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q) or f /. (i + 1) = ((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q) ) by A32, A24, A31, Def1; supposeA33: f /. (i + 1) = ((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q) ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( s0 = 1 or s0 <> 1 ) ; suppose s0 = 1 ; ::_thesis: contradiction then f /. (i + 1) = (0. (TOP-REAL 2)) + (1 * q) by A12, EUCLID:29 .= 1 * q by EUCLID:27 .= q by EUCLID:29 ; hence contradiction by A6; ::_thesis: verum end; supposeA34: s0 <> 1 ; ::_thesis: contradiction 0. (TOP-REAL 2) = (((1 - s0) * p) + (s0 * q)) - (((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)) by A12, A33, EUCLID:42 .= (((1 - s0) * p) + (s0 * q)) + ((- ((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p)) - ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)) by EUCLID:38 .= ((((1 - s0) * p) + (s0 * q)) + (- ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q))) + (- ((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p)) by EUCLID:26 .= (- ((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p)) + (((1 - s0) * p) + ((s0 * q) + (- ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)))) by EUCLID:26 .= ((- ((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p)) + ((1 - s0) * p)) + ((s0 * q) + (- ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q))) by EUCLID:26 .= (((- (1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1)))) * p) + ((1 - s0) * p)) + ((s0 * q) + (- ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q))) by EUCLID:40 .= (((- (1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1)))) + (1 - s0)) * p) + ((s0 * q) + (- ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q))) by EUCLID:33 .= (((- (1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1)))) + (1 - s0)) * p) + ((s0 * q) + ((- (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * q)) by EUCLID:40 .= (((- 1) * (s0 - (min ((s0 + (r0 / |.(v2 - v1).|)),1)))) * p) + ((s0 + (- (min ((s0 + (r0 / |.(v2 - v1).|)),1)))) * q) by EUCLID:33 .= ((- (s0 - (min ((s0 + (r0 / |.(v2 - v1).|)),1)))) * p) + ((s0 + (- (min ((s0 + (r0 / |.(v2 - v1).|)),1)))) * q) .= (- ((s0 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p)) + ((s0 + (- (min ((s0 + (r0 / |.(v2 - v1).|)),1)))) * q) by EUCLID:40 .= ((s0 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * q) - ((s0 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) ; then (s0 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * q = - (- ((s0 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p)) by EUCLID:37 .= (s0 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p ; then A35: s0 + (- (min ((s0 + (r0 / |.(v2 - v1).|)),1))) = 0 by A10, EUCLID:34; 1 > s0 by A14, A34, XXREAL_0:1; hence contradiction by A23, A35, XXREAL_0:21; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; supposeA36: f /. (i + 1) = ((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q) ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( s0 = 0 or s0 <> 0 ) ; suppose s0 = 0 ; ::_thesis: contradiction then f /. (i + 1) = (1 * p) + (0. (TOP-REAL 2)) by A12, EUCLID:29 .= 1 * p by EUCLID:27 .= p by EUCLID:29 ; hence contradiction by A7, A8, XBOOLE_0:def_3; ::_thesis: verum end; supposeA37: s0 <> 0 ; ::_thesis: contradiction 0. (TOP-REAL 2) = (((1 - s0) * p) + (s0 * q)) - (((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q)) by A12, A36, EUCLID:42 .= (((1 - s0) * p) + (s0 * q)) + ((- ((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p)) - ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q)) by EUCLID:38 .= ((((1 - s0) * p) + (s0 * q)) + (- ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q))) + (- ((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p)) by EUCLID:26 .= (- ((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p)) + (((1 - s0) * p) + ((s0 * q) + (- ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q)))) by EUCLID:26 .= ((- ((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p)) + ((1 - s0) * p)) + ((s0 * q) + (- ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q))) by EUCLID:26 .= (((- (1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * p) + ((1 - s0) * p)) + ((s0 * q) + (- ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q))) by EUCLID:40 .= (((- (1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) + (1 - s0)) * p) + ((s0 * q) + (- ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q))) by EUCLID:33 .= (((- (1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) + (1 - s0)) * p) + ((s0 * q) + ((- (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * q)) by EUCLID:40 .= (((- 1) * (s0 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * p) + ((s0 + (- (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * q) by EUCLID:33 .= ((- (s0 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)))) * p) + ((s0 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * q) .= (- ((s0 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p)) + ((s0 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * q) by EUCLID:40 .= (- ((s0 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p)) + ((s0 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * q) .= ((s0 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * q) + (- ((s0 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p)) .= ((s0 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * q) - ((s0 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) ; then (s0 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * q = - (- ((s0 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p)) by EUCLID:37 .= (s0 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p ; then s0 + (- (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) = 0 by A10, EUCLID:34; hence contradiction by A13, A20, A37, XXREAL_0:29; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; end; end; then A38: ex x being set st ( x in LSeg ((((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)),(((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q))) & not x in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) ) by TARSKI:def_3; reconsider u4 = ((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q) as Point of (Euclid 2) by EUCLID:22; A39: |.(v2 - v1).| <> 0 by A10, EUCLID:17; reconsider u3 = ((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q) as Point of (Euclid 2) by EUCLID:22; A40: min ((s0 + (r0 / |.(v2 - v1).|)),1) <= 1 by XXREAL_0:22; 0 <= min ((s0 + (r0 / |.(v2 - v1).|)),1) by A9, A13, XXREAL_0:20; then ((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q) in LSeg (p,q) by A40; then A41: LSeg ((((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)),(((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q))) c= LSeg (p,q) by A22, TOPREAL1:6; reconsider u0 = f /. (i + 1) as Point of (Euclid 2) by EUCLID:22; A42: (((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q)) - (f /. (i + 1)) = (((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q)) + ((- ((1 - s0) * p)) - (s0 * q)) by A12, EUCLID:38 .= ((((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q)) + (- ((1 - s0) * p))) + (- (s0 * q)) by EUCLID:26 .= (((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q) + (((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + (- ((1 - s0) * p)))) + (- (s0 * q)) by EUCLID:26 .= ((((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + (- ((1 - s0) * p))) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q)) + ((- s0) * q) by EUCLID:40 .= ((((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((- (1 - s0)) * p)) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q)) + ((- s0) * q) by EUCLID:40 .= (((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((- (1 - s0)) * p)) + (((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q) + ((- s0) * q)) by EUCLID:26 .= (((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((- (1 - s0)) * p)) + (((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) + (- s0)) * q) by EUCLID:33 .= (((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) + (- (1 - s0))) * p) + (((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) - s0) * q) by EUCLID:33 .= ((- ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) - s0)) * p) + (((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) - s0) * q) .= (((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) - s0) * q) - (((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) - s0) * p) by EUCLID:40 .= ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) - s0) * (q - p) by EUCLID:49 .= ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) - s0) * (v2 - v1) ; now__::_thesis:_dist_(u4,u0)_<_s percases ( s0 + ((- r0) / |.(v2 - v1).|) <= 0 or not s0 + ((- r0) / |.(v2 - v1).|) <= 0 ) ; suppose s0 + ((- r0) / |.(v2 - v1).|) <= 0 ; ::_thesis: dist (u4,u0) < s then A43: max ((s0 + ((- r0) / |.(v2 - v1).|)),0) = 0 by XXREAL_0:def_10; max ((s0 + ((- r0) / |.(v2 - v1).|)),0) >= s0 + ((- r0) / |.(v2 - v1).|) by XXREAL_0:25; then (max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) + (- s0) >= (s0 + ((- r0) / |.(v2 - v1).|)) + (- s0) by XREAL_1:6; then A44: - ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) - s0) <= - ((- r0) / |.(v2 - v1).|) by XREAL_1:24; r0 + r0 = s ; then A45: r0 < s by A9, XREAL_1:29; reconsider v3 = ((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q), v4 = f /. (i + 1) as Element of REAL 2 by EUCLID:22; A46: - ((- r0) / |.(v2 - v1).|) = (- (- r0)) / |.(v2 - v1).| by XCMPLX_1:187 .= r0 / |.(v2 - v1).| ; A47: dist (u4,u0) = |.(v3 - v4).| by Th5 .= |.((((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q)) - (f /. (i + 1))).| .= (abs ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) - s0)) * |.(v2 - v1).| by A42, EUCLID:11 ; abs ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) - s0) = abs (- ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) - s0)) by COMPLEX1:52 .= - (0 - s0) by A13, A43, ABSVALUE:def_1 ; then (abs ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) - s0)) * |.(v2 - v1).| <= (r0 / |.(v2 - v1).|) * |.(v2 - v1).| by A43, A44, A46, XREAL_1:64; then dist (u4,u0) <= r0 by A39, A47, XCMPLX_1:87; hence dist (u4,u0) < s by A45, XXREAL_0:2; ::_thesis: verum end; suppose not s0 + ((- r0) / |.(v2 - v1).|) <= 0 ; ::_thesis: dist (u4,u0) < s then A48: (((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q)) - (f /. (i + 1)) = ((s0 + ((- r0) / |.(v2 - v1).|)) - s0) * (v2 - v1) by A42, XXREAL_0:def_10 .= ((s0 + ((- r0) / |.(v2 - v1).|)) - s0) * (q - p) .= ((- r0) / |.(v2 - v1).|) * (q - p) .= ((- r0) / |.(v2 - v1).|) * (v2 - v1) ; reconsider v3 = ((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q), v4 = f /. (i + 1) as Element of REAL 2 by EUCLID:22; A49: r0 + r0 = s ; dist (u4,u0) = |.(v3 - v4).| by Th5 .= |.((((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q)) - (f /. (i + 1))).| .= (abs ((- r0) / |.(v2 - v1).|)) * |.(v2 - v1).| by A48, EUCLID:11 .= ((abs (- r0)) / (abs |.(v2 - v1).|)) * |.(v2 - v1).| by COMPLEX1:67 .= ((abs (- r0)) / |.(v2 - v1).|) * |.(v2 - v1).| by ABSVALUE:def_1 .= abs (- r0) by A11, XCMPLX_1:87 .= abs r0 by COMPLEX1:52 .= r0 by A9, ABSVALUE:def_1 ; hence dist (u4,u0) < s by A9, A49, XREAL_1:29; ::_thesis: verum end; end; end; then u4 in { u7 where u7 is Point of (Euclid 2) : dist (u0,u7) < s } ; then A50: ((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q) in Ball (u0,s) by METRIC_1:17; A51: (((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)) - (f /. (i + 1)) = (((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)) + ((- ((1 - s0) * p)) - (s0 * q)) by A12, EUCLID:38 .= ((((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)) + (- ((1 - s0) * p))) + (- (s0 * q)) by EUCLID:26 .= (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q) + (((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + (- ((1 - s0) * p)))) + (- (s0 * q)) by EUCLID:26 .= ((((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + (- ((1 - s0) * p))) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)) + ((- s0) * q) by EUCLID:40 .= ((((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((- (1 - s0)) * p)) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)) + ((- s0) * q) by EUCLID:40 .= (((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((- (1 - s0)) * p)) + (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q) + ((- s0) * q)) by EUCLID:26 .= (((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((- (1 - s0)) * p)) + (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) + (- s0)) * q) by EUCLID:33 .= (((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) + (- (1 - s0))) * p) + (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) * q) by EUCLID:33 .= ((- ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0)) * p) + (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) * q) .= (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) * q) - (((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) * p) by EUCLID:40 .= ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) * (q - p) by EUCLID:49 .= ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) * (v2 - v1) ; now__::_thesis:_dist_(u3,u0)_<_s percases ( 1 <= s0 + (r0 / |.(v2 - v1).|) or not 1 <= s0 + (r0 / |.(v2 - v1).|) ) ; supposeA52: 1 <= s0 + (r0 / |.(v2 - v1).|) ; ::_thesis: dist (u3,u0) < s min ((s0 + (r0 / |.(v2 - v1).|)),1) <= s0 + (r0 / |.(v2 - v1).|) by XXREAL_0:17; then A53: (min ((s0 + (r0 / |.(v2 - v1).|)),1)) + (- s0) <= (s0 + (r0 / |.(v2 - v1).|)) + (- s0) by XREAL_1:6; min ((s0 + (r0 / |.(v2 - v1).|)),1) = 1 by A52, XXREAL_0:def_9; then (min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0 >= 0 by A14, XREAL_1:48; then abs ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) <= r0 / |.(v2 - v1).| by A53, ABSVALUE:def_1; then A54: (abs ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0)) * |.(v2 - v1).| <= (r0 / |.(v2 - v1).|) * |.(v2 - v1).| by XREAL_1:64; reconsider v3 = ((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q), v4 = f /. (i + 1) as Element of REAL 2 by EUCLID:22; r0 + r0 = s ; then A55: r0 < s by A9, XREAL_1:29; dist (u3,u0) = |.(v3 - v4).| by Th5 .= |.((((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)) - (f /. (i + 1))).| .= |.(((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0) * (v2 - v1)).| by A51 .= (abs ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) - s0)) * |.(v2 - v1).| by EUCLID:11 ; then dist (u3,u0) <= r0 by A39, A54, XCMPLX_1:87; hence dist (u3,u0) < s by A55, XXREAL_0:2; ::_thesis: verum end; suppose not 1 <= s0 + (r0 / |.(v2 - v1).|) ; ::_thesis: dist (u3,u0) < s then A56: (((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)) - (f /. (i + 1)) = ((s0 + (r0 / |.(v2 - v1).|)) - s0) * (v2 - v1) by A51, XXREAL_0:def_9 .= ((s0 + (r0 / |.(v2 - v1).|)) - s0) * (q - p) .= (r0 / |.(v2 - v1).|) * (q - p) .= (r0 / |.(v2 - v1).|) * (v2 - v1) ; reconsider v3 = ((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q), v4 = f /. (i + 1) as Element of REAL 2 by EUCLID:22; A57: r0 + r0 = s ; dist (u3,u0) = |.(v3 - v4).| by Th5 .= |.((((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)) - (f /. (i + 1))).| .= (abs (r0 / |.(v2 - v1).|)) * |.(v2 - v1).| by A56, EUCLID:11 .= ((abs r0) / (abs |.(v2 - v1).|)) * |.(v2 - v1).| by COMPLEX1:67 .= ((abs r0) / |.(v2 - v1).|) * |.(v2 - v1).| by ABSVALUE:def_1 .= abs r0 by A11, XCMPLX_1:87 .= r0 by A9, ABSVALUE:def_1 ; hence dist (u3,u0) < s by A9, A57, XREAL_1:29; ::_thesis: verum end; end; end; then u3 in { u6 where u6 is Point of (Euclid 2) : dist (u0,u6) < s } ; then ((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q) in Ball (u0,s) by METRIC_1:17; then LSeg ((((1 - (min ((s0 + (r0 / |.(v2 - v1).|)),1))) * p) + ((min ((s0 + (r0 / |.(v2 - v1).|)),1)) * q)),(((1 - (max ((s0 + ((- r0) / |.(v2 - v1).|)),0))) * p) + ((max ((s0 + ((- r0) / |.(v2 - v1).|)),0)) * q))) c= Ball (u0,s) by A50, TOPREAL3:21; hence ex p3 being Point of (TOP-REAL 2) st ( not p3 in (LSeg (f,i)) \/ (LSeg (f,(i + 1))) & p3 in LSeg (p,q) & p3 in Ball (u,s) ) by A4, A38, A41; ::_thesis: verum end; end; end; definition let f1, f2 be FinSequence of the carrier of (TOP-REAL 2); let P be Subset of (TOP-REAL 2); predf1,f2 are_generators_of P means :Def5: :: SPPOL_1:def 5 ( f1 is alternating & f1 is being_S-Seq & f2 is alternating & f2 is being_S-Seq & f1 /. 1 = f2 /. 1 & f1 /. (len f1) = f2 /. (len f2) & <*(f1 /. 2),(f1 /. 1),(f2 /. 2)*> is alternating & <*(f1 /. ((len f1) - 1)),(f1 /. (len f1)),(f2 /. ((len f2) - 1))*> is alternating & f1 /. 1 <> f1 /. (len f1) & (L~ f1) /\ (L~ f2) = {(f1 /. 1),(f1 /. (len f1))} & P = (L~ f1) \/ (L~ f2) ); end; :: deftheorem Def5 defines are_generators_of SPPOL_1:def_5_:_ for f1, f2 being FinSequence of the carrier of (TOP-REAL 2) for P being Subset of (TOP-REAL 2) holds ( f1,f2 are_generators_of P iff ( f1 is alternating & f1 is being_S-Seq & f2 is alternating & f2 is being_S-Seq & f1 /. 1 = f2 /. 1 & f1 /. (len f1) = f2 /. (len f2) & <*(f1 /. 2),(f1 /. 1),(f2 /. 2)*> is alternating & <*(f1 /. ((len f1) - 1)),(f1 /. (len f1)),(f2 /. ((len f2) - 1))*> is alternating & f1 /. 1 <> f1 /. (len f1) & (L~ f1) /\ (L~ f2) = {(f1 /. 1),(f1 /. (len f1))} & P = (L~ f1) \/ (L~ f2) ) ); theorem :: SPPOL_1:38 for i being Element of NAT for P being Subset of (TOP-REAL 2) for f1, f2 being FinSequence of the carrier of (TOP-REAL 2) st f1,f2 are_generators_of P & 1 < i & i < len f1 holds f1 /. i is_extremal_in P proof let i be Element of NAT ; ::_thesis: for P being Subset of (TOP-REAL 2) for f1, f2 being FinSequence of the carrier of (TOP-REAL 2) st f1,f2 are_generators_of P & 1 < i & i < len f1 holds f1 /. i is_extremal_in P let P be Subset of (TOP-REAL 2); ::_thesis: for f1, f2 being FinSequence of the carrier of (TOP-REAL 2) st f1,f2 are_generators_of P & 1 < i & i < len f1 holds f1 /. i is_extremal_in P let f1, f2 be FinSequence of the carrier of (TOP-REAL 2); ::_thesis: ( f1,f2 are_generators_of P & 1 < i & i < len f1 implies f1 /. i is_extremal_in P ) set p0 = f1 /. i; set q1 = f1 /. 1; set q2 = f1 /. (len f1); set F1 = { (LSeg (f1,k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } ; set PP = union { (LSeg (f1,k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } ; reconsider u0 = f1 /. i as Point of (Euclid 2) by EUCLID:22; reconsider F2 = { (LSeg (f2,k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len f2 ) } as Subset-Family of (TOP-REAL 2) by Th25; assume that A1: f1,f2 are_generators_of P and A2: 1 < i and A3: i < len f1 ; ::_thesis: f1 /. i is_extremal_in P set P2 = union F2; A4: (L~ f1) /\ (L~ f2) = {(f1 /. 1),(f1 /. (len f1))} by A1, Def5; reconsider j = i - 1 as Element of NAT by A2, INT_1:3, XREAL_1:48; 1 + 1 <= i by A2, NAT_1:13; then A5: (1 + 1) - 1 <= j by XREAL_1:9; reconsider F = { (LSeg (f1,k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len f1 & k <> j & k <> j + 1 ) } as Subset-Family of (TOP-REAL 2) by Lm3; set P1 = union F; set Q = (union F) \/ (union F2); A6: j + 1 = i ; then LSeg (f1,j) = LSeg ((f1 /. j),(f1 /. i)) by A3, A5, TOPREAL1:def_3; then A7: f1 /. i in LSeg (f1,j) by RLTOPSP1:68; A8: P = (L~ f1) \/ (L~ f2) by A1, Def5; A9: f1 is being_S-Seq by A1, Def5; then A10: f1 is one-to-one by TOPREAL1:def_8; A11: len f1 >= 1 + 1 by A9, TOPREAL1:def_8; A12: i + 1 <= len f1 by A3, NAT_1:13; then A13: LSeg (f1,i) in { (LSeg (f1,k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } by A2; LSeg (f1,i) = LSeg ((f1 /. i),(f1 /. (i + 1))) by A2, A12, TOPREAL1:def_3; then A14: f1 /. i in LSeg (f1,i) by RLTOPSP1:68; then A15: f1 /. i in L~ f1 by A13, TARSKI:def_4; not f1 /. i in (union F) \/ (union F2) proof assume A16: f1 /. i in (union F) \/ (union F2) ; ::_thesis: contradiction percases ( f1 /. i in union F or f1 /. i in union F2 ) by A16, XBOOLE_0:def_3; supposeA17: f1 /. i in union F ; ::_thesis: contradiction A18: f1 is s.n.c. by A9, TOPREAL1:def_8; consider Z being set such that A19: f1 /. i in Z and A20: Z in F by A17, TARSKI:def_4; consider k being Element of NAT such that A21: LSeg (f1,k) = Z and 1 <= k and k + 1 <= len f1 and A22: k <> i - 1 and A23: k <> i by A20; ( k < j + 1 or i < k ) by A23, XXREAL_0:1; then ( k <= j or i < k ) by NAT_1:13; then A24: ( k < j or i < k ) by A22, XXREAL_0:1; now__::_thesis:_contradiction percases ( j - k > 0 or k - i > 0 ) by A24, XREAL_1:50; suppose j - k > 0 ; ::_thesis: contradiction then 1 + (j - k) > 1 + 0 by XREAL_1:6; then i - k > 1 ; then k + 1 < i by XREAL_1:20; then LSeg (f1,k) misses LSeg (f1,i) by A18, TOPREAL1:def_7; then (LSeg (f1,k)) /\ (LSeg (f1,i)) = {} by XBOOLE_0:def_7; hence contradiction by A14, A19, A21, XBOOLE_0:def_4; ::_thesis: verum end; suppose k - i > 0 ; ::_thesis: contradiction then (k - i) + 1 > 0 + 1 by XREAL_1:6; then k - j > 1 ; then j + 1 < k by XREAL_1:20; then LSeg (f1,j) misses LSeg (f1,k) by A18, TOPREAL1:def_7; then (LSeg (f1,j)) /\ (LSeg (f1,k)) = {} by XBOOLE_0:def_7; hence contradiction by A7, A19, A21, XBOOLE_0:def_4; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; supposeA25: f1 /. i in union F2 ; ::_thesis: contradiction 1 <= len f1 by A11, XXREAL_0:2; then 1 in Seg (len f1) by FINSEQ_1:1; then A26: 1 in dom f1 by FINSEQ_1:def_3; 1 <= len f1 by A2, A3, XXREAL_0:2; then A27: len f1 in dom f1 by FINSEQ_3:25; i in Seg (len f1) by A2, A3, FINSEQ_1:1; then A28: i in dom f1 by FINSEQ_1:def_3; f1 /. i in {(f1 /. 1),(f1 /. (len f1))} by A4, A15, A25, XBOOLE_0:def_4; then ( f1 /. i = f1 /. 1 or f1 /. i = f1 /. (len f1) ) by TARSKI:def_2; hence contradiction by A2, A3, A10, A26, A28, A27, PARTFUN2:10; ::_thesis: verum end; end; end; then A29: u0 in ((union F) \/ (union F2)) ` by SUBSET_1:29; A30: f1 is alternating by A1, Def5; A31: TopStruct(# the carrier of (TOP-REAL 2), the topology of (TOP-REAL 2) #) = TopSpaceMetr (Euclid 2) by EUCLID:def_8; then reconsider QQ = ((union F) \/ (union F2)) ` as Subset of (TopSpaceMetr (Euclid 2)) ; A32: f1 is special by A9, TOPREAL1:def_8; ( union F is closed & union F2 is closed ) by Lm4, Th26; then (union F) \/ (union F2) is closed by TOPS_1:9; then ((union F) \/ (union F2)) ` is open by TOPS_1:3; then QQ is open by A31, PRE_TOPC:30; then consider r0 being real number such that A33: r0 > 0 and A34: Ball (u0,r0) c= ((union F) \/ (union F2)) ` by A29, TOPMETR:15; reconsider r0 = r0 as Real by XREAL_0:def_1; A35: j + 2 <= len f1 by A12; now__::_thesis:_for_y_being_set_holds_ (_(_y_in_((union_F)_\/_(LSeg_(f1,j)))_\/_(LSeg_(f1,i))_implies_y_in_union__{__(LSeg_(f1,k))_where_k_is_Element_of_NAT_:_(_1_<=_k_&_k_+_1_<=_len_f1_)__}__)_&_(_y_in_union__{__(LSeg_(f1,k))_where_k_is_Element_of_NAT_:_(_1_<=_k_&_k_+_1_<=_len_f1_)__}__implies_y_in_((union_F)_\/_(LSeg_(f1,j)))_\/_(LSeg_(f1,i))_)_) let y be set ; ::_thesis: ( ( y in ((union F) \/ (LSeg (f1,j))) \/ (LSeg (f1,i)) implies y in union { (LSeg (f1,k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } ) & ( y in union { (LSeg (f1,k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } implies b1 in ((union F) \/ (LSeg (f1,j))) \/ (LSeg (f1,i)) ) ) hereby ::_thesis: ( y in union { (LSeg (f1,k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } implies b1 in ((union F) \/ (LSeg (f1,j))) \/ (LSeg (f1,i)) ) assume y in ((union F) \/ (LSeg (f1,j))) \/ (LSeg (f1,i)) ; ::_thesis: y in union { (LSeg (f1,k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } then A36: ( y in (union F) \/ (LSeg (f1,j)) or y in LSeg (f1,i) ) by XBOOLE_0:def_3; percases ( y in union F or y in LSeg (f1,j) or y in LSeg (f1,i) ) by A36, XBOOLE_0:def_3; suppose y in union F ; ::_thesis: y in union { (LSeg (f1,k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } then consider Z3 being set such that A37: y in Z3 and A38: Z3 in F by TARSKI:def_4; ex k being Element of NAT st ( LSeg (f1,k) = Z3 & 1 <= k & k + 1 <= len f1 & not k = i - 1 & not k = i ) by A38; then Z3 in { (LSeg (f1,k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } ; hence y in union { (LSeg (f1,k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } by A37, TARSKI:def_4; ::_thesis: verum end; supposeA39: y in LSeg (f1,j) ; ::_thesis: y in union { (LSeg (f1,k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } LSeg (f1,j) in { (LSeg (f1,k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } by A3, A6, A5; hence y in union { (LSeg (f1,k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } by A39, TARSKI:def_4; ::_thesis: verum end; suppose y in LSeg (f1,i) ; ::_thesis: y in union { (LSeg (f1,k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } hence y in union { (LSeg (f1,k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } by A13, TARSKI:def_4; ::_thesis: verum end; end; end; assume y in union { (LSeg (f1,k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } ; ::_thesis: b1 in ((union F) \/ (LSeg (f1,j))) \/ (LSeg (f1,i)) then consider Z2 being set such that A40: y in Z2 and A41: Z2 in { (LSeg (f1,k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } by TARSKI:def_4; consider k being Element of NAT such that A42: LSeg (f1,k) = Z2 and A43: ( 1 <= k & k + 1 <= len f1 ) by A41; percases ( k = i - 1 or k = i or ( k <> i - 1 & k <> i ) ) ; supposeA44: ( k = i - 1 or k = i ) ; ::_thesis: b1 in ((union F) \/ (LSeg (f1,j))) \/ (LSeg (f1,i)) now__::_thesis:_y_in_((union_F)_\/_(LSeg_(f1,j)))_\/_(LSeg_(f1,i)) percases ( k = i - 1 or k = i ) by A44; suppose k = i - 1 ; ::_thesis: y in ((union F) \/ (LSeg (f1,j))) \/ (LSeg (f1,i)) then y in (LSeg (f1,j)) \/ (LSeg (f1,i)) by A40, A42, XBOOLE_0:def_3; then y in (union F) \/ ((LSeg (f1,j)) \/ (LSeg (f1,i))) by XBOOLE_0:def_3; hence y in ((union F) \/ (LSeg (f1,j))) \/ (LSeg (f1,i)) by XBOOLE_1:4; ::_thesis: verum end; suppose k = i ; ::_thesis: y in ((union F) \/ (LSeg (f1,j))) \/ (LSeg (f1,i)) hence y in ((union F) \/ (LSeg (f1,j))) \/ (LSeg (f1,i)) by A40, A42, XBOOLE_0:def_3; ::_thesis: verum end; end; end; hence y in ((union F) \/ (LSeg (f1,j))) \/ (LSeg (f1,i)) ; ::_thesis: verum end; suppose ( k <> i - 1 & k <> i ) ; ::_thesis: b1 in ((union F) \/ (LSeg (f1,j))) \/ (LSeg (f1,i)) then Z2 in F by A42, A43; then y in union F by A40, TARSKI:def_4; then y in (union F) \/ ((LSeg (f1,j)) \/ (LSeg (f1,i))) by XBOOLE_0:def_3; hence y in ((union F) \/ (LSeg (f1,j))) \/ (LSeg (f1,i)) by XBOOLE_1:4; ::_thesis: verum end; end; end; then A45: ((union F) \/ (LSeg (f1,j))) \/ (LSeg (f1,i)) = union { (LSeg (f1,k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } by TARSKI:1; A46: now__::_thesis:_for_p,_q_being_Point_of_(TOP-REAL_2)_st_f1_/._i_in_LSeg_(p,q)_&_LSeg_(p,q)_c=_P_&_not_f1_/._i_=_p_holds_ f1_/._i_=_q let p, q be Point of (TOP-REAL 2); ::_thesis: ( f1 /. i in LSeg (p,q) & LSeg (p,q) c= P & not f1 /. i = b1 implies f1 /. i = b2 ) assume that A47: f1 /. i in LSeg (p,q) and A48: LSeg (p,q) c= P ; ::_thesis: ( f1 /. i = b1 or f1 /. i = b2 ) percases ( LSeg (p,q) c= (LSeg (f1,j)) \/ (LSeg (f1,i)) or not LSeg (p,q) c= (LSeg (f1,j)) \/ (LSeg (f1,i)) ) ; supposeA49: LSeg (p,q) c= (LSeg (f1,j)) \/ (LSeg (f1,i)) ; ::_thesis: ( f1 /. i = b1 or f1 /. i = b2 ) f1 /. i is_extremal_in (LSeg (f1,j)) \/ (LSeg (f1,i)) by A30, A6, A5, A35, A32, Th36; hence ( f1 /. i = p or f1 /. i = q ) by A47, A49, Def1; ::_thesis: verum end; suppose not LSeg (p,q) c= (LSeg (f1,j)) \/ (LSeg (f1,i)) ; ::_thesis: ( f1 /. i = b1 or f1 /. i = b2 ) then consider x being set such that A50: x in LSeg (p,q) and A51: not x in (LSeg (f1,j)) \/ (LSeg (f1,i)) by TARSKI:def_3; reconsider p8 = x as Point of (TOP-REAL 2) by A50; A52: LSeg (p,q) = (LSeg (p,p8)) \/ (LSeg (p8,q)) by A50, TOPREAL1:5; now__::_thesis:_(_f1_/._i_=_p_or_f1_/._i_=_q_) percases ( f1 /. i in LSeg (p,p8) or f1 /. i in LSeg (p8,q) ) by A47, A52, XBOOLE_0:def_3; supposeA53: f1 /. i in LSeg (p,p8) ; ::_thesis: ( f1 /. i = p or f1 /. i = q ) now__::_thesis:_not_f1_/._i_<>_p assume f1 /. i <> p ; ::_thesis: contradiction then consider q3 being Point of (TOP-REAL 2) such that A54: not q3 in (LSeg (f1,j)) \/ (LSeg (f1,i)) and A55: q3 in LSeg (p8,p) and A56: q3 in Ball (u0,r0) by A30, A5, A35, A32, A33, A34, A51, A53, Th37; A57: not q3 in (union F) \/ (union F2) by A34, A56, XBOOLE_0:def_5; then not q3 in union F by XBOOLE_0:def_3; then not q3 in (union F) \/ ((LSeg (f1,j)) \/ (LSeg (f1,i))) by A54, XBOOLE_0:def_3; then A58: not q3 in union { (LSeg (f1,k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } by A45, XBOOLE_1:4; LSeg (p8,p) c= LSeg (p,q) by A52, XBOOLE_1:7; then A59: LSeg (p8,p) c= P by A48, XBOOLE_1:1; not q3 in L~ f2 by A57, XBOOLE_0:def_3; hence contradiction by A8, A55, A58, A59, XBOOLE_0:def_3; ::_thesis: verum end; hence ( f1 /. i = p or f1 /. i = q ) ; ::_thesis: verum end; supposeA60: f1 /. i in LSeg (p8,q) ; ::_thesis: ( f1 /. i = p or f1 /. i = q ) now__::_thesis:_not_f1_/._i_<>_q assume f1 /. i <> q ; ::_thesis: contradiction then consider q3 being Point of (TOP-REAL 2) such that A61: not q3 in (LSeg (f1,j)) \/ (LSeg (f1,i)) and A62: q3 in LSeg (p8,q) and A63: q3 in Ball (u0,r0) by A30, A5, A35, A32, A33, A34, A51, A60, Th37; A64: not q3 in (union F) \/ (union F2) by A34, A63, XBOOLE_0:def_5; then not q3 in union F by XBOOLE_0:def_3; then not q3 in (union F) \/ ((LSeg (f1,j)) \/ (LSeg (f1,i))) by A61, XBOOLE_0:def_3; then A65: not q3 in union { (LSeg (f1,k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } by A45, XBOOLE_1:4; LSeg (p8,q) c= LSeg (p,q) by A52, XBOOLE_1:7; then A66: LSeg (p8,q) c= P by A48, XBOOLE_1:1; not q3 in L~ f2 by A64, XBOOLE_0:def_3; hence contradiction by A8, A62, A65, A66, XBOOLE_0:def_3; ::_thesis: verum end; hence ( f1 /. i = p or f1 /. i = q ) ; ::_thesis: verum end; end; end; hence ( f1 /. i = p or f1 /. i = q ) ; ::_thesis: verum end; end; end; f1 /. i in union { (LSeg (f1,k)) where k is Element of NAT : ( 1 <= k & k + 1 <= len f1 ) } by A14, A13, TARSKI:def_4; then f1 /. i in P by A8, XBOOLE_0:def_3; hence f1 /. i is_extremal_in P by A46, Def1; ::_thesis: verum end; theorem :: SPPOL_1:39 for n being Element of NAT for p, q being Point of (TOP-REAL n) for p9, q9 being Point of (Euclid n) st p = p9 & q = q9 holds dist (p9,q9) = |.(p - q).| by Th5; theorem :: SPPOL_1:40 for p, q, r being Point of (TOP-REAL 2) st LSeg (p,q) is horizontal & r in LSeg (p,q) holds p `2 = r `2 proof let p, q, r be Point of (TOP-REAL 2); ::_thesis: ( LSeg (p,q) is horizontal & r in LSeg (p,q) implies p `2 = r `2 ) assume LSeg (p,q) is horizontal ; ::_thesis: ( not r in LSeg (p,q) or p `2 = r `2 ) then A1: p `2 = q `2 by Th15; assume r in LSeg (p,q) ; ::_thesis: p `2 = r `2 then consider t being Real such that A2: r = ((1 - t) * p) + (t * q) and 0 <= t and t <= 1 ; thus p `2 = ((1 - t) * (p `2)) + (t * (p `2)) .= (((1 - t) * p) `2) + (t * (q `2)) by A1, TOPREAL3:4 .= (((1 - t) * p) `2) + ((t * q) `2) by TOPREAL3:4 .= r `2 by A2, TOPREAL3:2 ; ::_thesis: verum end; theorem :: SPPOL_1:41 for p, q, r being Point of (TOP-REAL 2) st LSeg (p,q) is vertical & r in LSeg (p,q) holds p `1 = r `1 proof let p, q, r be Point of (TOP-REAL 2); ::_thesis: ( LSeg (p,q) is vertical & r in LSeg (p,q) implies p `1 = r `1 ) assume LSeg (p,q) is vertical ; ::_thesis: ( not r in LSeg (p,q) or p `1 = r `1 ) then A1: p `1 = q `1 by Th16; assume r in LSeg (p,q) ; ::_thesis: p `1 = r `1 then consider t being Real such that A2: r = ((1 - t) * p) + (t * q) and 0 <= t and t <= 1 ; thus p `1 = ((1 - t) * (p `1)) + (t * (p `1)) .= (((1 - t) * p) `1) + (t * (q `1)) by A1, TOPREAL3:4 .= (((1 - t) * p) `1) + ((t * q) `1) by TOPREAL3:4 .= r `1 by A2, TOPREAL3:2 ; ::_thesis: verum end; registration cluster non empty functional compact horizontal for Element of bool the carrier of (TOP-REAL 2); existence ex b1 being Subset of (TOP-REAL 2) st ( b1 is compact & not b1 is empty & b1 is horizontal ) proof take LSeg (|[0,0]|,|[1,0]|) ; ::_thesis: ( LSeg (|[0,0]|,|[1,0]|) is compact & not LSeg (|[0,0]|,|[1,0]|) is empty & LSeg (|[0,0]|,|[1,0]|) is horizontal ) ( |[0,0]| `2 = 0 & |[1,0]| `2 = 0 ) by EUCLID:52; hence ( LSeg (|[0,0]|,|[1,0]|) is compact & not LSeg (|[0,0]|,|[1,0]|) is empty & LSeg (|[0,0]|,|[1,0]|) is horizontal ) by Th15; ::_thesis: verum end; cluster non empty functional compact vertical for Element of bool the carrier of (TOP-REAL 2); existence ex b1 being Subset of (TOP-REAL 2) st ( b1 is compact & not b1 is empty & b1 is vertical ) proof take LSeg (|[0,0]|,|[0,1]|) ; ::_thesis: ( LSeg (|[0,0]|,|[0,1]|) is compact & not LSeg (|[0,0]|,|[0,1]|) is empty & LSeg (|[0,0]|,|[0,1]|) is vertical ) ( |[0,0]| `1 = 0 & |[0,1]| `1 = 0 ) by EUCLID:52; hence ( LSeg (|[0,0]|,|[0,1]|) is compact & not LSeg (|[0,0]|,|[0,1]|) is empty & LSeg (|[0,0]|,|[0,1]|) is vertical ) by Th16; ::_thesis: verum end; end;