sppol_1.miz



    begin

    reserve n,i,k,m for Nat;

    theorem :: SPPOL_1:1

    for n,k be Nat holds n < k implies n <= (k - 1)

    proof

      let n,k be Nat;

      assume n < k;

      then (n + 1) <= k by NAT_1: 13;

      then ((n + 1) - 1) <= (k - 1) by XREAL_1: 9;

      hence thesis;

    end;

    theorem :: SPPOL_1:2

    1 <= (k - m) & (k - m) <= n implies (k - m) in ( Seg n) & (k - m) is Element of NAT

    proof

      assume that

       A1: 1 <= (k - m) and

       A2: (k - m) <= n;

      (k - m) is Element of NAT by A1, INT_1: 3;

      hence thesis by A1, A2, FINSEQ_1: 1;

    end;

    scheme :: SPPOL_1:sch1

    FinSeqFam { D() -> non empty set , f() -> FinSequence of D() , F( FinSequence of D(), Nat) -> set , P[ Nat] } :

{ F(f,i) : i in ( dom f()) & P[i] } is finite;

      deffunc U( Nat) = F(f,$1);

      set F = { U(i) : i in ( dom f()) & P[i] }, F9 = { U(i) where i be Element of NAT : i in ( dom f()) };

      

       A1: F c= F9

      proof

        let x be object;

        assume x in F;

        then ex i be Nat st x = F(f,i) & i in ( dom f()) & P[i];

        hence thesis;

      end;

      

       A2: ( dom f()) is finite;

      F9 is finite from FRAENKEL:sch 21( A2);

      hence thesis by A1;

    end;

    scheme :: SPPOL_1:sch2

    FinSeqFam9 { D() -> non empty set , f() -> FinSequence of D() , F( FinSequence of D(), Nat) -> set , P[ set] } :

{ F(f,i) : 1 <= i & i <= ( len f()) & P[i] } is finite;

      deffunc U( Nat) = F(f,$1);

      set F = { U(i) : 1 <= i & i <= ( len f()) & P[i] }, F9 = { U(i) where i be Element of NAT : i in ( dom f()) };

      

       A1: F c= F9

      proof

        let x be object;

        assume x in F;

        then

        consider i be Nat such that

         A2: x = F(f,i) and

         A3: 1 <= i & i <= ( len f()) and P[i];

        i in ( dom f()) by A3, FINSEQ_3: 25;

        hence thesis by A2;

      end;

      

       A4: ( dom f()) is finite;

      F9 is finite from FRAENKEL:sch 21( A4);

      hence thesis by A1;

    end;

    theorem :: SPPOL_1:3

    

     Th3: for x1,x2,x3 be Element of ( REAL n) holds ( |.(x1 - x2).| - |.(x2 - x3).|) <= |.(x1 - x3).|

    proof

      let x1,x2,x3 be Element of ( REAL n);

       |.(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 thesis;

    end;

    theorem :: SPPOL_1:4

    for x1,x2,x3 be Element of ( REAL n) holds ( |.(x2 - x1).| - |.(x2 - x3).|) <= |.(x3 - x1).|

    proof

      let x1,x2,x3 be Element of ( REAL n);

       |.(x2 - x1).| = |.(x1 - x2).| by EUCLID: 18;

      then ( |.(x2 - x1).| - |.(x2 - x3).|) <= |.(x1 - x3).| by Th3;

      hence thesis by EUCLID: 18;

    end;

    begin

    reserve r,r1,r2,s,s1,s2 for Real;

    reserve p,p1,p2,q1,q2 for Point of ( TOP-REAL n);

    theorem :: SPPOL_1:5

    

     Th5: for u1,u2 be Point of ( Euclid n), v1,v2 be Element of ( REAL n) st v1 = u1 & v2 = u2 holds ( dist (u1,u2)) = |.(v1 - v2).|

    proof

      let u1,u2 be Point of ( Euclid n), v1,v2 be Element of ( REAL n);

      assume v1 = u1 & v2 = u2;

      

      hence ( dist (u1,u2)) = (( Pitag_dist n) . (v1,v2)) by METRIC_1:def 1

      .= |.(v1 - v2).| by EUCLID:def 6;

    end;

    theorem :: SPPOL_1:6

    for P be non empty Subset of ( TOP-REAL n) st P is closed & P c= ( LSeg (p1,p2)) holds ex s st (((1 - s) * p1) + (s * p2)) in P & for r st 0 <= r & r <= 1 & (((1 - r) * p1) + (r * p2)) in P holds s <= r

    proof

      let P be non empty Subset of ( TOP-REAL n);

      set W = { r : 0 <= r & r <= 1 & (((1 - r) * p1) + (r * p2)) in P };

      W c= REAL

      proof

        let x be object;

        assume x in W;

        then ex r st r = x & 0 <= r & r <= 1 & (((1 - r) * p1) + (r * p2)) in P;

        hence thesis by XREAL_0:def 1;

      end;

      then

      reconsider W as Subset of REAL ;

      assume that

       A1: P is closed and

       A2: P c= ( LSeg (p1,p2));

      take r2 = ( lower_bound W);

      

       A3: W is bounded_below

      proof

        take 0 ;

        let r be ExtReal;

        assume r in W;

        then ex s st s = r & 0 <= s & s <= 1 & (((1 - s) * p1) + (s * p2)) in P;

        hence thesis;

      end;

      hereby

        set p = (((1 - r2) * p1) + (r2 * p2));

        reconsider u = p as Point of ( Euclid n) by EUCLID: 22;

        

         A4: the TopStruct 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 be Real st r0 in W

        proof

          consider v be 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 such that

           A8: v = (((1 - s) * p1) + (s * p2)) & 0 <= s & s <= 1;

          s in { r : 0 <= r & r <= 1 & (((1 - r) * p1) + (r * p2)) in P } by A7, A8;

          hence thesis;

        end;

        assume

         A9: not p in P;

        then p in (the carrier of ( TOP-REAL n) \ P) by XBOOLE_0:def 5;

        then

        consider r0 be Real such that

         A10: r0 > 0 and

         A11: ( Ball (u,r0)) c= Q by A5, TOPMETR: 15;

        per cases ;

          suppose

           A12: p1 <> p2;

          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 be Real such that

           A14: r4 in W and

           A15: r4 < (r2 + (r0 / |.(v2 - v1).|)) by A3, A6, SEQ_4:def 2;

          reconsider r4 as Real;

          (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 = p3 as Point of ( Euclid n) by EUCLID: 22;

          reconsider v3 = p3, v4 = p as Element of ( REAL n) by EUCLID: 22;

          

           A17: (p3 - p) = ((((1 - r4) * p1) + (r4 * p2)) + (( - ((1 - r2) * p1)) - (r2 * p2))) by RLVECT_1: 30

          .= (((((1 - r4) * p1) + (r4 * p2)) + ( - ((1 - r2) * p1))) + ( - (r2 * p2))) by RLVECT_1:def 3

          .= (((r4 * p2) + (((1 - r4) * p1) + ( - ((1 - r2) * p1)))) + ( - (r2 * p2))) by RLVECT_1:def 3

          .= (((((1 - r4) * p1) + ( - ((1 - r2) * p1))) + (r4 * p2)) + (( - r2) * p2)) by RLVECT_1: 79

          .= (((((1 - r4) * p1) + (( - (1 - r2)) * p1)) + (r4 * p2)) + (( - r2) * p2)) by RLVECT_1: 79

          .= ((((1 - r4) * p1) + (( - (1 - r2)) * p1)) + ((r4 * p2) + (( - r2) * p2))) by RLVECT_1:def 3

          .= ((((1 - r4) * p1) + (( - (1 - r2)) * p1)) + ((r4 + ( - r2)) * p2)) by RLVECT_1:def 6

          .= ((((1 - r4) + ( - (1 - r2))) * p1) + ((r4 - r2) * p2)) by RLVECT_1:def 6

          .= ((( - (r4 - r2)) * p1) + ((r4 - r2) * p2))

          .= (((r4 - r2) * p2) - ((r4 - r2) * p1)) by RLVECT_1: 79

          .= ((r4 - r2) * (p2 - p1)) by RLVECT_1: 34

          .= ((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

          .= |.(p3 - p).|

          .= |.((r4 - r2) * (v2 - v1)).| by A17

          .= ( |.(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 be Point of ( Euclid n) : ( dist (u,u0)) < r0 };

          then

           A19: u3 in ( Ball (u,r0)) by METRIC_1: 17;

          ex r 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;

        end;

          suppose

           A20: p1 = p2;

          then

           A21: ( LSeg (p1,p2)) = {p1} by RLTOPSP1: 70;

          

           A22: ex q1 be Point of ( TOP-REAL n) st q1 in P by SUBSET_1: 4;

          p = (((1 - r2) + r2) * p1) by A20, RLVECT_1:def 6

          .= p1 by RLVECT_1:def 8;

          hence contradiction by A2, A9, A21, A22, TARSKI:def 1;

        end;

      end;

      let r;

      assume 0 <= r & r <= 1 & (((1 - r) * p1) + (r * p2)) in P;

      then r in W;

      hence thesis by A3, SEQ_4:def 2;

    end;

    theorem :: SPPOL_1:7

    

     Th7: for p1, p2, q1, q2 st ( LSeg (q1,q2)) c= ( LSeg (p1,p2)) & p1 in ( LSeg (q1,q2)) holds p1 = q1 or p1 = q2

    proof

      let p1, p2, q1, q2;

      assume

       A1: ( LSeg (q1,q2)) c= ( LSeg (p1,p2));

      q2 in ( LSeg (q1,q2)) by RLTOPSP1: 68;

      then q2 in ( LSeg (p1,p2)) by A1;

      then

      consider s2 such that

       A2: q2 = (((1 - s2) * p1) + (s2 * p2)) and

       A3: 0 <= s2 and s2 <= 1;

      assume p1 in ( LSeg (q1,q2));

      then

      consider r1 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 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, RLVECT_1:def 5

      .= ((((1 - r1) * ((1 - s1) * p1)) + ((1 - r1) * (s1 * p2))) + ((r1 * ((1 - s2) * p1)) + (r1 * (s2 * p2)))) by RLVECT_1:def 5

      .= (((((1 - r1) * ((1 - s1) * p1)) + ((1 - r1) * (s1 * p2))) + (r1 * ((1 - s2) * p1))) + (r1 * (s2 * p2))) by RLVECT_1:def 3

      .= ((((((1 - r1) * (1 - s1)) * p1) + ((1 - r1) * (s1 * p2))) + (r1 * ((1 - s2) * p1))) + (r1 * (s2 * p2))) by RLVECT_1:def 7

      .= ((((((1 - r1) * (1 - s1)) * p1) + (((1 - r1) * s1) * p2)) + (r1 * ((1 - s2) * p1))) + (r1 * (s2 * p2))) by RLVECT_1:def 7

      .= ((((((1 - r1) * (1 - s1)) * p1) + (((1 - r1) * s1) * p2)) + ((r1 * (1 - s2)) * p1)) + (r1 * (s2 * p2))) by RLVECT_1:def 7

      .= ((((((1 - r1) * (1 - s1)) * p1) + (((1 - r1) * s1) * p2)) + ((r1 * (1 - s2)) * p1)) + ((r1 * s2) * p2)) by RLVECT_1:def 7

      .= ((((r1 * s2) * p2) + ((((1 - r1) * s1) * p2) + (((1 - r1) * (1 - s1)) * p1))) + ((r1 * (1 - s2)) * p1)) by RLVECT_1:def 3

      .= (((((r1 * s2) * p2) + (((1 - r1) * s1) * p2)) + (((1 - r1) * (1 - s1)) * p1)) + ((r1 * (1 - s2)) * p1)) by RLVECT_1:def 3

      .= (((((r1 * s2) + ((1 - r1) * s1)) * p2) + (((1 - r1) * (1 - s1)) * p1)) + ((r1 * (1 - s2)) * p1)) by RLVECT_1:def 6

      .= ((((r1 * s2) + ((1 - r1) * s1)) * p2) + ((((1 - r1) * (1 - s1)) * p1) + ((r1 * (1 - s2)) * p1))) by RLVECT_1:def 3

      .= ((((r1 * s2) + ((1 - r1) * s1)) * p2) + ((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) * p1)) by RLVECT_1:def 6;

      

      then ( 0. ( TOP-REAL n)) = (((((r1 * s2) + ((1 - r1) * s1)) * p2) + ((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) * p1)) - p1) by RLVECT_1: 5

      .= ((((r1 * s2) + ((1 - r1) * s1)) * p2) + (((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) * p1) - p1)) by RLVECT_1:def 3

      .= ((((r1 * s2) + ((1 - r1) * s1)) * p2) + (((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) * p1) - (1 * p1))) by RLVECT_1:def 8

      .= ((((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) - 1) * p1) + (((r1 * s2) + ((1 - r1) * s1)) * p2)) by RLVECT_1: 35

      .= ((((((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 RLVECT_1: 21;

      then (((((1 - r1) * (1 - s1)) + (r1 * (1 - s2))) - 1) * p1) = (( - ((r1 * s2) + ((1 - r1) * s1))) * p2) by RLVECT_1: 79;

      then

       A9: ( - ((r1 * s2) + ((1 - r1) * s1))) = ( - 0 ) or p1 = p2 by RLVECT_1: 36;

      per cases by A9;

        suppose

         A10: ((r1 * s2) + ((1 - r1) * s1)) = 0 ;

        now

          per cases by A5, A8, A3, A10, XREAL_1: 170;

            suppose r1 = 0 & s1 = 0 ;

            

            then p1 = ((1 * q1) + ( 0. ( TOP-REAL n))) by A4, RLVECT_1: 10

            .= (q1 + ( 0. ( TOP-REAL n))) by RLVECT_1:def 8

            .= q1 by RLVECT_1: 4;

            hence thesis;

          end;

            suppose r1 = 1 & s2 = 0 ;

            

            then p1 = (( 0. ( TOP-REAL n)) + (1 * q2)) by A4, RLVECT_1: 10

            .= (1 * q2) by RLVECT_1: 4

            .= q2 by RLVECT_1:def 8;

            hence thesis;

          end;

            suppose s2 = 0 & s1 = 0 ;

            

            then q1 = ((1 * p1) + ( 0. ( TOP-REAL n))) by A7, RLVECT_1: 10

            .= (p1 + ( 0. ( TOP-REAL n))) by RLVECT_1:def 8

            .= p1 by RLVECT_1: 4;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

        suppose p1 = p2;

        then ( LSeg (q1,q2)) c= {p1} by A1, RLTOPSP1: 70;

        hence thesis by A6, TARSKI:def 1;

      end;

    end;

    theorem :: SPPOL_1:8

    for p1, p2, q1, q2 st ( LSeg (p1,p2)) = ( LSeg (q1,q2)) holds p1 = q1 & p2 = q2 or p1 = q2 & p2 = q1

    proof

      let p1, p2, q1, q2;

      

       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));

      per cases by A3, Th7, RLTOPSP1: 68;

        suppose

         A4: p1 = q1 & p2 = q1;

        then ( LSeg (p1,p2)) = {q1} by RLTOPSP1: 70;

        hence thesis by A3, A2, A4, TARSKI:def 1;

      end;

        suppose

         A5: p1 = q2 & p2 = q2;

        then ( LSeg (p1,p2)) = {q2} by RLTOPSP1: 70;

        hence thesis by A3, A1, A5, TARSKI:def 1;

      end;

        suppose p1 = q1 & p2 = q2 or p1 = q2 & p2 = q1;

        hence thesis;

      end;

    end;

    registration

      let n, p1, p2;

      cluster ( LSeg (p1,p2)) -> compact;

      coherence

      proof

        set P = ( LSeg (p1,p2)), T = (( TOP-REAL n) | P);

        now

          per cases ;

            suppose p1 = p2;

            then P = {p1} by RLTOPSP1: 70;

            

            then

             A1: {p1} = ( [#] T) by PRE_TOPC:def 5

            .= the carrier of T;

            then ( Sspace p1) = T by TEX_2:def 2;

            then T = ( 1TopSp {p1}) by A1, TDLAT_3:def 1;

            hence T is compact;

          end;

            suppose p1 <> p2;

            then ( LSeg (p1,p2)) is_an_arc_of (p1,p2) by TOPREAL1: 9;

            then

            consider f be Function of I[01] , T such that

             A2: f is being_homeomorphism and (f . 0 ) = p1 and (f . 1) = p2;

            

             A3: I[01] is compact by HEINE: 4, TOPMETR: 20;

            f is continuous & ( rng f) = ( [#] T) by A2, TOPS_2:def 5;

            hence T is compact by A3, COMPTS_1: 14;

          end;

        end;

        hence thesis by COMPTS_1: 3;

      end;

      cluster ( LSeg (p1,p2)) -> closed;

      coherence by COMPTS_1: 7;

    end

    definition

      let n, p;

      let P be Subset of ( TOP-REAL n);

      :: SPPOL_1:def1

      pred p is_extremal_in P means p in P & for p1, p2 st p in ( LSeg (p1,p2)) & ( LSeg (p1,p2)) c= P holds p = p1 or p = p2;

    end

    theorem :: SPPOL_1:9

    for P,Q be 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 P,Q be Subset of ( TOP-REAL n);

      assume that

       A1: p is_extremal_in P and

       A2: Q c= P;

      assume p in Q;

      hence p in Q;

      let p1, p2;

      assume

       A3: p in ( LSeg (p1,p2));

      assume ( LSeg (p1,p2)) c= Q;

      then ( LSeg (p1,p2)) c= P by A2;

      hence thesis by A1, A3;

    end;

    theorem :: SPPOL_1:10

    p is_extremal_in {p}

    proof

      thus p in {p} by TARSKI:def 1;

      let p1, p2;

      assume that p in ( LSeg (p1,p2)) and

       A1: ( LSeg (p1,p2)) c= {p};

      p2 in ( LSeg (p1,p2)) by RLTOPSP1: 68;

      hence thesis by A1, TARSKI:def 1;

    end;

    theorem :: SPPOL_1:11

    

     Th11: p1 is_extremal_in ( LSeg (p1,p2)) by RLTOPSP1: 68, Th7;

    theorem :: SPPOL_1:12

    p2 is_extremal_in ( LSeg (p1,p2)) by Th11;

    theorem :: SPPOL_1:13

    p is_extremal_in ( LSeg (p1,p2)) implies p = p1 or p = p2;

    begin

    reserve P,Q for Subset of ( TOP-REAL 2),

f,f1,f2 for FinSequence of the carrier of ( TOP-REAL 2),

p,p1,p2,p3,q,q3 for Point of ( TOP-REAL 2);

    theorem :: SPPOL_1:14

    

     Th14: for p1, p2 st (p1 `1 ) <> (p2 `1 ) & (p1 `2 ) <> (p2 `2 ) holds ex p 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;

      assume that

       A1: (p1 `1 ) <> (p2 `1 ) and

       A2: (p1 `2 ) <> (p2 `2 );

      take p = ((1 / 2) * (p1 + p2));

      

       A3: p = (((1 - (1 / 2)) * p1) + ((1 / 2) * p2)) by RLVECT_1:def 5;

      hence p in ( LSeg (p1,p2));

      hereby

        assume

         A4: (p `1 ) = (p1 `1 );

        (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;

      end;

      hereby

        assume

         A5: (p `1 ) = (p2 `1 );

        (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;

      end;

      hereby

        assume

         A6: (p `2 ) = (p1 `2 );

        (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;

      end;

      hereby

        assume

         A7: (p `2 ) = (p2 `2 );

        (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;

      end;

    end;

    definition

      let P;

      :: SPPOL_1:def2

      attr P is horizontal means for p, q st p in P & q in P holds (p `2 ) = (q `2 );

      :: SPPOL_1:def3

      attr P is vertical means for p, q st p in P & q in P holds (p `1 ) = (q `1 );

    end

    

     Lm1: P is non trivial & P is horizontal implies P is non vertical

    proof

      assume that

       A1: P is non trivial and

       A2: (for p, q st p in P & q in P holds (p `2 ) = (q `2 )) & for p, q st p in P & q in P holds (p `1 ) = (q `1 );

      consider p, q 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;

    end;

    registration

      cluster non trivial horizontal -> non vertical for Subset of ( TOP-REAL 2);

      coherence by Lm1;

      cluster non trivial vertical -> non horizontal for Subset of ( TOP-REAL 2);

      coherence ;

    end

    theorem :: SPPOL_1:15

    

     Th15: (p `2 ) = (q `2 ) iff ( LSeg (p,q)) is horizontal

    proof

      set P = ( LSeg (p,q));

      thus (p `2 ) = (q `2 ) implies P is horizontal

      proof

        assume

         A1: (p `2 ) = (q `2 );

        let p1, p2;

        assume

         A2: p1 in P;

        assume p2 in P;

        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 thesis by A3, XXREAL_0: 1;

      end;

      p in P & q in P by RLTOPSP1: 68;

      hence thesis;

    end;

    theorem :: SPPOL_1:16

    

     Th16: (p `1 ) = (q `1 ) iff ( LSeg (p,q)) is vertical

    proof

      set P = ( LSeg (p,q));

      thus (p `1 ) = (q `1 ) implies P is vertical

      proof

        assume

         A1: (p `1 ) = (q `1 );

        let p1, p2;

        assume

         A2: p1 in P;

        assume p2 in P;

        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 thesis by A3, XXREAL_0: 1;

      end;

      p in P & q in P by RLTOPSP1: 68;

      hence thesis;

    end;

    theorem :: SPPOL_1:17

    p1 in ( LSeg (p,q)) & p2 in ( LSeg (p,q)) & (p1 `1 ) <> (p2 `1 ) & (p1 `2 ) = (p2 `2 ) implies ( LSeg (p,q)) is horizontal

    proof

      assume p1 in ( LSeg (p,q));

      then

      consider r1 such that

       A1: p1 = (((1 - r1) * p) + (r1 * q)) and 0 <= r1 and r1 <= 1;

      assume p2 in ( LSeg (p,q));

      then

      consider r2 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 );

      ((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 thesis by Th15;

    end;

    theorem :: SPPOL_1:18

    p1 in ( LSeg (p,q)) & p2 in ( LSeg (p,q)) & (p1 `2 ) <> (p2 `2 ) & (p1 `1 ) = (p2 `1 ) implies ( LSeg (p,q)) is vertical

    proof

      assume p1 in ( LSeg (p,q));

      then

      consider r1 such that

       A1: p1 = (((1 - r1) * p) + (r1 * q)) and 0 <= r1 and r1 <= 1;

      assume p2 in ( LSeg (p,q));

      then

      consider r2 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 );

      ((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 thesis by Th16;

    end;

    registration

      let f, i;

      cluster ( LSeg (f,i)) -> closed;

      coherence

      proof

        per cases ;

          suppose 1 <= i & (i + 1) <= ( len f);

          then ( LSeg (f,i)) = ( LSeg ((f /. i),(f /. (i + 1)))) by TOPREAL1:def 3;

          hence thesis;

        end;

          suppose

           A1: not (1 <= i & (i + 1) <= ( len f));

          ( {} ( TOP-REAL 2)) is closed;

          hence thesis by A1, TOPREAL1:def 3;

        end;

      end;

    end

    theorem :: SPPOL_1:19

    

     Th19: f is special implies ( LSeg (f,i)) is vertical or ( LSeg (f,i)) is horizontal

    proof

      assume

       A1: for j be Nat st 1 <= j & (j + 1) <= ( len f) holds ((f /. j) `1 ) = ((f /. (j + 1)) `1 ) or ((f /. j) `2 ) = ((f /. (j + 1)) `2 );

      set p1 = (f /. i), p2 = (f /. (i + 1));

      per cases ;

        suppose

         A2: 1 <= i & (i + 1) <= ( len f);

        

         A3: (p1 `2 ) = (p2 `2 ) implies ( LSeg (p1,p2)) is horizontal by Th15;

        (p1 `1 ) = (p2 `1 ) implies ( LSeg (p1,p2)) is vertical by Th16;

        hence thesis by A1, A2, A3, TOPREAL1:def 3;

      end;

        suppose not (1 <= i & (i + 1) <= ( len f));

        then for p, q st p in ( LSeg (f,i)) & q in ( LSeg (f,i)) holds (p `2 ) = (q `2 ) by TOPREAL1:def 3;

        hence thesis;

      end;

    end;

    theorem :: SPPOL_1:20

    

     Th20: f is one-to-one & 1 <= i & (i + 1) <= ( len f) implies ( LSeg (f,i)) is non trivial

    proof

      assume

       A1: f is one-to-one;

      

       A2: i <> (i + 1);

      assume

       A3: 1 <= i & (i + 1) <= ( len f);

      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 thesis by A4, A5, ZFMISC_1:def 10;

    end;

    theorem :: SPPOL_1:21

    f is one-to-one & 1 <= i & (i + 1) <= ( len f) & ( LSeg (f,i)) is vertical implies ( LSeg (f,i)) is non horizontal by Lm1, Th20;

    theorem :: SPPOL_1:22

    

     Th22: for f holds { ( LSeg (f,i)) : 1 <= i & i <= ( len f) } is finite

    proof

      defpred X[ set] means not contradiction;

      deffunc U( FinSequence of ( TOP-REAL 2), Nat) = ( LSeg ($1,$2));

      let f;

      set Y = { ( LSeg (f,i)) : 1 <= i & i <= ( len f) };

      set X = { U(f,i) : 1 <= i & i <= ( len f) & X[i] };

      

       A1: for e be object holds e in X iff e in Y

      proof

        let e be object;

        thus e in X implies e in Y

        proof

          assume e in X;

          then ex i be Nat st e = U(f,i) & 1 <= i & i <= ( len f) & X[i];

          hence thesis;

        end;

        assume e in Y;

        then ex i be Nat st e = ( LSeg (f,i)) & 1 <= i & i <= ( len f);

        hence thesis;

      end;

      X is finite from FinSeqFam9;

      hence thesis by A1, TARSKI: 2;

    end;

    theorem :: SPPOL_1:23

    

     Th23: for f holds { ( LSeg (f,i)) : 1 <= i & (i + 1) <= ( len f) } is finite

    proof

      let f;

      set F = { ( LSeg (f,i)) : 1 <= i & (i + 1) <= ( len f) }, F9 = { ( LSeg (f,i)) : 1 <= i & i <= ( len f) };

      F c= F9

      proof

        let x be object;

        assume x in F;

        then

        consider i be 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 thesis by A1;

      end;

      hence thesis by Th22, FINSET_1: 1;

    end;

    

     Lm2: for f, k holds { ( LSeg (f,i)) : 1 <= i & (i + 1) <= ( len f) & i <> k & i <> (k + 1) } is finite

    proof

      let f, k;

      set F = { ( LSeg (f,i)) : 1 <= i & (i + 1) <= ( len f) & i <> k & i <> (k + 1) };

      set F1 = { ( LSeg (f,i)) : 1 <= i & (i + 1) <= ( len f) };

      F c= F1

      proof

        let x be object;

        assume x in F;

        then ex i st ( LSeg (f,i)) = x & 1 <= i & (i + 1) <= ( len f) & i <> k & i <> (k + 1);

        hence thesis;

      end;

      hence thesis by Th23, FINSET_1: 1;

    end;

    theorem :: SPPOL_1:24

    for f holds { ( LSeg (f,i)) : 1 <= i & i <= ( len f) } is Subset-Family of ( TOP-REAL 2)

    proof

      let f;

      set F = { ( LSeg (f,i)) : 1 <= i & i <= ( len f) };

      F c= ( bool ( REAL 2))

      proof

        let x be object;

        assume x in F;

        then ex i st ( LSeg (f,i)) = x & 1 <= i & i <= ( len f);

        then x is Subset of ( REAL 2) by EUCLID: 22;

        hence thesis;

      end;

      hence thesis by EUCLID: 22;

    end;

    theorem :: SPPOL_1:25

    

     Th25: for f holds { ( LSeg (f,i)) : 1 <= i & (i + 1) <= ( len f) } is Subset-Family of ( TOP-REAL 2)

    proof

      let f;

      set F = { ( LSeg (f,i)) : 1 <= i & (i + 1) <= ( len f) };

      F c= ( bool ( REAL 2))

      proof

        let x be object;

        assume x in F;

        then ex i st ( LSeg (f,i)) = x & 1 <= i & (i + 1) <= ( len f);

        then x is Subset of ( REAL 2) by EUCLID: 22;

        hence thesis;

      end;

      hence thesis by EUCLID: 22;

    end;

    

     Lm3: for f, k holds { ( LSeg (f,i)) : 1 <= i & (i + 1) <= ( len f) & i <> k & i <> (k + 1) } is Subset-Family of ( TOP-REAL 2)

    proof

      let f, k;

      set F = { ( LSeg (f,i)) : 1 <= i & (i + 1) <= ( len f) & i <> k & i <> (k + 1) };

      F c= ( bool ( REAL 2))

      proof

        let x be object;

        assume x in F;

        then ex i 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 thesis;

      end;

      hence thesis by EUCLID: 22;

    end;

    theorem :: SPPOL_1:26

    

     Th26: for f st Q = ( union { ( LSeg (f,i)) : 1 <= i & (i + 1) <= ( len f) }) holds Q is closed

    proof

      let f;

      reconsider F = { ( LSeg (f,i)) : 1 <= i & (i + 1) <= ( len f) } as Subset-Family of ( TOP-REAL 2) by Th25;

      now

        let P;

        assume P in F;

        then ex i st ( LSeg (f,i)) = P & 1 <= i & (i + 1) <= ( len f);

        hence P is closed;

      end;

      then

       A1: F is closed by TOPS_2:def 2;

      F is finite by Th23;

      hence thesis by A1, TOPS_2: 21;

    end;

    registration

      let f;

      cluster ( L~ f) -> closed;

      coherence by Th26;

    end

    

     Lm4: for f, Q, k st Q = ( union { ( LSeg (f,i)) : 1 <= i & (i + 1) <= ( len f) & i <> k & i <> (k + 1) }) holds Q is closed

    proof

      let f, Q, k;

      reconsider F = { ( LSeg (f,i)) : 1 <= i & (i + 1) <= ( len f) & i <> k & i <> (k + 1) } as Subset-Family of ( TOP-REAL 2) by Lm3;

      now

        let P;

        assume P in F;

        then ex i st ( LSeg (f,i)) = P & 1 <= i & (i + 1) <= ( len f) & i <> k & i <> (k + 1);

        hence P is closed;

      end;

      then

       A1: F is closed by TOPS_2:def 2;

      F is finite by Lm2;

      hence thesis by A1, TOPS_2: 21;

    end;

    definition

      let IT be FinSequence of ( TOP-REAL 2);

      :: SPPOL_1:def4

      attr IT is alternating means for i st 1 <= i & (i + 2) <= ( len IT) holds ((IT /. i) `1 ) <> ((IT /. (i + 2)) `1 ) & ((IT /. i) `2 ) <> ((IT /. (i + 2)) `2 );

    end

    theorem :: SPPOL_1:27

    

     Th27: f is special alternating & 1 <= i & (i + 2) <= ( len f) & ((f /. i) `1 ) = ((f /. (i + 1)) `1 ) implies ((f /. (i + 1)) `2 ) = ((f /. (i + 2)) `2 )

    proof

      assume that

       A1: f is special and

       A2: f is alternating & 1 <= i and

       A3: (i + 2) <= ( len f);

      set p2 = (f /. (i + 1)), p3 = (f /. (i + 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;

      hence thesis by A2, A3;

    end;

    theorem :: SPPOL_1:28

    

     Th28: f is special alternating & 1 <= i & (i + 2) <= ( len f) & ((f /. i) `2 ) = ((f /. (i + 1)) `2 ) implies ((f /. (i + 1)) `1 ) = ((f /. (i + 2)) `1 )

    proof

      assume that

       A1: f is special and

       A2: f is alternating & 1 <= i and

       A3: (i + 2) <= ( len f);

      set p2 = (f /. (i + 1)), p3 = (f /. (i + 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;

      hence thesis by A2, A3;

    end;

    theorem :: SPPOL_1:29

    

     Th29: f is special alternating & 1 <= i & (i + 2) <= ( len f) & p1 = (f /. i) & p2 = (f /. (i + 1)) & p3 = (f /. (i + 2)) implies (p1 `1 ) = (p2 `1 ) & (p3 `1 ) <> (p2 `1 ) or (p1 `2 ) = (p2 `2 ) & (p3 `2 ) <> (p2 `2 )

    proof

      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));

      (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;

      hence thesis by A2, A3, A4, A5, A7;

    end;

    theorem :: SPPOL_1:30

    f is special alternating & 1 <= i & (i + 2) <= ( len f) & p1 = (f /. i) & p2 = (f /. (i + 1)) & p3 = (f /. (i + 2)) implies (p2 `1 ) = (p3 `1 ) & (p1 `1 ) <> (p2 `1 ) or (p2 `2 ) = (p3 `2 ) & (p1 `2 ) <> (p2 `2 )

    proof

      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));

      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;

      hence thesis by A2, A3, A4, A6;

    end;

    

     Lm5: for f, i, p1, p2 st f is alternating & 1 <= i & (i + 2) <= ( len f) & p1 = (f /. i) & p2 = (f /. (i + 2)) holds ex p 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, i, p1, p2;

      assume f is alternating & 1 <= i & (i + 2) <= ( len f) & p1 = (f /. i) & p2 = (f /. (i + 2));

      then (p1 `1 ) <> (p2 `1 ) & (p1 `2 ) <> (p2 `2 );

      hence thesis by Th14;

    end;

    theorem :: SPPOL_1:31

    f is special alternating & 1 <= i & (i + 2) <= ( len f) implies not ( LSeg ((f /. i),(f /. (i + 2)))) c= (( LSeg (f,i)) \/ ( LSeg (f,(i + 1))))

    proof

      set p1 = (f /. i), 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);

      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 (p1,p0)) 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 (p0,p2)) by A4, TOPREAL1:def 3;

      consider p such that

       A7: p in ( LSeg (p1,p2)) and

       A8: (p `1 ) <> (p1 `1 ) and

       A9: (p `1 ) <> (p2 `1 ) and

       A10: (p `2 ) <> (p1 `2 ) and

       A11: (p `2 ) <> (p2 `2 ) by A2, A3, A4, Lm5;

      assume

       A12: ( LSeg (p1,p2)) c= (( LSeg (f,i)) \/ ( LSeg (f,(i + 1))));

      per cases by A7, A5, A6, A12, XBOOLE_0:def 3;

        suppose

         A13: p in ( LSeg (p1,p0));

        

         A14: p1 in ( LSeg (p1,p0)) by RLTOPSP1: 68;

        ( LSeg (p1,p0)) is vertical or ( LSeg (p1,p0)) is horizontal by A1, A5, Th19;

        hence contradiction by A8, A10, A13, A14;

      end;

        suppose

         A15: p in ( LSeg (p0,p2));

        

         A16: p2 in ( LSeg (p0,p2)) by RLTOPSP1: 68;

        ( LSeg (p0,p2)) is vertical or ( LSeg (p0,p2)) is horizontal by A1, A6, Th19;

        hence contradiction by A9, A11, A15, A16;

      end;

    end;

    theorem :: SPPOL_1:32

    

     Th32: f is special alternating & 1 <= i & (i + 2) <= ( len f) & ( LSeg (f,i)) is vertical implies ( LSeg (f,(i + 1))) is horizontal

    proof

      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;

      (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 thesis by A3, A5, TOPREAL1:def 3;

    end;

    theorem :: SPPOL_1:33

    

     Th33: f is special alternating & 1 <= i & (i + 2) <= ( len f) & ( LSeg (f,i)) is horizontal implies ( LSeg (f,(i + 1))) is vertical

    proof

      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;

      (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 thesis by A3, A5, TOPREAL1:def 3;

    end;

    theorem :: SPPOL_1:34

    f is special alternating & 1 <= i & (i + 2) <= ( len f) implies ( LSeg (f,i)) is vertical & ( LSeg (f,(i + 1))) is horizontal or ( LSeg (f,i)) is horizontal & ( LSeg (f,(i + 1))) is vertical by Th32, Th19, Th33;

    theorem :: SPPOL_1:35

    

     Th35: f is special 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)))) implies (f /. (i + 1)) = p or (f /. (i + 1)) = q

    proof

      assume that

       A1: f is special & f is alternating and

       A2: 1 <= i and

       A3: (i + 2) <= ( len f);

      (i + 1) <= (i + 2) by XREAL_1: 6;

      then

       A4: (i + 1) <= ( len f) by A3, XXREAL_0: 2;

      set p1 = (f /. i), p0 = (f /. (i + 1)), p2 = (f /. (i + 2));

      

       A5: (i + (1 + 1)) = ((i + 1) + 1) & 1 <= (i + 1) by NAT_1: 11;

      assume that

       A6: p0 in ( LSeg (p,q)) and

       A7: ( LSeg (p,q)) c= (( LSeg (f,i)) \/ ( LSeg (f,(i + 1))));

      

       A8: p in ( LSeg (p,q)) & q in ( LSeg (p,q)) by RLTOPSP1: 68;

      now

        per cases by A7, A8, XBOOLE_0:def 3;

          case p in ( LSeg (f,i)) & q in ( LSeg (f,i));

          then p in ( LSeg (p1,p0)) & q in ( LSeg (p1,p0)) by A2, A4, TOPREAL1:def 3;

          then

           A9: ( LSeg (p,q)) c= ( LSeg (p1,p0)) by TOPREAL1: 6;

          p0 is_extremal_in ( LSeg (p1,p0)) by Th11;

          hence thesis by A6, A9;

        end;

          case

           A10: p in ( LSeg (f,i)) & q in ( LSeg (f,(i + 1)));

          then p in ( LSeg (p1,p0)) by A2, A4, TOPREAL1:def 3;

          then

          consider s such that

           A11: p = (((1 - s) * p1) + (s * p0)) and 0 <= s and s <= 1;

          

           A12: (p `1 ) = ((((1 - s) * p1) `1 ) + ((s * p0) `1 )) by A11, TOPREAL3: 2

          .= (((1 - s) * (p1 `1 )) + ((s * p0) `1 )) by TOPREAL3: 4

          .= (((1 - s) * (p1 `1 )) + (s * (p0 `1 ))) by TOPREAL3: 4;

          q in ( LSeg (p0,p2)) by A3, A5, A10, TOPREAL1:def 3;

          then

          consider s1 such that

           A13: q = (((1 - s1) * p0) + (s1 * p2)) and 0 <= s1 and s1 <= 1;

          

           A14: (q `2 ) = ((((1 - s1) * p0) `2 ) + ((s1 * p2) `2 )) by A13, TOPREAL3: 2

          .= (((1 - s1) * (p0 `2 )) + ((s1 * p2) `2 )) by TOPREAL3: 4

          .= (((1 - s1) * (p0 `2 )) + (s1 * (p2 `2 ))) by TOPREAL3: 4;

          

           A15: (p `2 ) = ((((1 - s) * p1) `2 ) + ((s * p0) `2 )) by A11, TOPREAL3: 2

          .= (((1 - s) * (p1 `2 )) + ((s * p0) `2 )) by TOPREAL3: 4

          .= (((1 - s) * (p1 `2 )) + (s * (p0 `2 ))) by TOPREAL3: 4;

          

           A16: (q `1 ) = ((((1 - s1) * p0) `1 ) + ((s1 * p2) `1 )) by A13, TOPREAL3: 2

          .= (((1 - s1) * (p0 `1 )) + ((s1 * p2) `1 )) by TOPREAL3: 4

          .= (((1 - s1) * (p0 `1 )) + (s1 * (p2 `1 ))) by TOPREAL3: 4;

          now

            

             A17: (f /. (i + 2)) = (f /. (i + 2)) & (f /. i) = (f /. i);

            per cases by A1, A2, A3, A17, Th29;

              case

               A18: (p1 `1 ) = (p0 `1 ) & (p2 `1 ) <> (p0 `1 );

              consider r such that

               A19: p0 = (((1 - r) * p) + (r * q)) and 0 <= r and r <= 1 by A6;

              (p0 `1 ) = ((((1 - r) * p) `1 ) + ((r * q) `1 )) by A19, TOPREAL3: 2

              .= (((1 - r) * (p `1 )) + ((r * q) `1 )) by TOPREAL3: 4

              .= (((1 - r) * (p0 `1 )) + (r * (q `1 ))) by A12, A18, TOPREAL3: 4;

              then (r * ((p0 `1 ) - (q `1 ))) = 0 ;

              then

               A20: r = 0 or ((p0 `1 ) - (q `1 )) = 0 by XCMPLX_1: 6;

              now

                per cases by A20;

                  case r = 0 ;

                  

                  then p0 = (((1 - 0 ) * p) + ( 0. ( TOP-REAL 2))) by A19, RLVECT_1: 10

                  .= (1 * p) by RLVECT_1: 4

                  .= p by RLVECT_1:def 8;

                  hence thesis;

                end;

                  case (p0 `1 ) = (q `1 );

                  then (s1 * ((p0 `1 ) - (p2 `1 ))) = 0 by A16;

                  then

                   A21: s1 = 0 or ((p0 `1 ) - (p2 `1 )) = 0 by XCMPLX_1: 6;

                  now

                    per cases by A21;

                      case s1 = 0 ;

                      

                      then q = (((1 - 0 ) * p0) + ( 0. ( TOP-REAL 2))) by A13, RLVECT_1: 10

                      .= (1 * p0) by RLVECT_1: 4

                      .= p0 by RLVECT_1:def 8;

                      hence thesis;

                    end;

                      case (p0 `1 ) = (p2 `1 );

                      hence contradiction by A18;

                    end;

                  end;

                  hence thesis;

                end;

              end;

              hence thesis;

            end;

              case

               A22: (p1 `2 ) = (p0 `2 ) & (p2 `2 ) <> (p0 `2 );

              consider r such that

               A23: p0 = (((1 - r) * p) + (r * q)) and 0 <= r and r <= 1 by A6;

              (p0 `2 ) = ((((1 - r) * p) `2 ) + ((r * q) `2 )) by A23, TOPREAL3: 2

              .= (((1 - r) * (p `2 )) + ((r * q) `2 )) by TOPREAL3: 4

              .= (((1 - r) * (p0 `2 )) + (r * (q `2 ))) by A15, A22, TOPREAL3: 4;

              then (r * ((p0 `2 ) - (q `2 ))) = 0 ;

              then

               A24: r = 0 or ((p0 `2 ) - (q `2 )) = 0 by XCMPLX_1: 6;

              now

                per cases by A24;

                  case r = 0 ;

                  

                  then p0 = (((1 - 0 ) * p) + ( 0. ( TOP-REAL 2))) by A23, RLVECT_1: 10

                  .= (1 * p) by RLVECT_1: 4

                  .= p by RLVECT_1:def 8;

                  hence thesis;

                end;

                  case (p0 `2 ) = (q `2 );

                  then (s1 * ((p0 `2 ) - (p2 `2 ))) = 0 by A14;

                  then

                   A25: s1 = 0 or ((p0 `2 ) - (p2 `2 )) = 0 by XCMPLX_1: 6;

                  now

                    per cases by A25;

                      case s1 = 0 ;

                      

                      then q = (((1 - 0 ) * p0) + ( 0. ( TOP-REAL 2))) by A13, RLVECT_1: 10

                      .= (1 * p0) by RLVECT_1: 4

                      .= p0 by RLVECT_1:def 8;

                      hence thesis;

                    end;

                      case (p0 `2 ) = (p2 `2 );

                      hence contradiction by A22;

                    end;

                  end;

                  hence thesis;

                end;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

          case

           A26: p in ( LSeg (f,(i + 1))) & q in ( LSeg (f,i));

          then q in ( LSeg (p1,p0)) by A2, A4, TOPREAL1:def 3;

          then

          consider s such that

           A27: q = (((1 - s) * p1) + (s * p0)) and 0 <= s and s <= 1;

          

           A28: (q `1 ) = ((((1 - s) * p1) `1 ) + ((s * p0) `1 )) by A27, TOPREAL3: 2

          .= (((1 - s) * (p1 `1 )) + ((s * p0) `1 )) by TOPREAL3: 4

          .= (((1 - s) * (p1 `1 )) + (s * (p0 `1 ))) by TOPREAL3: 4;

          p in ( LSeg (p0,p2)) by A3, A5, A26, TOPREAL1:def 3;

          then

          consider s1 such that

           A29: p = (((1 - s1) * p0) + (s1 * p2)) and 0 <= s1 and s1 <= 1;

          

           A30: (p `2 ) = ((((1 - s1) * p0) `2 ) + ((s1 * p2) `2 )) by A29, TOPREAL3: 2

          .= (((1 - s1) * (p0 `2 )) + ((s1 * p2) `2 )) by TOPREAL3: 4

          .= (((1 - s1) * (p0 `2 )) + (s1 * (p2 `2 ))) by TOPREAL3: 4;

          

           A31: (q `2 ) = ((((1 - s) * p1) `2 ) + ((s * p0) `2 )) by A27, TOPREAL3: 2

          .= (((1 - s) * (p1 `2 )) + ((s * p0) `2 )) by TOPREAL3: 4

          .= (((1 - s) * (p1 `2 )) + (s * (p0 `2 ))) by TOPREAL3: 4;

          

           A32: (p `1 ) = ((((1 - s1) * p0) `1 ) + ((s1 * p2) `1 )) by A29, TOPREAL3: 2

          .= (((1 - s1) * (p0 `1 )) + ((s1 * p2) `1 )) by TOPREAL3: 4

          .= (((1 - s1) * (p0 `1 )) + (s1 * (p2 `1 ))) by TOPREAL3: 4;

          now

            

             A33: (f /. (i + 2)) = (f /. (i + 2)) & (f /. i) = (f /. i);

            per cases by A1, A2, A3, A33, Th29;

              case

               A34: (p1 `1 ) = (p0 `1 ) & (p2 `1 ) <> (p0 `1 );

              p0 in ( LSeg (q,p)) by A6;

              then

              consider r such that

               A35: p0 = (((1 - r) * q) + (r * p)) and 0 <= r and r <= 1;

              (p0 `1 ) = ((((1 - r) * q) `1 ) + ((r * p) `1 )) by A35, TOPREAL3: 2

              .= (((1 - r) * (q `1 )) + ((r * p) `1 )) by TOPREAL3: 4

              .= (((1 - r) * (p0 `1 )) + (r * (p `1 ))) by A28, A34, TOPREAL3: 4;

              then (r * ((p0 `1 ) - (p `1 ))) = 0 ;

              then

               A36: r = 0 or ((p0 `1 ) - (p `1 )) = 0 by XCMPLX_1: 6;

              now

                per cases by A36;

                  case r = 0 ;

                  

                  then p0 = (((1 - 0 ) * q) + ( 0. ( TOP-REAL 2))) by A35, RLVECT_1: 10

                  .= (1 * q) by RLVECT_1: 4

                  .= q by RLVECT_1:def 8;

                  hence thesis;

                end;

                  case (p0 `1 ) = (p `1 );

                  then (s1 * ((p0 `1 ) - (p2 `1 ))) = 0 by A32;

                  then

                   A37: s1 = 0 or ((p0 `1 ) - (p2 `1 )) = 0 by XCMPLX_1: 6;

                  now

                    per cases by A37;

                      case s1 = 0 ;

                      

                      then p = (((1 - 0 ) * p0) + ( 0. ( TOP-REAL 2))) by A29, RLVECT_1: 10

                      .= (1 * p0) by RLVECT_1: 4

                      .= p0 by RLVECT_1:def 8;

                      hence thesis;

                    end;

                      case (p0 `1 ) = (p2 `1 );

                      hence contradiction by A34;

                    end;

                  end;

                  hence thesis;

                end;

              end;

              hence thesis;

            end;

              case

               A38: (p1 `2 ) = (p0 `2 ) & (p2 `2 ) <> (p0 `2 );

              p0 in ( LSeg (q,p)) by A6;

              then

              consider r such that

               A39: p0 = (((1 - r) * q) + (r * p)) and 0 <= r and r <= 1;

              (p0 `2 ) = ((((1 - r) * q) `2 ) + ((r * p) `2 )) by A39, TOPREAL3: 2

              .= (((1 - r) * (q `2 )) + ((r * p) `2 )) by TOPREAL3: 4

              .= (((1 - r) * (p0 `2 )) + (r * (p `2 ))) by A31, A38, TOPREAL3: 4;

              then (r * ((p0 `2 ) - (p `2 ))) = 0 ;

              then

               A40: r = 0 or ((p0 `2 ) - (p `2 )) = 0 by XCMPLX_1: 6;

              now

                per cases by A40;

                  case r = 0 ;

                  

                  then p0 = (((1 - 0 ) * q) + ( 0. ( TOP-REAL 2))) by A39, RLVECT_1: 10

                  .= (1 * q) by RLVECT_1: 4

                  .= q by RLVECT_1:def 8;

                  hence thesis;

                end;

                  case (p0 `2 ) = (p `2 );

                  then (s1 * ((p0 `2 ) - (p2 `2 ))) = 0 by A30;

                  then

                   A41: s1 = 0 or ((p0 `2 ) - (p2 `2 )) = 0 by XCMPLX_1: 6;

                  now

                    per cases by A41;

                      case s1 = 0 ;

                      

                      then p = (((1 - 0 ) * p0) + ( 0. ( TOP-REAL 2))) by A29, RLVECT_1: 10

                      .= (1 * p0) by RLVECT_1: 4

                      .= p0 by RLVECT_1:def 8;

                      hence thesis;

                    end;

                      case (p0 `2 ) = (p2 `2 );

                      hence contradiction by A38;

                    end;

                  end;

                  hence thesis;

                end;

              end;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

          case p in ( LSeg (f,(i + 1))) & q in ( LSeg (f,(i + 1)));

          then p in ( LSeg (p0,p2)) & q in ( LSeg (p0,p2)) by A3, A5, TOPREAL1:def 3;

          then

           A42: ( LSeg (p,q)) c= ( LSeg (p0,p2)) by TOPREAL1: 6;

          p0 is_extremal_in ( LSeg (p0,p2)) by Th11;

          hence thesis by A6, A42;

        end;

      end;

      hence thesis;

    end;

    theorem :: SPPOL_1:36

    

     Th36: f is special alternating & 1 <= i & (i + 2) <= ( len f) implies (f /. (i + 1)) is_extremal_in (( LSeg (f,i)) \/ ( LSeg (f,(i + 1))))

    proof

      assume that

       A1: f is special & f is alternating and

       A2: 1 <= i and

       A3: (i + 2) <= ( len f);

      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),p2)) by A2, TOPREAL1:def 3;

      then p2 in ( LSeg (f,i)) by RLTOPSP1: 68;

      then

       A4: p2 in (( LSeg (f,i)) \/ ( LSeg (f,(i + 1)))) by XBOOLE_0:def 3;

      for p, q st p2 in ( LSeg (p,q)) & ( LSeg (p,q)) c= (( LSeg (f,i)) \/ ( LSeg (f,(i + 1)))) holds p2 = p or p2 = q by A1, A2, A3, Th35;

      hence thesis by A4;

    end;

    theorem :: SPPOL_1:37

    

     Th37: for u be Point of ( Euclid 2) st f is special 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 st s > 0 holds ex p3 st not p3 in (( LSeg (f,i)) \/ ( LSeg (f,(i + 1)))) & p3 in ( LSeg (p,q)) & p3 in ( Ball (u,s))

    proof

      let u be Point of ( Euclid 2) such 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))));

      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),p0)) by A2, TOPREAL1:def 3;

      then

       A8: p0 in ( LSeg (f,i)) by RLTOPSP1: 68;

      let s;

      assume

       A9: s > 0 ;

      per cases ;

        suppose p = q;

        then (f /. (i + 1)) in {p} by A5, RLTOPSP1: 70;

        then p in ( LSeg (f,i)) by A8, TARSKI:def 1;

        hence thesis by A7, XBOOLE_0:def 3;

      end;

        suppose

         A10: p <> q;

        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 be Real such that

         A12: p0 = (((1 - s0) * p) + (s0 * q)) and

         A13: 0 <= s0 and

         A14: s0 <= 1 by A5;

        set r3 = ( min ((s0 + (r0 / |.(v2 - v1).|)),1)), r4 = ( max ((s0 + (( - r0) / |.(v2 - v1).|)), 0 ));

        set p4 = (((1 - r4) * p) + (r4 * q));

        set p3 = (((1 - r3) * p) + (r3 * 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 <= r4 & r4 <= 1 by XXREAL_0: 28, XXREAL_0: 30;

        then

         A22: p4 in ( LSeg (p,q));

        

         A23: s0 < (s0 + (r0 / |.(v2 - v1).|)) by A15, A11, XREAL_1: 29, XREAL_1: 139;

         not ( LSeg (p3,p4)) c= (( LSeg (f,i)) \/ ( LSeg (f,(i + 1))))

        proof

          

           A24: p0 in ( LSeg (p3,p4))

          proof

            (s0 + (( - r0) / |.(v2 - v1).|)) < (s0 + (r0 / |.(v2 - v1).|)) by A9, A19, XREAL_1: 6;

            then

             A25: r4 < (s0 + (r0 / |.(v2 - v1).|)) by A17, A13, XXREAL_0: 29;

            

             A26: r4 <= 1 by A21, XXREAL_0: 28;

            per cases by A26, XXREAL_0: 1;

              suppose r4 < 1;

              then r4 < r3 by A25, XXREAL_0: 21;

              then

               A27: (r3 - r4) > 0 by XREAL_1: 50;

              set r5 = ((r3 - s0) / (r3 - r4));

              ( min ((s0 + (r0 / |.(v2 - v1).|)),1)) >= s0 by A14, A16, XXREAL_0: 20;

              then

               A28: (r3 - s0) >= 0 by XREAL_1: 48;

              ( max ((s0 + (( - r0) / |.(v2 - v1).|)), 0 )) <= s0 by A13, A20, XXREAL_0: 28;

              then (r3 - s0) <= (r3 - r4) by XREAL_1: 10;

              then ((r3 - s0) / (r3 - r4)) <= ((r3 - r4) / (r3 - r4)) by A27, XREAL_1: 72;

              then

               A29: r5 <= 1 by A27, XCMPLX_1: 60;

              

               A30: (((1 - ((r3 - s0) / (r3 - r4))) * r3) + (((r3 - s0) / (r3 - r4)) * r4)) = (r3 - (((r3 - s0) / (r3 - r4)) * (r3 - r4)))

              .= (r3 - (r3 - s0)) by A27, XCMPLX_1: 87

              .= s0;

              (((1 - r5) * p3) + (r5 * p4)) = ((((1 - ((r3 - s0) / (r3 - r4))) * ((1 - r3) * p)) + ((1 - ((r3 - s0) / (r3 - r4))) * (r3 * q))) + (((r3 - s0) / (r3 - r4)) * (((1 - r4) * p) + (r4 * q)))) by RLVECT_1:def 5

              .= ((((1 - ((r3 - s0) / (r3 - r4))) * ((1 - r3) * p)) + ((1 - ((r3 - s0) / (r3 - r4))) * (r3 * q))) + ((((r3 - s0) / (r3 - r4)) * ((1 - r4) * p)) + (((r3 - s0) / (r3 - r4)) * (r4 * q)))) by RLVECT_1:def 5

              .= ((((r3 - s0) / (r3 - r4)) * ((1 - r4) * p)) + ((((1 - ((r3 - s0) / (r3 - r4))) * ((1 - r3) * p)) + ((1 - ((r3 - s0) / (r3 - r4))) * (r3 * q))) + (((r3 - s0) / (r3 - r4)) * (r4 * q)))) by RLVECT_1:def 3;

              

              then (((1 - r5) * p3) + (r5 * p4)) = (((((r3 - s0) / (r3 - r4)) * ((1 - r4) * p)) + (((1 - ((r3 - s0) / (r3 - r4))) * ((1 - r3) * p)) + ((1 - ((r3 - s0) / (r3 - r4))) * (r3 * q)))) + (((r3 - s0) / (r3 - r4)) * (r4 * q))) by RLVECT_1:def 3

              .= ((((((r3 - s0) / (r3 - r4)) * ((1 - r4) * p)) + ((1 - ((r3 - s0) / (r3 - r4))) * ((1 - r3) * p))) + ((1 - ((r3 - s0) / (r3 - r4))) * (r3 * q))) + (((r3 - s0) / (r3 - r4)) * (r4 * q))) by RLVECT_1:def 3

              .= (((((((r3 - s0) / (r3 - r4)) * (1 - r4)) * p) + ((1 - ((r3 - s0) / (r3 - r4))) * ((1 - r3) * p))) + ((1 - ((r3 - s0) / (r3 - r4))) * (r3 * q))) + (((r3 - s0) / (r3 - r4)) * (r4 * q))) by RLVECT_1:def 7;

              

              then (((1 - r5) * p3) + (r5 * p4)) = (((((((r3 - s0) / (r3 - r4)) * (1 - r4)) * p) + (((1 - ((r3 - s0) / (r3 - r4))) * (1 - r3)) * p)) + ((1 - ((r3 - s0) / (r3 - r4))) * (r3 * q))) + (((r3 - s0) / (r3 - r4)) * (r4 * q))) by RLVECT_1:def 7

              .= (((((((r3 - s0) / (r3 - r4)) * (1 - r4)) * p) + (((1 - ((r3 - s0) / (r3 - r4))) * (1 - r3)) * p)) + (((1 - ((r3 - s0) / (r3 - r4))) * r3) * q)) + (((r3 - s0) / (r3 - r4)) * (r4 * q))) by RLVECT_1:def 7;

              then (((1 - r5) * p3) + (r5 * p4)) = (((((((r3 - s0) / (r3 - r4)) * (1 - r4)) * p) + (((1 - ((r3 - s0) / (r3 - r4))) * (1 - r3)) * p)) + (((1 - ((r3 - s0) / (r3 - r4))) * r3) * q)) + ((((r3 - s0) / (r3 - r4)) * r4) * q)) by RLVECT_1:def 7;

              

              then (((1 - r5) * p3) + (r5 * p4)) = (((((((r3 - s0) / (r3 - r4)) * (1 - r4)) + ((1 - ((r3 - s0) / (r3 - r4))) * (1 - r3))) * p) + (((1 - ((r3 - s0) / (r3 - r4))) * r3) * q)) + ((((r3 - s0) / (r3 - r4)) * r4) * q)) by RLVECT_1:def 6

              .= ((((((r3 - s0) / (r3 - r4)) * (1 - r4)) + ((1 - ((r3 - s0) / (r3 - r4))) * (1 - r3))) * p) + ((((1 - ((r3 - s0) / (r3 - r4))) * r3) * q) + ((((r3 - s0) / (r3 - r4)) * r4) * q))) by RLVECT_1:def 3

              .= p0 by A12, A30, RLVECT_1:def 6;

              hence thesis by A27, A28, A29;

            end;

              suppose r4 = 1;

              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 thesis by A18, XCMPLX_1: 187;

            end;

          end;

          

           A31: p0 is_extremal_in (( LSeg (f,i)) \/ ( LSeg (f,(i + 1)))) by A1, A2, A3, Th36;

          assume

           A32: ( LSeg (p3,p4)) c= (( LSeg (f,i)) \/ ( LSeg (f,(i + 1))));

          per cases by A32, A24, A31;

            suppose

             A33: p0 = p3;

            now

              per cases ;

                suppose s0 = 1;

                

                then p0 = (( 0. ( TOP-REAL 2)) + (1 * q)) by A12, RLVECT_1: 10

                .= (1 * q) by RLVECT_1: 4

                .= q by RLVECT_1:def 8;

                hence contradiction by A6;

              end;

                suppose

                 A34: s0 <> 1;

                ( 0. ( TOP-REAL 2)) = ((((1 - s0) * p) + (s0 * q)) - (((1 - r3) * p) + (r3 * q))) by A12, A33, RLVECT_1: 5

                .= ((((1 - s0) * p) + (s0 * q)) + (( - ((1 - r3) * p)) - (r3 * q))) by RLVECT_1: 30

                .= (((((1 - s0) * p) + (s0 * q)) + ( - (r3 * q))) + ( - ((1 - r3) * p))) by RLVECT_1:def 3

                .= (( - ((1 - r3) * p)) + (((1 - s0) * p) + ((s0 * q) + ( - (r3 * q))))) by RLVECT_1:def 3

                .= ((( - ((1 - r3) * p)) + ((1 - s0) * p)) + ((s0 * q) + ( - (r3 * q)))) by RLVECT_1:def 3

                .= (((( - (1 - r3)) * p) + ((1 - s0) * p)) + ((s0 * q) + ( - (r3 * q)))) by RLVECT_1: 79

                .= (((( - (1 - r3)) + (1 - s0)) * p) + ((s0 * q) + ( - (r3 * q)))) by RLVECT_1:def 6

                .= (((( - (1 - r3)) + (1 - s0)) * p) + ((s0 * q) + (( - r3) * q))) by RLVECT_1: 79

                .= (((( - 1) * (s0 - r3)) * p) + ((s0 + ( - r3)) * q)) by RLVECT_1:def 6

                .= ((( - (s0 - r3)) * p) + ((s0 + ( - r3)) * q))

                .= (( - ((s0 - r3) * p)) + ((s0 + ( - r3)) * q)) by RLVECT_1: 79

                .= (((s0 - r3) * q) - ((s0 - r3) * p));

                

                then ((s0 - r3) * q) = ( - ( - ((s0 - r3) * p))) by RLVECT_1: 6

                .= ((s0 - r3) * p);

                then

                 A35: (s0 + ( - r3)) = 0 by A10, RLVECT_1: 36;

                1 > s0 by A14, A34, XXREAL_0: 1;

                hence contradiction by A23, A35, XXREAL_0: 21;

              end;

            end;

            hence contradiction;

          end;

            suppose

             A36: p0 = p4;

            now

              per cases ;

                suppose s0 = 0 ;

                

                then p0 = ((1 * p) + ( 0. ( TOP-REAL 2))) by A12, RLVECT_1: 10

                .= (1 * p) by RLVECT_1: 4

                .= p by RLVECT_1:def 8;

                hence contradiction by A7, A8, XBOOLE_0:def 3;

              end;

                suppose

                 A37: s0 <> 0 ;

                ( 0. ( TOP-REAL 2)) = ((((1 - s0) * p) + (s0 * q)) - (((1 - r4) * p) + (r4 * q))) by A12, A36, RLVECT_1: 5

                .= ((((1 - s0) * p) + (s0 * q)) + (( - ((1 - r4) * p)) - (r4 * q))) by RLVECT_1: 30

                .= (((((1 - s0) * p) + (s0 * q)) + ( - (r4 * q))) + ( - ((1 - r4) * p))) by RLVECT_1:def 3

                .= (( - ((1 - r4) * p)) + (((1 - s0) * p) + ((s0 * q) + ( - (r4 * q))))) by RLVECT_1:def 3

                .= ((( - ((1 - r4) * p)) + ((1 - s0) * p)) + ((s0 * q) + ( - (r4 * q)))) by RLVECT_1:def 3

                .= (((( - (1 - r4)) * p) + ((1 - s0) * p)) + ((s0 * q) + ( - (r4 * q)))) by RLVECT_1: 79

                .= (((( - (1 - r4)) + (1 - s0)) * p) + ((s0 * q) + ( - (r4 * q)))) by RLVECT_1:def 6

                .= (((( - (1 - r4)) + (1 - s0)) * p) + ((s0 * q) + (( - r4) * q))) by RLVECT_1: 79

                .= (((( - 1) * (s0 - r4)) * p) + ((s0 + ( - r4)) * q)) by RLVECT_1:def 6

                .= ((( - (s0 - r4)) * p) + ((s0 - r4) * q))

                .= (( - ((s0 - r4) * p)) + ((s0 - r4) * q)) by RLVECT_1: 79

                .= (( - ((s0 - r4) * p)) + ((s0 - r4) * q))

                .= (((s0 - r4) * q) + ( - ((s0 - r4) * p)))

                .= (((s0 - r4) * q) - ((s0 - r4) * p));

                

                then ((s0 - r4) * q) = ( - ( - ((s0 - r4) * p))) by RLVECT_1: 6

                .= ((s0 - r4) * p);

                then (s0 + ( - r4)) = 0 by A10, RLVECT_1: 36;

                hence contradiction by A13, A20, A37, XXREAL_0: 29;

              end;

            end;

            hence contradiction;

          end;

        end;

        then

         A38: ex x be object st x in ( LSeg (p3,p4)) & not x in (( LSeg (f,i)) \/ ( LSeg (f,(i + 1))));

        reconsider u4 = p4 as Point of ( Euclid 2) by EUCLID: 22;

        

         A39: |.(v2 - v1).| <> 0 by A10, EUCLID: 17;

        reconsider u3 = p3 as Point of ( Euclid 2) by EUCLID: 22;

        

         A40: r3 <= 1 by XXREAL_0: 22;

         0 <= r3 by A9, A13, XXREAL_0: 20;

        then p3 in ( LSeg (p,q)) by A40;

        then

         A41: ( LSeg (p3,p4)) c= ( LSeg (p,q)) by A22, TOPREAL1: 6;

        reconsider u0 = p0 as Point of ( Euclid 2) by EUCLID: 22;

        

         A42: (p4 - p0) = ((((1 - r4) * p) + (r4 * q)) + (( - ((1 - s0) * p)) - (s0 * q))) by A12, RLVECT_1: 30

        .= (((((1 - r4) * p) + (r4 * q)) + ( - ((1 - s0) * p))) + ( - (s0 * q))) by RLVECT_1:def 3

        .= (((r4 * q) + (((1 - r4) * p) + ( - ((1 - s0) * p)))) + ( - (s0 * q))) by RLVECT_1:def 3

        .= (((((1 - r4) * p) + ( - ((1 - s0) * p))) + (r4 * q)) + (( - s0) * q)) by RLVECT_1: 79

        .= (((((1 - r4) * p) + (( - (1 - s0)) * p)) + (r4 * q)) + (( - s0) * q)) by RLVECT_1: 79

        .= ((((1 - r4) * p) + (( - (1 - s0)) * p)) + ((r4 * q) + (( - s0) * q))) by RLVECT_1:def 3

        .= ((((1 - r4) * p) + (( - (1 - s0)) * p)) + ((r4 + ( - s0)) * q)) by RLVECT_1:def 6

        .= ((((1 - r4) + ( - (1 - s0))) * p) + ((r4 - s0) * q)) by RLVECT_1:def 6

        .= ((( - (r4 - s0)) * p) + ((r4 - s0) * q))

        .= (((r4 - s0) * q) - ((r4 - s0) * p)) by RLVECT_1: 79

        .= ((r4 - s0) * (q - p)) by RLVECT_1: 34

        .= ((r4 - s0) * (v2 - v1));

        now

          per cases ;

            suppose (s0 + (( - r0) / |.(v2 - v1).|)) <= 0 ;

            then

             A43: r4 = 0 by XXREAL_0:def 10;

            r4 >= (s0 + (( - r0) / |.(v2 - v1).|)) by XXREAL_0: 25;

            then (r4 + ( - s0)) >= ((s0 + (( - r0) / |.(v2 - v1).|)) + ( - s0)) by XREAL_1: 6;

            then

             A44: ( - (r4 - s0)) <= ( - (( - r0) / |.(v2 - v1).|)) by XREAL_1: 24;

            (r0 + r0) = s;

            then

             A45: r0 < s by A9, XREAL_1: 29;

            reconsider v3 = p4, v4 = p0 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

            .= |.(p4 - p0).|

            .= ( |.(r4 - s0).| * |.(v2 - v1).|) by A42, EUCLID: 11;

             |.(r4 - s0).| = |.( - (r4 - s0)).| by COMPLEX1: 52

            .= ( - ( 0 - s0)) by A13, A43, ABSVALUE:def 1;

            then ( |.(r4 - 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;

          end;

            suppose not (s0 + (( - r0) / |.(v2 - v1).|)) <= 0 ;

            

            then

             A48: (p4 - p0) = (((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 = p4, v4 = p0 as Element of ( REAL 2) by EUCLID: 22;

            

             A49: (r0 + r0) = s;

            ( dist (u4,u0)) = |.(v3 - v4).| by Th5

            .= |.(p4 - p0).|

            .= ( |.(( - r0) / |.(v2 - v1).|).| * |.(v2 - v1).|) by A48, EUCLID: 11

            .= (( |.( - r0).| / |. |.(v2 - v1).|.|) * |.(v2 - v1).|) by COMPLEX1: 67

            .= (( |.( - r0).| / |.(v2 - v1).|) * |.(v2 - v1).|) by ABSVALUE:def 1

            .= |.( - r0).| by A11, XCMPLX_1: 87

            .= |.r0.| by COMPLEX1: 52

            .= r0 by A9, ABSVALUE:def 1;

            hence ( dist (u4,u0)) < s by A9, A49, XREAL_1: 29;

          end;

        end;

        then u4 in { u7 where u7 be Point of ( Euclid 2) : ( dist (u0,u7)) < s };

        then

         A50: p4 in ( Ball (u0,s)) by METRIC_1: 17;

        

         A51: (p3 - p0) = ((((1 - r3) * p) + (r3 * q)) + (( - ((1 - s0) * p)) - (s0 * q))) by A12, RLVECT_1: 30

        .= (((((1 - r3) * p) + (r3 * q)) + ( - ((1 - s0) * p))) + ( - (s0 * q))) by RLVECT_1:def 3

        .= (((r3 * q) + (((1 - r3) * p) + ( - ((1 - s0) * p)))) + ( - (s0 * q))) by RLVECT_1:def 3

        .= (((((1 - r3) * p) + ( - ((1 - s0) * p))) + (r3 * q)) + (( - s0) * q)) by RLVECT_1: 79

        .= (((((1 - r3) * p) + (( - (1 - s0)) * p)) + (r3 * q)) + (( - s0) * q)) by RLVECT_1: 79

        .= ((((1 - r3) * p) + (( - (1 - s0)) * p)) + ((r3 * q) + (( - s0) * q))) by RLVECT_1:def 3

        .= ((((1 - r3) * p) + (( - (1 - s0)) * p)) + ((r3 + ( - s0)) * q)) by RLVECT_1:def 6

        .= ((((1 - r3) + ( - (1 - s0))) * p) + ((r3 - s0) * q)) by RLVECT_1:def 6

        .= ((( - (r3 - s0)) * p) + ((r3 - s0) * q))

        .= (((r3 - s0) * q) - ((r3 - s0) * p)) by RLVECT_1: 79

        .= ((r3 - s0) * (q - p)) by RLVECT_1: 34

        .= ((r3 - s0) * (v2 - v1));

        now

          per cases ;

            suppose

             A52: 1 <= (s0 + (r0 / |.(v2 - v1).|));

            r3 <= (s0 + (r0 / |.(v2 - v1).|)) by XXREAL_0: 17;

            then

             A53: (r3 + ( - s0)) <= ((s0 + (r0 / |.(v2 - v1).|)) + ( - s0)) by XREAL_1: 6;

            r3 = 1 by A52, XXREAL_0:def 9;

            then (r3 - s0) >= 0 by A14, XREAL_1: 48;

            then |.(r3 - s0).| <= (r0 / |.(v2 - v1).|) by A53, ABSVALUE:def 1;

            then

             A54: ( |.(r3 - s0).| * |.(v2 - v1).|) <= ((r0 / |.(v2 - v1).|) * |.(v2 - v1).|) by XREAL_1: 64;

            reconsider v3 = p3, v4 = p0 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

            .= |.(p3 - p0).|

            .= |.((r3 - s0) * (v2 - v1)).| by A51

            .= ( |.(r3 - 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;

          end;

            suppose not 1 <= (s0 + (r0 / |.(v2 - v1).|));

            

            then

             A56: (p3 - p0) = (((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 = p3, v4 = p0 as Element of ( REAL 2) by EUCLID: 22;

            

             A57: (r0 + r0) = s;

            ( dist (u3,u0)) = |.(v3 - v4).| by Th5

            .= |.(p3 - p0).|

            .= ( |.(r0 / |.(v2 - v1).|).| * |.(v2 - v1).|) by A56, EUCLID: 11

            .= (( |.r0.| / |. |.(v2 - v1).|.|) * |.(v2 - v1).|) by COMPLEX1: 67

            .= (( |.r0.| / |.(v2 - v1).|) * |.(v2 - v1).|) by ABSVALUE:def 1

            .= |.r0.| by A11, XCMPLX_1: 87

            .= r0 by A9, ABSVALUE:def 1;

            hence ( dist (u3,u0)) < s by A9, A57, XREAL_1: 29;

          end;

        end;

        then u3 in { u6 where u6 be Point of ( Euclid 2) : ( dist (u0,u6)) < s };

        then p3 in ( Ball (u0,s)) by METRIC_1: 17;

        then ( LSeg (p3,p4)) c= ( Ball (u0,s)) by A50, TOPREAL3: 21;

        hence thesis by A4, A38, A41;

      end;

    end;

    definition

      let f1, f2, P;

      :: SPPOL_1:def5

      pred f1,f2 are_generators_of P means f1 is alternating being_S-Seq & f2 is alternating 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

    theorem :: SPPOL_1:38

    (f1,f2) are_generators_of P & 1 < i & i < ( len f1) implies (f1 /. i) is_extremal_in P

    proof

      set p0 = (f1 /. i);

      set q1 = (f1 /. 1), q2 = (f1 /. ( len f1));

      set F1 = { ( LSeg (f1,k)) : 1 <= k & (k + 1) <= ( len f1) };

      set PP = ( union F1);

      reconsider u0 = p0 as Point of ( Euclid 2) by EUCLID: 22;

      reconsider F2 = { ( LSeg (f2,k)) : 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);

      set P2 = ( union F2);

      

       A4: (( L~ f1) /\ ( L~ f2)) = {q1, q2} by A1;

      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)) : 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 = (P1 \/ P2);

      

       A6: (j + 1) = i;

      then ( LSeg (f1,j)) = ( LSeg ((f1 /. j),p0)) by A3, A5, TOPREAL1:def 3;

      then

       A7: p0 in ( LSeg (f1,j)) by RLTOPSP1: 68;

      

       A8: P = (( L~ f1) \/ ( L~ f2)) by A1;

      

       A9: f1 is being_S-Seq by A1;

      then

       A10: f1 is one-to-one;

      

       A11: ( len f1) >= (1 + 1) by A9;

      

       A12: (i + 1) <= ( len f1) by A3, NAT_1: 13;

      then

       A13: ( LSeg (f1,i)) in F1 by A2;

      ( LSeg (f1,i)) = ( LSeg (p0,(f1 /. (i + 1)))) by A2, A12, TOPREAL1:def 3;

      then

       A14: p0 in ( LSeg (f1,i)) by RLTOPSP1: 68;

      then

       A15: p0 in ( L~ f1) by A13, TARSKI:def 4;

       not p0 in Q

      proof

        assume

         A16: p0 in Q;

        per cases by A16, XBOOLE_0:def 3;

          suppose

           A17: p0 in P1;

          

           A18: f1 is s.n.c. by A9;

          consider Z be set such that

           A19: p0 in Z and

           A20: Z in F by A17, TARSKI:def 4;

          consider k 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

            per cases by A24, XREAL_1: 50;

              suppose (j - k) > 0 ;

              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;

              then (( LSeg (f1,k)) /\ ( LSeg (f1,i))) = {} by XBOOLE_0:def 7;

              hence contradiction by A14, A19, A21, XBOOLE_0:def 4;

            end;

              suppose (k - i) > 0 ;

              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;

              then (( LSeg (f1,j)) /\ ( LSeg (f1,k))) = {} by XBOOLE_0:def 7;

              hence contradiction by A7, A19, A21, XBOOLE_0:def 4;

            end;

          end;

          hence contradiction;

        end;

          suppose

           A25: p0 in P2;

          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;

          p0 in {q1, q2} by A4, A15, A25, XBOOLE_0:def 4;

          then p0 = q1 or p0 = q2 by TARSKI:def 2;

          hence contradiction by A2, A3, A10, A26, A28, A27, PARTFUN2: 10;

        end;

      end;

      then

       A29: u0 in (Q ` ) by SUBSET_1: 29;

      

       A30: f1 is alternating by A1;

      

       A31: the TopStruct of ( TOP-REAL 2) = ( TopSpaceMetr ( Euclid 2)) by EUCLID:def 8;

      then

      reconsider QQ = (Q ` ) as Subset of ( TopSpaceMetr ( Euclid 2));

      

       A32: f1 is special by A9;

      P1 is closed & P2 is closed by Lm4, Th26;

      then Q is closed by TOPS_1: 9;

      then (Q ` ) is open by TOPS_1: 3;

      then QQ is open by A31, PRE_TOPC: 30;

      then

      consider r0 be Real such that

       A33: r0 > 0 and

       A34: ( Ball (u0,r0)) c= (Q ` ) by A29, TOPMETR: 15;

      reconsider r0 as Real;

      

       A35: (j + 2) <= ( len f1) by A12;

      now

        let y be object;

        hereby

          assume y in ((P1 \/ ( LSeg (f1,j))) \/ ( LSeg (f1,i)));

          then

           A36: y in (P1 \/ ( LSeg (f1,j))) or y in ( LSeg (f1,i)) by XBOOLE_0:def 3;

          per cases by A36, XBOOLE_0:def 3;

            suppose y in P1;

            then

            consider Z3 be set such that

             A37: y in Z3 and

             A38: Z3 in F by TARSKI:def 4;

            ex k st ( LSeg (f1,k)) = Z3 & 1 <= k & (k + 1) <= ( len f1) & not k = (i - 1) & not k = i by A38;

            then Z3 in F1;

            hence y in PP by A37, TARSKI:def 4;

          end;

            suppose

             A39: y in ( LSeg (f1,j));

            ( LSeg (f1,j)) in F1 by A3, A6, A5;

            hence y in PP by A39, TARSKI:def 4;

          end;

            suppose y in ( LSeg (f1,i));

            hence y in PP by A13, TARSKI:def 4;

          end;

        end;

        assume y in PP;

        then

        consider Z2 be set such that

         A40: y in Z2 and

         A41: Z2 in F1 by TARSKI:def 4;

        consider k such that

         A42: ( LSeg (f1,k)) = Z2 and

         A43: 1 <= k & (k + 1) <= ( len f1) by A41;

        per cases ;

          suppose

           A44: k = (i - 1) or k = i;

          now

            per cases by A44;

              suppose k = (i - 1);

              then y in (( LSeg (f1,j)) \/ ( LSeg (f1,i))) by A40, A42, XBOOLE_0:def 3;

              then y in (P1 \/ (( LSeg (f1,j)) \/ ( LSeg (f1,i)))) by XBOOLE_0:def 3;

              hence y in ((P1 \/ ( LSeg (f1,j))) \/ ( LSeg (f1,i))) by XBOOLE_1: 4;

            end;

              suppose k = i;

              hence y in ((P1 \/ ( LSeg (f1,j))) \/ ( LSeg (f1,i))) by A40, A42, XBOOLE_0:def 3;

            end;

          end;

          hence y in ((P1 \/ ( LSeg (f1,j))) \/ ( LSeg (f1,i)));

        end;

          suppose k <> (i - 1) & k <> i;

          then Z2 in F by A42, A43;

          then y in P1 by A40, TARSKI:def 4;

          then y in (P1 \/ (( LSeg (f1,j)) \/ ( LSeg (f1,i)))) by XBOOLE_0:def 3;

          hence y in ((P1 \/ ( LSeg (f1,j))) \/ ( LSeg (f1,i))) by XBOOLE_1: 4;

        end;

      end;

      then

       A45: ((P1 \/ ( LSeg (f1,j))) \/ ( LSeg (f1,i))) = PP by TARSKI: 2;

       A46:

      now

        let p, q;

        assume that

         A47: p0 in ( LSeg (p,q)) and

         A48: ( LSeg (p,q)) c= P;

        per cases ;

          suppose

           A49: ( LSeg (p,q)) c= (( LSeg (f1,j)) \/ ( LSeg (f1,i)));

          p0 is_extremal_in (( LSeg (f1,j)) \/ ( LSeg (f1,i))) by A30, A6, A5, A35, A32, Th36;

          hence p0 = p or p0 = q by A47, A49;

        end;

          suppose not ( LSeg (p,q)) c= (( LSeg (f1,j)) \/ ( LSeg (f1,i)));

          then

          consider x be object such that

           A50: x in ( LSeg (p,q)) and

           A51: not x in (( LSeg (f1,j)) \/ ( LSeg (f1,i)));

          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

            per cases by A47, A52, XBOOLE_0:def 3;

              suppose

               A53: p0 in ( LSeg (p,p8));

              now

                assume (f1 /. i) <> p;

                then

                consider q3 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 Q by A34, A56, XBOOLE_0:def 5;

                then not q3 in P1 by XBOOLE_0:def 3;

                then not q3 in (P1 \/ (( LSeg (f1,j)) \/ ( LSeg (f1,i)))) by A54, XBOOLE_0:def 3;

                then

                 A58: not q3 in PP 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;

                 not q3 in ( L~ f2) by A57, XBOOLE_0:def 3;

                hence contradiction by A8, A55, A58, A59, XBOOLE_0:def 3;

              end;

              hence p0 = p or p0 = q;

            end;

              suppose

               A60: p0 in ( LSeg (p8,q));

              now

                assume (f1 /. i) <> q;

                then

                consider q3 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 Q by A34, A63, XBOOLE_0:def 5;

                then not q3 in P1 by XBOOLE_0:def 3;

                then not q3 in (P1 \/ (( LSeg (f1,j)) \/ ( LSeg (f1,i)))) by A61, XBOOLE_0:def 3;

                then

                 A65: not q3 in PP 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;

                 not q3 in ( L~ f2) by A64, XBOOLE_0:def 3;

                hence contradiction by A8, A62, A65, A66, XBOOLE_0:def 3;

              end;

              hence p0 = p or p0 = q;

            end;

          end;

          hence p0 = p or p0 = q;

        end;

      end;

      p0 in PP by A14, A13, TARSKI:def 4;

      then p0 in P by A8, XBOOLE_0:def 3;

      hence thesis by A46;

    end;

    theorem :: SPPOL_1:39

    for p,q be Point of ( TOP-REAL n), p9,q9 be 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 be 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);

      assume ( LSeg (p,q)) is horizontal;

      then

       A1: (p `2 ) = (q `2 ) by Th15;

      assume r in ( LSeg (p,q));

      then

      consider t be 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;

    end;

    theorem :: SPPOL_1:41

    for p,q,r be 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);

      assume ( LSeg (p,q)) is vertical;

      then

       A1: (p `1 ) = (q `1 ) by Th16;

      assume r in ( LSeg (p,q));

      then

      consider t be 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;

    end;

    registration

      cluster compact non empty horizontal for Subset of ( TOP-REAL 2);

      existence

      proof

        take ( LSeg ( |[ 0 , 0 ]|, |[1, 0 ]|));

        ( |[ 0 , 0 ]| `2 ) = 0 & ( |[1, 0 ]| `2 ) = 0 by EUCLID: 52;

        hence thesis by Th15;

      end;

      cluster compact non empty vertical for Subset of ( TOP-REAL 2);

      existence

      proof

        take ( LSeg ( |[ 0 , 0 ]|, |[ 0 , 1]|));

        ( |[ 0 , 0 ]| `1 ) = 0 & ( |[ 0 , 1]| `1 ) = 0 by EUCLID: 52;

        hence thesis by Th16;

      end;

    end