rltopsp1.miz



    begin

    reserve r,s,t,u for Real;

    theorem :: RLTOPSP1:1

    for X be non empty RLSStruct, M be Subset of X, x be Point of X, r be Real st x in M holds (r * x) in (r * M);

    reconsider jj = 1 as positive Real;

    registration

      cluster non zero for Real;

      existence

      proof

        take jj;

        thus thesis;

      end;

    end

    theorem :: RLTOPSP1:2

    

     Th2: for T be non empty TopSpace, X be non empty Subset of T, FX be Subset-Family of T st FX is Cover of X holds for x be Point of T st x in X holds ex W be Subset of T st x in W & W in FX

    proof

      let T be non empty TopSpace, X be non empty Subset of T, FX be Subset-Family of T;

      assume FX is Cover of X;

      then

       A1: X c= ( union FX) by SETFAM_1:def 11;

      let x be Point of T;

      assume x in X;

      then

      consider W be set such that

       A2: x in W and

       A3: W in FX by A1, TARSKI:def 4;

      reconsider W as Subset of T by A3;

      take W;

      thus thesis by A2, A3;

    end;

    theorem :: RLTOPSP1:3

    

     Th3: for X be non empty addLoopStr, M,N be Subset of X, x,y be Point of X st x in M & y in N holds (x + y) in (M + N)

    proof

      let X be non empty addLoopStr, M,N be Subset of X, x,y be Point of X;

      (M + N) = { (u + v) where u,v be Point of X : u in M & v in N } by RUSUB_4:def 9;

      hence thesis;

    end;

    

     Lm1: for X be non empty addLoopStr, M be Subset of X, x,y be Point of X st y in M holds (x + y) in (x + M)

    proof

      let X be non empty addLoopStr, M be Subset of X, x,y be Point of X;

      (x + M) = { (x + u) where u be Point of X : u in M } by RUSUB_4:def 8;

      hence thesis;

    end;

    

     Lm2: for X be non empty addLoopStr, M,N be Subset of X holds { (x + N) where x be Point of X : x in M } is Subset-Family of X

    proof

      let X be non empty addLoopStr, M,N be Subset of X;

      set F = { (u + N) where u be Point of X : u in M };

      F c= ( bool the carrier of X)

      proof

        let x be object;

        assume x in F;

        then ex u be Point of X st x = (u + N) & u in M;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: RLTOPSP1:4

    

     Th4: for X be non empty addLoopStr, M,N be Subset of X, F be Subset-Family of X st F = { (x + N) where x be Point of X : x in M } holds (M + N) = ( union F)

    proof

      let X be non empty addLoopStr, M,N be Subset of X, F be Subset-Family of X;

      assume

       A1: F = { (x + N) where x be Point of X : x in M };

      thus (M + N) c= ( union F)

      proof

        let x be object;

        assume x in (M + N);

        then x in { (u + v) where u,v be Point of X : u in M & v in N } by RUSUB_4:def 9;

        then

        consider u,v be Point of X such that

         A2: x = (u + v) and

         A3: u in M and

         A4: v in N;

        (u + N) = { (u + v9) where v9 be Point of X : v9 in N } by RUSUB_4:def 8;

        then

         A5: x in (u + N) by A2, A4;

        (u + N) in F by A1, A3;

        hence thesis by A5, TARSKI:def 4;

      end;

      let x be object;

      assume x in ( union F);

      then

      consider Y be set such that

       A6: x in Y and

       A7: Y in F by TARSKI:def 4;

      consider u be Point of X such that

       A8: Y = (u + N) and

       A9: u in M by A1, A7;

      (u + N) = { (u + v) where v be Point of X : v in N } by RUSUB_4:def 8;

      then ex v be Point of X st x = (u + v) & v in N by A6, A8;

      then x in { (u9 + v9) where u9,v9 be Point of X : u9 in M & v9 in N } by A9;

      hence thesis by RUSUB_4:def 9;

    end;

    theorem :: RLTOPSP1:5

    

     Th5: for X be add-associative right_zeroed right_complementable non empty addLoopStr, M be Subset of X holds (( 0. X) + M) = M

    proof

      let X be add-associative right_zeroed right_complementable non empty addLoopStr, M be Subset of X;

      

       A1: (( 0. X) + M) = { (( 0. X) + u) where u be Point of X : u in M } by RUSUB_4:def 8;

      thus (( 0. X) + M) c= M

      proof

        let x be object;

        assume x in (( 0. X) + M);

        then ex u be Point of X st x = (( 0. X) + u) & u in M by A1;

        hence thesis;

      end;

      let x be object;

      assume

       A2: x in M;

      then

      reconsider x as Point of X;

      (( 0. X) + x) = x;

      hence thesis by A1, A2;

    end;

    theorem :: RLTOPSP1:6

    

     Th6: for X be add-associative non empty addLoopStr, x,y be Point of X, M be Subset of X holds ((x + y) + M) = (x + (y + M))

    proof

      let X be add-associative non empty addLoopStr, x,y be Point of X, M be Subset of X;

      

       A1: (x + (y + M)) = { (x + u) where u be Point of X : u in (y + M) } by RUSUB_4:def 8;

      

       A2: (y + M) = { (y + u) where u be Point of X : u in M } by RUSUB_4:def 8;

      

       A3: ((x + y) + M) = { ((x + y) + u) where u be Point of X : u in M } by RUSUB_4:def 8;

      thus ((x + y) + M) c= (x + (y + M))

      proof

        let z be object;

        assume z in ((x + y) + M);

        then

        consider u be Point of X such that

         A4: ((x + y) + u) = z & u in M by A3;

        (x + (y + u)) = z & (y + u) in (y + M) by A2, A4, RLVECT_1:def 3;

        hence thesis by A1;

      end;

      let z be object;

      assume z in (x + (y + M));

      then

      consider u be Point of X such that

       A5: (x + u) = z and

       A6: u in (y + M) by A1;

      consider v be Point of X such that

       A7: (y + v) = u and

       A8: v in M by A2, A6;

      ((x + y) + v) = z by A5, A7, RLVECT_1:def 3;

      hence thesis by A3, A8;

    end;

    theorem :: RLTOPSP1:7

    

     Th7: for X be add-associative non empty addLoopStr, x be Point of X, M,N be Subset of X holds ((x + M) + N) = (x + (M + N))

    proof

      let X be add-associative non empty addLoopStr, x be Point of X, M,N be Subset of X;

      

       A1: (x + (M + N)) = { (x + u) where u be Point of X : u in (M + N) } by RUSUB_4:def 8;

      

       A2: (x + M) = { (x + u) where u be Point of X : u in M } by RUSUB_4:def 8;

      

       A3: (M + N) = { (u + v) where u,v be Point of X : u in M & v in N } by RUSUB_4:def 9;

      

       A4: ((x + M) + N) = { (u + v) where u,v be Point of X : u in (x + M) & v in N } by RUSUB_4:def 9;

      thus ((x + M) + N) c= (x + (M + N))

      proof

        let z be object;

        assume z in ((x + M) + N);

        then

        consider u,v be Point of X such that

         A5: (u + v) = z and

         A6: u in (x + M) and

         A7: v in N by A4;

        consider u9 be Point of X such that

         A8: (x + u9) = u & u9 in M by A2, A6;

        (x + (u9 + v)) = z & (u9 + v) in (M + N) by A3, A5, A7, A8, RLVECT_1:def 3;

        hence thesis by A1;

      end;

      let z be object;

      assume z in (x + (M + N));

      then

      consider u be Point of X such that

       A9: (x + u) = z and

       A10: u in (M + N) by A1;

      consider w,v be Point of X such that

       A11: (w + v) = u and

       A12: w in M and

       A13: v in N by A3, A10;

      

       A14: (x + w) in (x + M) by A2, A12;

      ((x + w) + v) = z by A9, A11, RLVECT_1:def 3;

      hence thesis by A4, A13, A14;

    end;

    theorem :: RLTOPSP1:8

    

     Th8: for X be non empty addLoopStr, M,N be Subset of X, x be Point of X st M c= N holds (x + M) c= (x + N)

    proof

      let X be non empty addLoopStr, M,N be Subset of X, x be Point of X such that

       A1: M c= N;

      let z be object;

      assume

       A2: z in (x + M);

      then

      reconsider z as Point of X;

      (x + M) = { (x + u) where u be Element of X : u in M } by RUSUB_4:def 8;

      then ex u be Point of X st (x + u) = z & u in M by A2;

      hence thesis by A1, Lm1;

    end;

    theorem :: RLTOPSP1:9

    

     Th9: for X be add-associative right_zeroed right_complementable non empty addLoopStr, M be Subset of X, x be Point of X st x in M holds ( 0. X) in (( - x) + M)

    proof

      let X be add-associative right_zeroed right_complementable non empty addLoopStr, M be Subset of X, x be Point of X;

      assume x in M;

      then (( - x) + x) in (( - x) + M) by Lm1;

      hence thesis by RLVECT_1: 5;

    end;

    theorem :: RLTOPSP1:10

    

     Th10: for X be non empty addLoopStr, M,N,V be Subset of X st M c= N holds (M + V) c= (N + V)

    proof

      let X be non empty addLoopStr, M,N,V be Subset of X such that

       A1: M c= N;

      let x be object;

      assume x in (M + V);

      then x in { (u + v) where u,v be Point of X : u in M & v in V } by RUSUB_4:def 9;

      then ex u,v be Point of X st (u + v) = x & u in M & v in V;

      then x in { (u9 + v9) where u9,v9 be Point of X : u9 in N & v9 in V } by A1;

      hence thesis by RUSUB_4:def 9;

    end;

    

     Lm3: for X be non empty addLoopStr, M,N,V be Subset of X st M c= N holds (V + M) c= (V + N)

    proof

      let X be non empty addLoopStr, M,N,V be Subset of X such that

       A1: M c= N;

      let x be object;

      assume x in (V + M);

      then x in { (u + v) where u,v be Point of X : u in V & v in M } by RUSUB_4:def 9;

      then ex u,v be Point of X st (u + v) = x & u in V & v in M;

      then x in { (u9 + v9) where u9,v9 be Point of X : u9 in V & v9 in N } by A1;

      hence thesis by RUSUB_4:def 9;

    end;

    theorem :: RLTOPSP1:11

    

     Th11: for X be non empty addLoopStr, V1,V2,W1,W2 be Subset of X st V1 c= W1 & V2 c= W2 holds (V1 + V2) c= (W1 + W2)

    proof

      let X be non empty addLoopStr, V1,V2,W1,W2 be Subset of X such that

       A1: V1 c= W1 & V2 c= W2;

      let x be object;

      assume x in (V1 + V2);

      then x in { (u + v) where u,v be Point of X : u in V1 & v in V2 } by RUSUB_4:def 9;

      then ex u,v be Point of X st (u + v) = x & u in V1 & v in V2;

      then x in { (u9 + v9) where u9,v9 be Point of X : u9 in W1 & v9 in W2 } by A1;

      hence thesis by RUSUB_4:def 9;

    end;

    theorem :: RLTOPSP1:12

    

     Th12: for X be right_zeroed non empty addLoopStr, V1,V2 be Subset of X st ( 0. X) in V2 holds V1 c= (V1 + V2)

    proof

      let X be right_zeroed non empty addLoopStr, V1,V2 be Subset of X such that

       A1: ( 0. X) in V2;

      let x be object;

      assume

       A2: x in V1;

      then

      reconsider x as Point of X;

      (x + ( 0. X)) = x by RLVECT_1:def 4;

      then x in { (u + v) where u,v be Point of X : u in V1 & v in V2 } by A1, A2;

      hence thesis by RUSUB_4:def 9;

    end;

    theorem :: RLTOPSP1:13

    

     Th13: for X be RealLinearSpace, r be Real holds (r * {( 0. X)}) = {( 0. X)}

    proof

      let X be RealLinearSpace, r be Real;

      thus (r * {( 0. X)}) c= {( 0. X)}

      proof

        let x be object;

        assume

         A1: x in (r * {( 0. X)});

        then

        reconsider x as Point of X;

        consider v be Point of X such that

         A2: x = (r * v) and

         A3: v in {( 0. X)} by A1;

        v = ( 0. X) by A3, TARSKI:def 1;

        then (r * v) = ( 0. X);

        hence thesis by A2, TARSKI:def 1;

      end;

      ( 0. X) in {( 0. X)} by TARSKI:def 1;

      then (r * ( 0. X)) in (r * {( 0. X)});

      then ( 0. X) in (r * {( 0. X)});

      hence thesis by ZFMISC_1: 31;

    end;

    theorem :: RLTOPSP1:14

    for X be RealLinearSpace, M be Subset of X, r be non zero Real st ( 0. X) in (r * M) holds ( 0. X) in M

    proof

      let X be RealLinearSpace, M be Subset of X, r be non zero Real;

      assume ( 0. X) in (r * M);

      then

       A1: ex v be Point of X st (r * v) = ( 0. X) & v in M;

      (r * ( 0. X)) = ( 0. X);

      hence thesis by A1, RLVECT_1: 36;

    end;

    theorem :: RLTOPSP1:15

    

     Th15: for X be RealLinearSpace, M,N be Subset of X, r be non zero Real holds ((r * M) /\ (r * N)) = (r * (M /\ N))

    proof

      let X be RealLinearSpace, M,N be Subset of X, r be non zero Real;

      thus for x be object st x in ((r * M) /\ (r * N)) holds x in (r * (M /\ N))

      proof

        let x be object;

        assume

         A1: x in ((r * M) /\ (r * N));

        then x in (r * M) by XBOOLE_0:def 4;

        then

        consider v1 be Point of X such that

         A2: (r * v1) = x and

         A3: v1 in M;

        x in (r * N) by A1, XBOOLE_0:def 4;

        then

        consider v2 be Point of X such that

         A4: (r * v2) = x and

         A5: v2 in N;

        v1 = v2 by A2, A4, RLVECT_1: 36;

        then v1 in (M /\ N) by A3, A5, XBOOLE_0:def 4;

        hence thesis by A2;

      end;

      let x be object;

      assume x in (r * (M /\ N));

      then

      consider v be Point of X such that

       A6: (r * v) = x and

       A7: v in (M /\ N);

      v in N by A7, XBOOLE_0:def 4;

      then

       A8: x in (r * N) by A6;

      v in M by A7, XBOOLE_0:def 4;

      then x in (r * M) by A6;

      hence thesis by A8, XBOOLE_0:def 4;

    end;

    theorem :: RLTOPSP1:16

    for X be non empty TopSpace, x be Point of X, A be a_neighborhood of x, B be Subset of X st A c= B holds B is a_neighborhood of x

    proof

      let X be non empty TopSpace, x be Point of X, A be a_neighborhood of x, B be Subset of X;

      assume A c= B;

      then x in ( Int A) & ( Int A) c= ( Int B) by CONNSP_2:def 1, TOPS_1: 19;

      hence thesis by CONNSP_2:def 1;

    end;

    definition

      let V be RealLinearSpace, M be Subset of V;

      :: original: convex

      redefine

      :: RLTOPSP1:def1

      attr M is convex means

      : Def1: for u,v be Point of V, r be Real st 0 <= r & r <= 1 & u in M & v in M holds ((r * u) + ((1 - r) * v)) in M;

      compatibility

      proof

        hereby

          assume

           A1: M is convex;

          let u,v be Point of V, r be Real such that

           A2: 0 <= r & r <= 1 and

           A3: u in M and

           A4: v in M;

          per cases by A2, XXREAL_0: 1;

            suppose 0 < r & r < 1;

            hence ((r * u) + ((1 - r) * v)) in M by A1, A3, A4;

          end;

            suppose 0 = r;

            then (r * u) = ( 0. V) & ((1 - r) * v) = v by RLVECT_1: 10, RLVECT_1:def 8;

            hence ((r * u) + ((1 - r) * v)) in M by A4;

          end;

            suppose r = 1;

            then ((1 - r) * v) = ( 0. V) & (r * u) = u by RLVECT_1: 10, RLVECT_1:def 8;

            hence ((r * u) + ((1 - r) * v)) in M by A3;

          end;

        end;

        assume

         A5: for u,v be Point of V, r be Real st 0 <= r & r <= 1 & u in M & v in M holds ((r * u) + ((1 - r) * v)) in M;

        let u,v be Point of V, r be Real;

        thus thesis by A5;

      end;

    end

    

     Lm4: for X be RealLinearSpace holds ( conv ( {} X)) = {}

    proof

      let X be RealLinearSpace;

      ( {} X) is convex;

      then ( {} X) in ( Convex-Family ( {} X)) by CONVEX1:def 4;

      hence thesis by SETFAM_1: 4;

    end;

    registration

      let X be RealLinearSpace, M be empty Subset of X;

      cluster ( conv M) -> empty;

      coherence

      proof

        M = ( {} X);

        hence thesis by Lm4;

      end;

    end

    theorem :: RLTOPSP1:17

    for X be RealLinearSpace, M be convex Subset of X holds ( conv M) = M by CONVEX1: 30, CONVEX1: 41;

    theorem :: RLTOPSP1:18

    

     Th18: for X be RealLinearSpace, M be Subset of X, r be Real holds (r * ( conv M)) = ( conv (r * M))

    proof

      let X be RealLinearSpace, M be Subset of X, r be Real;

      thus (r * ( conv M)) c= ( conv (r * M))

      proof

        let x be object;

        per cases ;

          suppose

           A1: r = 0 ;

          per cases ;

            suppose M = {} ;

            hence thesis by CONVEX1: 33;

          end;

            suppose

             A2: M <> {} ;

            then (r * M) = {( 0. X)} by A1, CONVEX1: 34;

            then

             A3: {( 0. X)} c= ( conv (r * M)) by CONVEX1: 41;

            ( conv M) <> {} by A2, CONVEX1: 41, XBOOLE_1: 3;

            then (r * ( conv M)) = {( 0. X)} by A1, CONVEX1: 34;

            hence thesis by A3;

          end;

        end;

          suppose

           A4: r <> 0 ;

          assume x in (r * ( conv M));

          then

          consider v be Point of X such that

           A5: x = (r * v) and

           A6: v in ( conv M);

          for V be set st V in ( Convex-Family (r * M)) holds (r * v) in V

          proof

            let V be set;

            assume

             A7: V in ( Convex-Family (r * M));

            then

            reconsider V as Subset of X;

            (r * M) c= V by A7, CONVEX1:def 4;

            then ((r " ) * (r * M)) c= ((r " ) * V) by CONVEX1: 39;

            then (((r " ) * r) * M) c= ((r " ) * V) by CONVEX1: 37;

            then (1 * M) c= ((r " ) * V) by A4, XCMPLX_0:def 7;

            then

             A8: M c= ((r " ) * V) by CONVEX1: 32;

            V is convex by A7, CONVEX1:def 4;

            then ((r " ) * V) is convex by CONVEX1: 1;

            then ((r " ) * V) in ( Convex-Family M) by A8, CONVEX1:def 4;

            then v in ((r " ) * V) by A6, SETFAM_1:def 1;

            then

            consider w be Point of X such that

             A9: v = ((r " ) * w) and

             A10: w in V;

            (r * v) = ((r * (r " )) * w) by A9, RLVECT_1:def 7

            .= (1 * w) by A4, XCMPLX_0:def 7

            .= w by RLVECT_1:def 8;

            hence thesis by A10;

          end;

          hence thesis by A5, SETFAM_1:def 1;

        end;

      end;

      (r * M) c= (r * ( conv M)) & (r * ( conv M)) is convex by CONVEX1: 1, CONVEX1: 39, CONVEX1: 41;

      hence thesis by CONVEX1: 30;

    end;

    theorem :: RLTOPSP1:19

    

     Th19: for X be RealLinearSpace, M1,M2 be Subset of X st M1 c= M2 holds ( Convex-Family M2) c= ( Convex-Family M1)

    proof

      let X be RealLinearSpace, M1,M2 be Subset of X such that

       A1: M1 c= M2;

      let M be object;

      assume

       A2: M in ( Convex-Family M2);

      then

      reconsider M as Subset of X;

      M2 c= M by A2, CONVEX1:def 4;

      then

       A3: M1 c= M by A1;

      M is convex by A2, CONVEX1:def 4;

      hence thesis by A3, CONVEX1:def 4;

    end;

    theorem :: RLTOPSP1:20

    

     Th20: for X be RealLinearSpace, M1,M2 be Subset of X st M1 c= M2 holds ( conv M1) c= ( conv M2)

    proof

      let X be RealLinearSpace, M1,M2 be Subset of X;

      assume M1 c= M2;

      then ( Convex-Family M2) c= ( Convex-Family M1) by Th19;

      then

       A1: ( meet ( Convex-Family M1)) c= ( meet ( Convex-Family M2)) by SETFAM_1: 6;

      let x be object;

      assume x in ( conv M1);

      hence thesis by A1;

    end;

    theorem :: RLTOPSP1:21

    for X be RealLinearSpace, M be convex Subset of X, r be Real st 0 <= r & r <= 1 & ( 0. X) in M holds (r * M) c= M

    proof

      let X be RealLinearSpace, M be convex Subset of X, r be Real such that

       A1: 0 <= r & r <= 1 & ( 0. X) in M;

      let x be object;

      assume x in (r * M);

      then

      consider v be Point of X such that

       A2: (r * v) = x and

       A3: v in M;

      ((r * v) + ((1 - r) * ( 0. X))) in M by A1, A3, Def1;

      then ((r * v) + ( 0. X)) in M;

      hence thesis by A2;

    end;

    definition

      let X be RealLinearSpace, v,w be Point of X;

      :: RLTOPSP1:def2

      func LSeg (v,w) -> Subset of X equals { (((1 - r) * v) + (r * w)) : 0 <= r & r <= 1 };

      coherence

      proof

        { (((1 - r) * v) + (r * w)) : 0 <= r & r <= 1 } c= the carrier of X

        proof

          let x be object;

          assume x in { (((1 - r) * v) + (r * w)) : 0 <= r & r <= 1 };

          then ex r st x = (((1 - r) * v) + (r * w)) & 0 <= r & r <= 1;

          hence thesis;

        end;

        hence thesis;

      end;

      commutativity

      proof

        let A be Subset of X, v,w be Point of X;

        assume

         A1: A = { (((1 - r) * v) + (r * w)) : 0 <= r & r <= 1 };

        thus A c= { (((1 - r) * w) + (r * v)) : 0 <= r & r <= 1 }

        proof

          let x be object;

          assume x in A;

          then

          consider r such that

           A2: x = (((1 - r) * v) + (r * w)) and

           A3: 0 <= r & r <= 1 by A1;

          

           A4: (1 - (1 - r)) = r;

           0 <= (1 - r) & (1 - r) <= (1 - 0 ) by A3, XREAL_1: 10, XREAL_1: 48;

          hence thesis by A2, A4;

        end;

        let x be object;

        assume x in { (((1 - r) * w) + (r * v)) : 0 <= r & r <= 1 };

        then

        consider r such that

         A5: x = (((1 - r) * w) + (r * v)) and

         A6: 0 <= r & r <= 1;

        

         A7: (1 - (1 - r)) = r;

         0 <= (1 - r) & (1 - r) <= (1 - 0 ) by A6, XREAL_1: 10, XREAL_1: 48;

        hence thesis by A1, A5, A7;

      end;

    end

    registration

      let X be RealLinearSpace, v,w be Point of X;

      cluster ( LSeg (v,w)) -> non empty convex;

      coherence

      proof

        

         A1: ( 0 * w) = ( 0. X) & (v + ( 0. X)) = v by RLVECT_1: 10;

        (1 - 0 ) = 1 & (1 * v) = v by RLVECT_1:def 8;

        then v in ( LSeg (v,w)) by A1;

        hence ( LSeg (v,w)) is non empty;

        let u,u9 be Point of X, r be Real;

        assume that

         A2: 0 <= r and

         A3: r <= 1;

        

         A4: 0 <= (1 - r) by A3, XREAL_1: 48;

        assume u in ( LSeg (v,w));

        then

        consider s be Real such that

         A5: u = (((1 - s) * v) + (s * w)) and

         A6: 0 <= s and

         A7: s <= 1;

        

         A8: (r * u) = ((r * ((1 - s) * v)) + (r * (s * w))) by A5, RLVECT_1:def 5

        .= (((r * (1 - s)) * v) + (r * (s * w))) by RLVECT_1:def 7

        .= (((r * (1 - s)) * v) + ((r * s) * w)) by RLVECT_1:def 7;

        assume u9 in ( LSeg (v,w));

        then

        consider t be Real such that

         A9: u9 = (((1 - t) * v) + (t * w)) and

         A10: 0 <= t and

         A11: t <= 1;

        ((1 - r) * u9) = (((1 - r) * ((1 - t) * v)) + ((1 - r) * (t * w))) by A9, RLVECT_1:def 5

        .= ((((1 - r) * (1 - t)) * v) + ((1 - r) * (t * w))) by RLVECT_1:def 7

        .= ((((1 - r) * (1 - t)) * v) + (((1 - r) * t) * w)) by RLVECT_1:def 7;

        

        then

         A12: ((r * u) + ((1 - r) * u9)) = (((r * (1 - s)) * v) + (((r * s) * w) + ((((1 - r) * (1 - t)) * v) + (((1 - r) * t) * w)))) by A8, RLVECT_1:def 3

        .= (((r * (1 - s)) * v) + ((((1 - r) * (1 - t)) * v) + (((r * s) * w) + (((1 - r) * t) * w)))) by RLVECT_1:def 3

        .= ((((r * (1 - s)) * v) + (((1 - r) * (1 - t)) * v)) + (((r * s) * w) + (((1 - r) * t) * w))) by RLVECT_1:def 3

        .= ((((r * (1 - s)) + ((1 - r) * (1 - t))) * v) + (((r * s) * w) + (((1 - r) * t) * w))) by RLVECT_1:def 6

        .= (((1 - ((r * s) + ((1 - r) * t))) * v) + (((r * s) + ((1 - r) * t)) * w)) by RLVECT_1:def 6;

        (((1 - r) * t) + (r * s)) <= 1 by A2, A3, A7, A11, XREAL_1: 174;

        hence thesis by A2, A6, A10, A12, A4;

      end;

    end

    theorem :: RLTOPSP1:22

    for X be RealLinearSpace, M be Subset of X holds M is convex iff for u,w be Point of X st u in M & w in M holds ( LSeg (u,w)) c= M

    proof

      let X be RealLinearSpace, M be Subset of X;

      hereby

        assume

         A1: M is convex;

        let u,w be Point of X such that

         A2: u in M & w in M;

        thus ( LSeg (u,w)) c= M

        proof

          let x be object;

          assume x in ( LSeg (u,w));

          then ex r st x = (((1 - r) * u) + (r * w)) & 0 <= r & r <= 1;

          hence x in M by A1, A2;

        end;

      end;

      assume

       A3: for w,u be Point of X st w in M & u in M holds ( LSeg (w,u)) c= M;

      let u,w be Point of X, r be Real such that

       A4: 0 <= r & r <= 1 and

       A5: u in M & w in M;

      

       A6: ((r * u) + ((1 - r) * w)) in ( LSeg (w,u)) by A4;

      ( LSeg (w,u)) c= M by A3, A5;

      hence thesis by A6;

    end;

    definition

      let V be non empty RLSStruct, P be Subset-Family of V;

      :: RLTOPSP1:def3

      attr P is convex-membered means

      : Def3: for M be Subset of V st M in P holds M is convex;

    end

    registration

      let V be non empty RLSStruct;

      cluster non empty convex-membered for Subset-Family of V;

      existence

      proof

        reconsider F = {( {} V)} as Subset-Family of V;

        take F;

        thus F is non empty;

        let M be Subset of V;

        assume M in F;

        then M = ( {} V) by TARSKI:def 1;

        hence thesis;

      end;

    end

    theorem :: RLTOPSP1:23

    for V be non empty RLSStruct, F be convex-membered Subset-Family of V holds ( meet F) is convex

    proof

      let V be non empty RLSStruct, F be convex-membered Subset-Family of V;

      for M be Subset of V st M in F holds M is convex by Def3;

      hence thesis by CONVEX1: 15;

    end;

    definition

      let X be non empty RLSStruct, A be Subset of X;

      :: RLTOPSP1:def4

      func - A -> Subset of X equals (( - 1) * A);

      coherence ;

    end

    theorem :: RLTOPSP1:24

    

     Th24: for X be RealLinearSpace, M,N be Subset of X, v be Point of X holds (v + M) meets N iff v in (N + ( - M))

    proof

      let X be RealLinearSpace, M,N be Subset of X, v be Point of X;

      

       A1: (N + (( - 1) * M)) = { (u + w) where u,w be Point of X : u in N & w in (( - 1) * M) } by RUSUB_4:def 9;

      hereby

        

         A2: (v + M) = { (v + u) where u be Point of X : u in M } by RUSUB_4:def 8;

        assume (v + M) meets N;

        then

        consider z be object such that

         A3: z in (v + M) and

         A4: z in N by XBOOLE_0: 3;

        consider u be Point of X such that

         A5: (v + u) = z and

         A6: u in M by A3, A2;

        reconsider z as Point of X by A3;

        

         A7: (( - 1) * u) in (( - 1) * M) by A6;

        (z + (( - 1) * u)) = (v + (u + (( - 1) * u))) by A5, RLVECT_1:def 3

        .= (v + (u + ( - u))) by RLVECT_1: 16

        .= (v + ( 0. X)) by RLVECT_1: 5

        .= v;

        hence v in (N + ( - M)) by A4, A7, Th3;

      end;

      assume v in (N + ( - M));

      then

      consider u,w be Point of X such that

       A8: v = (u + w) and

       A9: u in N and

       A10: w in (( - 1) * M) by A1;

      consider w9 be Point of X such that

       A11: w = (( - 1) * w9) and

       A12: w9 in M by A10;

      

       A13: (( - 1) * w) = ((( - 1) * ( - 1)) * w9) by A11, RLVECT_1:def 7

      .= w9 by RLVECT_1:def 8;

      (v + w9) = (u + (w + w9)) by A8, RLVECT_1:def 3

      .= (u + (w + ( - w))) by A13, RLVECT_1: 16

      .= (u + ( 0. X)) by RLVECT_1: 5

      .= u;

      then u in (v + M) by A12, Lm1;

      hence thesis by A9, XBOOLE_0: 3;

    end;

    definition

      let X be non empty RLSStruct, A be Subset of X;

      :: RLTOPSP1:def5

      attr A is symmetric means

      : Def5: A = ( - A);

    end

    registration

      let X be RealLinearSpace;

      cluster non empty symmetric for Subset of X;

      existence

      proof

        take V = {( 0. X)};

        thus V is non empty;

        thus V = ( - V) by Th13;

      end;

    end

    theorem :: RLTOPSP1:25

    

     Th25: for X be RealLinearSpace, A be symmetric Subset of X, x be Point of X st x in A holds ( - x) in A

    proof

      let X be RealLinearSpace, A be symmetric Subset of X, x be Point of X such that

       A1: x in A;

      A = ( - A) by Def5

      .= (( - 1) * A);

      then

      consider v be Point of X such that

       A2: x = (( - 1) * v) and

       A3: v in A by A1;

      (( - 1) * x) = ((( - 1) * ( - 1)) * v) by A2, RLVECT_1:def 7

      .= v by RLVECT_1:def 8;

      hence thesis by A3, RLVECT_1: 16;

    end;

    definition

      let X be non empty RLSStruct, A be Subset of X;

      :: RLTOPSP1:def6

      attr A is circled means

      : Def6: for r be Real st |.r.| <= 1 holds (r * A) c= A;

    end

    registration

      let X be non empty RLSStruct;

      cluster empty -> circled for Subset of X;

      coherence by CONVEX1: 33;

    end

    theorem :: RLTOPSP1:26

    

     Th26: for X be RealLinearSpace holds {( 0. X)} is circled by Th13;

    registration

      let X be RealLinearSpace;

      cluster non empty circled for Subset of X;

      existence

      proof

        take {( 0. X)};

        thus thesis by Th26;

      end;

    end

    theorem :: RLTOPSP1:27

    

     Th27: for X be RealLinearSpace, B be non empty circled Subset of X holds ( 0. X) in B

    proof

      let X be RealLinearSpace;

      let B be non empty circled Subset of X;

       |. 0 .| = 0 by ABSVALUE: 2;

      then ( 0 * B) c= B by Def6;

      then

       A1: {( 0. X)} c= B by CONVEX1: 34;

      ( 0. X) in {( 0. X)} by TARSKI:def 1;

      hence thesis by A1;

    end;

    

     Lm5: for X be RealLinearSpace, A,B be circled Subset of X holds (A + B) is circled

    proof

      let X be non empty RealLinearSpace, A,B be circled Subset of X;

      

       A1: (A + B) = { (u + v) where u,v be Point of X : u in A & v in B } by RUSUB_4:def 9;

      let r be Real;

      assume |.r.| <= 1;

      then

       A2: (r * A) c= A & (r * B) c= B by Def6;

      let x be object;

      assume x in (r * (A + B));

      then

      consider x9 be Point of X such that

       A3: x = (r * x9) and

       A4: x9 in (A + B);

      consider u,v be Point of X such that

       A5: x9 = (u + v) and

       A6: u in A & v in B by A1, A4;

      

       A7: (r * u) in (r * A) & (r * v) in (r * B) by A6;

      x = ((r * u) + (r * v)) by A3, A5, RLVECT_1:def 5;

      hence thesis by A2, A7, Th3;

    end;

    registration

      let X be RealLinearSpace, A,B be circled Subset of X;

      cluster (A + B) -> circled;

      coherence by Lm5;

    end

    theorem :: RLTOPSP1:28

    

     Th28: for X be RealLinearSpace, A be circled Subset of X holds for r be Real st |.r.| = 1 holds (r * A) = A

    proof

      let X be RealLinearSpace, A be circled Subset of X;

      let r be Real;

      assume

       A1: |.r.| = 1;

      hence

       A2: (r * A) c= A by Def6;

      let x be object;

      assume

       A3: x in A;

      then

      reconsider x as Point of X;

      

       A4: (r * x) in (r * A) by A3;

      per cases ;

        suppose 0 <= r;

        then r = 1 by A1, ABSVALUE:def 1;

        hence thesis by A3, CONVEX1: 32;

      end;

        suppose r < 0 ;

        then |.r.| = ( - r) by ABSVALUE:def 1;

        then (( - 1) * (( - 1) * x)) in (r * A) by A1, A2, A4;

        then ((( - 1) * ( - 1)) * x) in (r * A) by RLVECT_1:def 7;

        hence thesis by RLVECT_1:def 8;

      end;

    end;

    

     Lm6: for X be RealLinearSpace, A be circled Subset of X holds A is symmetric

    proof

      let X be RealLinearSpace, A be circled Subset of X;

       |.( - 1).| = ( - ( - 1)) by ABSVALUE:def 1

      .= 1;

      hence A = ( - A) by Th28;

    end;

    registration

      let X be RealLinearSpace;

      cluster circled -> symmetric for Subset of X;

      coherence by Lm6;

    end

    

     Lm7: for X be RealLinearSpace, M be circled Subset of X holds ( conv M) is circled

    proof

      let X be RealLinearSpace, M be circled Subset of X;

      let r be Real;

      assume |.r.| <= 1;

      then

       A1: (r * M) c= M by Def6;

      (r * ( conv M)) = ( conv (r * M)) by Th18;

      hence thesis by A1, Th20;

    end;

    registration

      let X be RealLinearSpace, M be circled Subset of X;

      cluster ( conv M) -> circled;

      coherence by Lm7;

    end

    definition

      let X be non empty RLSStruct, F be Subset-Family of X;

      :: RLTOPSP1:def7

      attr F is circled-membered means

      : Def7: for V be Subset of X st V in F holds V is circled;

    end

    registration

      let V be non empty RLSStruct;

      cluster non empty circled-membered for Subset-Family of V;

      existence

      proof

        reconsider F = {( {} V)} as Subset-Family of V;

        take F;

        thus F is non empty;

        let M be Subset of V;

        assume M in F;

        hence thesis by TARSKI:def 1;

      end;

    end

    theorem :: RLTOPSP1:29

    for X be non empty RLSStruct, F be circled-membered Subset-Family of X holds ( union F) is circled

    proof

      let X be non empty RLSStruct, F be circled-membered Subset-Family of X;

      let r be Real such that

       A1: |.r.| <= 1;

      let x be object;

      assume x in (r * ( union F));

      then

      consider x9 be Point of X such that

       A2: x = (r * x9) and

       A3: x9 in ( union F);

      consider Y be set such that

       A4: x9 in Y and

       A5: Y in F by A3, TARSKI:def 4;

      reconsider Y as Subset of X by A5;

      Y is circled by A5, Def7;

      then

       A6: (r * Y) c= Y by A1;

      (r * x9) in (r * Y) by A4;

      hence thesis by A2, A5, A6, TARSKI:def 4;

    end;

    theorem :: RLTOPSP1:30

    for X be non empty RLSStruct, F be circled-membered Subset-Family of X holds ( meet F) is circled

    proof

      let X be non empty RLSStruct, F be circled-membered Subset-Family of X;

      let r be Real such that

       A1: |.r.| <= 1;

      let x be object;

      assume x in (r * ( meet F));

      then

      consider x9 be Point of X such that

       A2: x = (r * x9) and

       A3: x9 in ( meet F);

       A4:

      now

        let Y be set;

        assume

         A5: Y in F;

        then

        reconsider Y9 = Y as Subset of X;

        x9 in Y by A3, A5, SETFAM_1:def 1;

        then

         A6: (r * x9) in (r * Y9);

        Y9 is circled by A5, Def7;

        then (r * Y9) c= Y9 by A1;

        hence x in Y by A2, A6;

      end;

      F <> {} by A3, SETFAM_1:def 1;

      hence thesis by A4, SETFAM_1:def 1;

    end;

    begin

    definition

      struct ( RLSStruct, TopStruct) RLTopStruct (# the carrier -> set,

the ZeroF -> Element of the carrier,

the addF -> BinOp of the carrier,

the Mult -> Function of [: REAL , the carrier:], the carrier,

the topology -> Subset-Family of the carrier #)

       attr strict strict;

    end

    registration

      let X be non empty set, O be Element of X, F be BinOp of X, G be Function of [: REAL , X:], X, T be Subset-Family of X;

      cluster RLTopStruct (# X, O, F, G, T #) -> non empty;

      coherence ;

    end

    registration

      cluster strict non empty for RLTopStruct;

      existence

      proof

        set X = { 0 };

        reconsider O = 0 as Element of X by TARSKI:def 1;

        set F = the BinOp of X;

        set G = the Function of [: REAL , X:], X;

        take RT = RLTopStruct (# X, O, F, G, ( {} ( bool X)) #);

        thus RT is strict;

        thus the carrier of RT is non empty;

      end;

    end

    definition

      let X be non empty RLTopStruct;

      :: RLTOPSP1:def8

      attr X is add-continuous means

      : Def8: for x1,x2 be Point of X, V be Subset of X st V is open & (x1 + x2) in V holds ex V1,V2 be Subset of X st V1 is open & V2 is open & x1 in V1 & x2 in V2 & (V1 + V2) c= V;

      :: RLTOPSP1:def9

      attr X is Mult-continuous means

      : Def9: for a be Real, x be Point of X, V be Subset of X st V is open & (a * x) in V holds ex r be positive Real, W be Subset of X st W is open & x in W & for s be Real st |.(s - a).| < r holds (s * W) c= V;

    end

    registration

      cluster strict add-continuous Mult-continuous TopSpace-like Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital for non empty RLTopStruct;

      existence

      proof

        set ZS = { 0 };

        set T = { {} , ZS};

        T c= ( bool ZS)

        proof

          let x be object;

          reconsider xx = x as set by TARSKI: 1;

          assume x in T;

          then x = {} or x = ZS by TARSKI:def 2;

          then xx c= ZS;

          hence thesis;

        end;

        then

        reconsider T as Subset-Family of ZS;

        reconsider O = 0 as Element of ZS by TARSKI:def 1;

        deffunc A( Element of ZS, Element of ZS) = O;

        consider F be BinOp of ZS such that

         A1: for x,y be Element of ZS holds (F . (x,y)) = A(x,y) from BINOP_1:sch 4;

        deffunc M( Real, Element of ZS) = O;

        consider G be Function of [: REAL , ZS:], ZS such that

         A2: for a be Element of REAL holds for x be Element of ZS holds (G . (a,x)) = M(a,x) from BINOP_1:sch 4;

        take W = RLTopStruct (# ZS, O, F, G, T #);

        thus W is strict;

        thus W is add-continuous

        proof

          reconsider V1 = {O}, V2 = {O} as Subset of W;

          let x1,x2 be Point of W, V be Subset of W such that

           A3: V is open and

           A4: (x1 + x2) in V;

          take V1, V2;

          V1 in T by TARSKI:def 2;

          hence V1 is open & V2 is open;

          thus x1 in V1 & x2 in V2;

          V in T by A3;

          then V = the carrier of W by A4, TARSKI:def 2;

          hence thesis;

        end;

        thus W is Mult-continuous

        proof

          reconsider V9 = {O} as Subset of W;

          let a be Real, x be Point of W, V be Subset of W such that

           A5: V is open and

           A6: (a * x) in V;

          take jj, V9;

          V9 in T by TARSKI:def 2;

          hence V9 is open;

          thus x in V9;

          let s be Real such that |.(s - a).| < jj;

          V in T by A5;

          then V = {} or V = ZS by TARSKI:def 2;

          hence thesis by A6;

        end;

        thus W is TopSpace-like

        proof

          thus the carrier of W in the topology of W by TARSKI:def 2;

          hereby

            let a be Subset-Family of W;

            assume a c= the topology of W;

            then a = {} or a = { {} } or a = {ZS} or a = { {} , ZS} by ZFMISC_1: 36;

            then ( union a) = {} or ( union a) = ZS or ( union a) = ( {} \/ ZS) by ZFMISC_1: 2, ZFMISC_1: 25, ZFMISC_1: 75;

            hence ( union a) in the topology of W by TARSKI:def 2;

          end;

          let a,b be Subset of W such that

           A7: a in the topology of W and

           A8: b in the topology of W;

          

           A9: b = {} or b = ZS by A8, TARSKI:def 2;

          a = {} or a = ZS by A7, TARSKI:def 2;

          hence thesis by A9, TARSKI:def 2;

        end;

        thus for x,y be Point of W holds (x + y) = (y + x)

        proof

          let x,y be Point of W;

          reconsider X = x, Y = y as Element of ZS;

          (x + y) = A(X,Y) by A1;

          hence thesis by A1;

        end;

        thus for x,y,z be Point of W holds ((x + y) + z) = (x + (y + z))

        proof

          let x,y,z be Point of W;

          reconsider X = x, Y = y, Z = z as Element of ZS;

          ((x + y) + z) = A(A,Z) by A1;

          hence thesis by A1;

        end;

        thus for x be Point of W holds (x + ( 0. W)) = x

        proof

          let x be Point of W;

          reconsider X = x as Element of ZS;

          (x + ( 0. W)) = A(X,O) by A1;

          hence thesis by TARSKI:def 1;

        end;

        thus for x be Point of W holds x is right_complementable

        proof

          reconsider y = O as Point of W;

          let x be Point of W;

          take y;

          thus thesis by A1;

        end;

        thus for a be Real, x,y be Point of W holds (a * (x + y)) = ((a * x) + (a * y))

        proof

          let a be Real;

          reconsider a as Element of REAL by XREAL_0:def 1;

          let x,y be Point of W;

          reconsider X = x, Y = y as Element of ZS;

          ((a * x) + (a * y)) = M(a,A) by A1

          .= (G . (a, A(X,Y))) by A2

          .= (G . (a,(F . (x,y)))) by A1;

          hence thesis;

        end;

        thus for a,b be Real holds for x be Point of W holds ((a + b) * x) = ((a * x) + (b * x))

        proof

          let a,b be Real, x be Point of W;

          reconsider a, b as Element of REAL by XREAL_0:def 1;

          set c = (a + b);

          reconsider X = x as Element of ZS;

          (c * x) = M(c,X) by A2;

          hence thesis by A1;

        end;

        thus for a,b be Real, x be Point of W holds ((a * b) * x) = (a * (b * x))

        proof

          let a,b be Real, x be Point of W;

          reconsider a, b as Element of REAL by XREAL_0:def 1;

          set c = (a * b);

          reconsider X = x as Element of ZS;

          (c * x) = M(c,X) by A2;

          hence thesis by A2;

        end;

        thus for x be Point of W holds (1 * x) = x

        proof

          reconsider A9 = 1 as Element of REAL by XREAL_0:def 1;

          let x be Point of W;

          reconsider X = x as Element of ZS;

          (A9 * x) = M(A9,X) by A2;

          hence thesis by TARSKI:def 1;

        end;

      end;

    end

    definition

      mode LinearTopSpace is add-continuous Mult-continuous TopSpace-like Abelian add-associative right_zeroed right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital non empty RLTopStruct;

    end

    theorem :: RLTOPSP1:31

    

     Th31: for X be LinearTopSpace, x1,x2 be Point of X, V be a_neighborhood of (x1 + x2) holds ex V1 be a_neighborhood of x1, V2 be a_neighborhood of x2 st (V1 + V2) c= V

    proof

      let X be LinearTopSpace;

      let x1,x2 be Point of X, V be a_neighborhood of (x1 + x2);

      (x1 + x2) in ( Int V) by CONNSP_2:def 1;

      then

      consider V1,V2 be Subset of X such that

       A1: V1 is open and

       A2: V2 is open and

       A3: x1 in V1 and

       A4: x2 in V2 and

       A5: (V1 + V2) c= ( Int V) by Def8;

      ( Int V2) = V2 by A2, TOPS_1: 23;

      then

      reconsider V2 as a_neighborhood of x2 by A4, CONNSP_2:def 1;

      ( Int V1) = V1 by A1, TOPS_1: 23;

      then

      reconsider V1 as a_neighborhood of x1 by A3, CONNSP_2:def 1;

      take V1, V2;

      ( Int V) c= V by TOPS_1: 16;

      hence thesis by A5;

    end;

    theorem :: RLTOPSP1:32

    

     Th32: for X be LinearTopSpace, a be Real, x be Point of X, V be a_neighborhood of (a * x) holds ex r be positive Real, W be a_neighborhood of x st for s be Real st |.(s - a).| < r holds (s * W) c= V

    proof

      let X be LinearTopSpace, a be Real, x be Point of X, V be a_neighborhood of (a * x);

      (a * x) in ( Int V) by CONNSP_2:def 1;

      then

      consider r be positive Real, W be Subset of X such that

       A1: W is open and

       A2: x in W and

       A3: for s be Real st |.(s - a).| < r holds (s * W) c= ( Int V) by Def9;

      ( Int W) = W by A1, TOPS_1: 23;

      then

      reconsider W as a_neighborhood of x by A2, CONNSP_2:def 1;

      take r;

      take W;

      let s be Real;

      assume |.(s - a).| < r;

      then

       A4: (s * W) c= ( Int V) by A3;

      ( Int V) c= V by TOPS_1: 16;

      hence thesis by A4;

    end;

    definition

      let X be non empty RLTopStruct, a be Point of X;

      :: RLTOPSP1:def10

      func transl (a,X) -> Function of X, X means

      : Def10: for x be Point of X holds (it . x) = (a + x);

      existence

      proof

        deffunc F( Point of X) = (a + $1);

        consider F be Function of the carrier of X, the carrier of X such that

         A1: for x be Point of X holds (F . x) = F(x) from FUNCT_2:sch 4;

        reconsider F as Function of X, X;

        take F;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let F,G be Function of X, X such that

         A2: for x be Point of X holds (F . x) = (a + x) and

         A3: for x be Point of X holds (G . x) = (a + x);

        now

          let x be Point of X;

          

          thus (F . x) = (a + x) by A2

          .= (G . x) by A3;

        end;

        hence F = G by FUNCT_2: 63;

      end;

    end

    theorem :: RLTOPSP1:33

    

     Th33: for X be non empty RLTopStruct, a be Point of X, V be Subset of X holds (( transl (a,X)) .: V) = (a + V)

    proof

      let X be non empty RLTopStruct, a be Point of X, V be Subset of X;

      thus (( transl (a,X)) .: V) c= (a + V)

      proof

        let y be object;

        assume y in (( transl (a,X)) .: V);

        then

        consider c be Point of X such that

         A1: c in V and

         A2: y = (( transl (a,X)) . c) by FUNCT_2: 65;

        y = (a + c) by A2, Def10;

        hence thesis by A1, Lm1;

      end;

      let x be object;

      assume x in (a + V);

      then x in { (a + u) where u be Point of X : u in V } by RUSUB_4:def 8;

      then

      consider u be Point of X such that

       A3: x = (a + u) and

       A4: u in V;

      x = (( transl (a,X)) . u) by A3, Def10;

      hence thesis by A4, FUNCT_2: 35;

    end;

    theorem :: RLTOPSP1:34

    

     Th34: for X be LinearTopSpace, a be Point of X holds ( rng ( transl (a,X))) = ( [#] X)

    proof

      let X be LinearTopSpace, a be Point of X;

      thus ( rng ( transl (a,X))) c= ( [#] X);

      let y be object;

      assume y in ( [#] X);

      then

      reconsider y as Point of X;

      (( transl (a,X)) . (( - a) + y)) = (a + (( - a) + y)) by Def10

      .= ((a + ( - a)) + y) by RLVECT_1:def 3

      .= (( 0. X) + y) by RLVECT_1: 5

      .= y;

      hence thesis by FUNCT_2: 4;

    end;

    

     Lm8: for X be LinearTopSpace, a be Point of X holds ( transl (a,X)) is one-to-one

    proof

      let X be LinearTopSpace, a be Point of X;

      now

        let x1,x2 be object such that

         A1: x1 in the carrier of X & x2 in the carrier of X and

         A2: (( transl (a,X)) . x1) = (( transl (a,X)) . x2);

        reconsider x19 = x1, x29 = x2 as Point of X by A1;

        (( transl (a,X)) . x1) = (a + x19) & (( transl (a,X)) . x2) = (a + x29) by Def10;

        hence x1 = x2 by A2, RLVECT_1: 8;

      end;

      hence thesis by FUNCT_2: 19;

    end;

    theorem :: RLTOPSP1:35

    

     Th35: for X be LinearTopSpace, a be Point of X holds (( transl (a,X)) " ) = ( transl (( - a),X))

    proof

      let X be LinearTopSpace, a be Point of X;

      

       A1: ( rng ( transl (a,X))) = ( [#] X) by Th34;

      now

        let x be Point of X;

        consider u be object such that

         A2: u in ( dom ( transl (a,X))) and

         A3: x = (( transl (a,X)) . u) by A1, FUNCT_1:def 3;

        reconsider u as Point of X by A2;

        

         A4: x = (a + u) by A3, Def10;

        ( transl (a,X)) is onto one-to-one by A1, Lm8, FUNCT_2:def 3;

        

        hence ((( transl (a,X)) " ) . x) = ((( transl (a,X)) qua Function " ) . x) by TOPS_2:def 4

        .= u by A3, Lm8, FUNCT_2: 26

        .= (( 0. X) + u)

        .= ((( - a) + a) + u) by RLVECT_1: 5

        .= (( - a) + x) by A4, RLVECT_1:def 3

        .= (( transl (( - a),X)) . x) by Def10;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    

     Lm9: for X be LinearTopSpace, a be Point of X holds ( transl (a,X)) is continuous

    proof

      let X be LinearTopSpace, a be Point of X;

       A1:

      now

        reconsider X9 = X as TopStruct;

        let P be Subset of X;

        defpred P[ Subset of X9] means ex D be Subset of X st D = $1 & D is open & (a + D) c= P;

        consider F be Subset-Family of X9 such that

         A2: for A be Subset of X9 holds A in F iff P[A] from SUBSET_1:sch 3;

        reconsider F as Subset-Family of X;

        assume

         A3: P is open;

        

         A4: ( union F) = (( transl (a,X)) " P)

        proof

          thus ( union F) c= (( transl (a,X)) " P)

          proof

            let x be object;

            assume x in ( union F);

            then

            consider A be set such that

             A5: x in A and

             A6: A in F by TARSKI:def 4;

            reconsider x as Point of X by A5, A6;

            

             A7: (( transl (a,X)) . x) = (a + x) by Def10;

            consider D be Subset of X such that

             A8: D = A and D is open and

             A9: (a + D) c= P by A2, A6;

            (a + D) = { (a + u) where u be Point of X : u in D } by RUSUB_4:def 8;

            then (a + x) in (a + D) by A5, A8;

            hence thesis by A9, A7, FUNCT_2: 38;

          end;

          let x be object;

          assume

           A10: x in (( transl (a,X)) " P);

          then

          reconsider x as Point of X;

          (( transl (a,X)) . x) in P by A10, FUNCT_2: 38;

          then (a + x) in P by Def10;

          then

          consider V,D be Subset of X such that V is open and

           A11: D is open and

           A12: a in V and

           A13: x in D and

           A14: (V + D) c= P by A3, Def8;

          ( {a} + D) = (a + D) & {a} c= V by A12, RUSUB_4: 33, ZFMISC_1: 31;

          then (a + D) c= (V + D) by Th10;

          then (a + D) c= P by A14;

          then D in F by A2, A11;

          hence thesis by A13, TARSKI:def 4;

        end;

        F is open

        proof

          let A be Subset of X;

          assume A in F;

          then ex D be Subset of X st D = A & D is open & (a + D) c= P by A2;

          hence thesis;

        end;

        hence (( transl (a,X)) " P) is open by A4, TOPS_2: 19;

      end;

      ( [#] X) <> {} ;

      hence thesis by A1, TOPS_2: 43;

    end;

    registration

      let X be LinearTopSpace, a be Point of X;

      cluster ( transl (a,X)) -> being_homeomorphism;

      coherence

      proof

        thus ( dom ( transl (a,X))) = ( [#] X) by FUNCT_2:def 1;

        thus ( rng ( transl (a,X))) = ( [#] X) by Th34;

        thus ( transl (a,X)) is one-to-one by Lm8;

        thus ( transl (a,X)) is continuous by Lm9;

        (( transl (a,X)) " ) = ( transl (( - a),X)) by Th35;

        hence thesis by Lm9;

      end;

    end

    

     Lm10: for X be LinearTopSpace, E be Subset of X, x be Point of X st E is open holds (x + E) is open

    proof

      let X be LinearTopSpace, E be Subset of X, x be Point of X;

      assume

       A1: E is open;

      (( transl (x,X)) .: E) = (x + E) by Th33;

      hence thesis by A1, TOPGRP_1: 25;

    end;

    registration

      let X be LinearTopSpace, E be open Subset of X, x be Point of X;

      cluster (x + E) -> open;

      coherence by Lm10;

    end

    

     Lm11: for X be LinearTopSpace, E be open Subset of X, K be Subset of X holds (K + E) is open

    proof

      let X be LinearTopSpace, E be open Subset of X, K be Subset of X;

      reconsider F = { (a + E) where a be Point of X : a in K } as Subset-Family of X by Lm2;

      

       A1: F is open

      proof

        let P be Subset of X;

        assume P in F;

        then ex a be Point of X st P = (a + E) & a in K;

        hence thesis;

      end;

      (K + E) = ( union F) by Th4;

      hence thesis by A1, TOPS_2: 19;

    end;

    registration

      let X be LinearTopSpace, E be open Subset of X, K be Subset of X;

      cluster (K + E) -> open;

      coherence by Lm11;

    end

    

     Lm12: for X be LinearTopSpace, D be closed Subset of X, x be Point of X holds (x + D) is closed

    proof

      let X be LinearTopSpace, D be closed Subset of X, x be Point of X;

      (( transl (x,X)) .: D) = (x + D) by Th33;

      hence thesis by TOPS_2: 58;

    end;

    registration

      let X be LinearTopSpace, D be closed Subset of X, x be Point of X;

      cluster (x + D) -> closed;

      coherence by Lm12;

    end

    theorem :: RLTOPSP1:36

    

     Th36: for X be LinearTopSpace, V1,V2,V be Subset of X st (V1 + V2) c= V holds (( Int V1) + ( Int V2)) c= ( Int V)

    proof

      let X be LinearTopSpace, V1,V2,V be Subset of X such that

       A1: (V1 + V2) c= V;

      ( Int V1) c= V1 & ( Int V2) c= V2 by TOPS_1: 16;

      then (( Int V1) + ( Int V2)) c= (V1 + V2) by Th11;

      then (( Int V1) + ( Int V2)) c= V by A1;

      hence thesis by TOPS_1: 24;

    end;

    theorem :: RLTOPSP1:37

    

     Th37: for X be LinearTopSpace, x be Point of X, V be Subset of X holds (x + ( Int V)) = ( Int (x + V))

    proof

      let X be LinearTopSpace, x be Point of X, V be Subset of X;

      (x + ( Int V)) c= (x + V) by Th8, TOPS_1: 16;

      hence (x + ( Int V)) c= ( Int (x + V)) by TOPS_1: 24;

      let v be object;

      assume

       A1: v in ( Int (x + V));

      then

      reconsider v as Point of X;

      consider Q be Subset of X such that

       A2: Q is open and

       A3: Q c= (x + V) and

       A4: v in Q by A1, TOPS_1: 22;

      (( - x) + Q) c= (( - x) + (x + V)) by A3, Th8;

      then (( - x) + Q) c= ((( - x) + x) + V) by Th6;

      then (( - x) + Q) c= (( 0. X) + V) by RLVECT_1: 5;

      then (( - x) + Q) c= V by Th5;

      then

       A5: (x + ( Int V)) = { (x + u) where u be Point of X : u in ( Int V) } & (( - x) + Q) c= ( Int V) by A2, RUSUB_4:def 8, TOPS_1: 24;

      (( - x) + v) in (( - x) + Q) by A4, Lm1;

      then (x + (( - x) + v)) in (x + ( Int V)) by A5;

      then ((x + ( - x)) + v) in (x + ( Int V)) by RLVECT_1:def 3;

      then (( 0. X) + v) in (x + ( Int V)) by RLVECT_1: 5;

      hence thesis;

    end;

    theorem :: RLTOPSP1:38

    for X be LinearTopSpace, x be Point of X, V be Subset of X holds (x + ( Cl V)) = ( Cl (x + V))

    proof

      let X be LinearTopSpace, x be Point of X, V be Subset of X;

      thus (x + ( Cl V)) c= ( Cl (x + V))

      proof

        let v be object;

        assume

         A1: v in (x + ( Cl V));

        then

        reconsider v as Point of X;

        now

          

           A2: (x + ( Cl V)) = { (x + u) where u be Point of X : u in ( Cl V) } by RUSUB_4:def 8;

          

           A3: (x + V) = { (x + u) where u be Point of X : u in V } by RUSUB_4:def 8;

          let G be Subset of X such that

           A4: G is open and

           A5: v in G;

          

           A6: (( - x) + G) = { (( - x) + u) where u be Point of X : u in G } by RUSUB_4:def 8;

          then

           A7: (( - x) + v) in (( - x) + G) by A5;

          consider u be Point of X such that

           A8: v = (x + u) and

           A9: u in ( Cl V) by A1, A2;

          (( - x) + v) = ((( - x) + x) + u) by A8, RLVECT_1:def 3

          .= (( 0. X) + u) by RLVECT_1: 5

          .= u;

          then V meets (( - x) + G) by A4, A9, A7, PRE_TOPC: 24;

          then

          consider z be object such that

           A10: z in V and

           A11: z in (( - x) + G) by XBOOLE_0: 3;

          reconsider z as Point of X by A10;

          consider w be Point of X such that

           A12: z = (( - x) + w) and

           A13: w in G by A6, A11;

          

           A14: (x + z) in (x + V) by A3, A10;

          (x + z) = ((x + ( - x)) + w) by A12, RLVECT_1:def 3

          .= (( 0. X) + w) by RLVECT_1: 5

          .= w;

          hence (x + V) meets G by A13, A14, XBOOLE_0: 3;

        end;

        hence thesis by PRE_TOPC: 24;

      end;

      (x + V) c= (x + ( Cl V)) by Th8, PRE_TOPC: 18;

      hence thesis by TOPS_1: 5;

    end;

    theorem :: RLTOPSP1:39

    for X be LinearTopSpace, x,v be Point of X, V be a_neighborhood of x holds (v + V) is a_neighborhood of (v + x)

    proof

      let X be LinearTopSpace, x,v be Point of X, V be a_neighborhood of x;

      (v + ( Int V)) = { (v + u) where u be Point of X : u in ( Int V) } & x in ( Int V) by CONNSP_2:def 1, RUSUB_4:def 8;

      then

       A1: (v + x) in (v + ( Int V));

      (v + ( Int V)) = ( Int (v + V)) by Th37;

      hence thesis by A1, CONNSP_2:def 1;

    end;

    theorem :: RLTOPSP1:40

    for X be LinearTopSpace, x be Point of X, V be a_neighborhood of x holds (( - x) + V) is a_neighborhood of ( 0. X)

    proof

      let X be LinearTopSpace, x be Point of X, V be a_neighborhood of x;

      (( - x) + ( Int V)) = { (( - x) + v) where v be Point of X : v in ( Int V) } & x in ( Int V) by CONNSP_2:def 1, RUSUB_4:def 8;

      then (( - x) + x) in (( - x) + ( Int V));

      then

       A1: ( 0. X) in (( - x) + ( Int V)) by RLVECT_1: 5;

      (( - x) + ( Int V)) c= ( Int (( - x) + V)) by Th37;

      hence thesis by A1, CONNSP_2:def 1;

    end;

    definition

      let X be non empty RLTopStruct;

      mode local_base of X is basis of ( 0. X);

    end

    definition

      let X be non empty RLTopStruct;

      :: RLTOPSP1:def11

      attr X is locally-convex means ex P be local_base of X st P is convex-membered;

    end

    definition

      let X be LinearTopSpace, E be Subset of X;

      :: RLTOPSP1:def12

      attr E is bounded means

      : Def12: for V be a_neighborhood of ( 0. X) holds ex s st s > 0 & for t st t > s holds E c= (t * V);

    end

    registration

      let X be LinearTopSpace;

      cluster empty -> bounded for Subset of X;

      coherence

      proof

        let S be Subset of X;

        assume S is empty;

        then

         A1: S = ( {} X);

        let V be a_neighborhood of ( 0. X);

        take 1;

        thus thesis by A1;

      end;

    end

    registration

      let X be LinearTopSpace;

      cluster bounded for Subset of X;

      existence

      proof

        take ( {} X);

        thus thesis;

      end;

    end

    theorem :: RLTOPSP1:41

    

     Th41: for X be LinearTopSpace, V1,V2 be bounded Subset of X holds (V1 \/ V2) is bounded

    proof

      let X be non empty LinearTopSpace, V1,V2 be bounded Subset of X;

      thus thesis

      proof

        let V be a_neighborhood of ( 0. X);

        consider s such that

         A1: s > 0 and

         A2: for t st t > s holds V1 c= (t * V) by Def12;

        consider r such that

         A3: r > 0 and

         A4: for t st t > r holds V2 c= (t * V) by Def12;

        per cases ;

          suppose

           A5: r <= s;

          take s;

          thus s > 0 by A1;

          let t such that

           A6: t > s;

          t > r by A5, A6, XXREAL_0: 2;

          then

           A7: V2 c= (t * V) by A4;

          V1 c= (t * V) by A2, A6;

          hence thesis by A7, XBOOLE_1: 8;

        end;

          suppose

           A8: r > s;

          take r;

          thus r > 0 by A3;

          let t such that

           A9: t > r;

          t > s by A8, A9, XXREAL_0: 2;

          then

           A10: V1 c= (t * V) by A2;

          V2 c= (t * V) by A4, A9;

          hence thesis by A10, XBOOLE_1: 8;

        end;

      end;

    end;

    theorem :: RLTOPSP1:42

    for X be LinearTopSpace, P be bounded Subset of X, Q be Subset of X st Q c= P holds Q is bounded

    proof

      let X be LinearTopSpace, P be bounded Subset of X, Q be Subset of X such that

       A1: Q c= P;

      let V be a_neighborhood of ( 0. X);

      consider s such that

       A2: s > 0 and

       A3: for t st t > s holds P c= (t * V) by Def12;

      take s;

      thus s > 0 by A2;

      let t;

      assume t > s;

      then P c= (t * V) by A3;

      hence thesis by A1;

    end;

    theorem :: RLTOPSP1:43

    for X be LinearTopSpace, F be Subset-Family of X st F is finite & F = the set of all P where P be bounded Subset of X holds ( union F) is bounded

    proof

      let X be LinearTopSpace, F be Subset-Family of X such that

       A1: F is finite and

       A2: F = the set of all P where P be bounded Subset of X;

      defpred P[ set] means ex A be Subset of X st A = ( union $1) & A is bounded;

       A3:

      now

        let P be Subset of X;

        assume P in F;

        then ex A be bounded Subset of X st P = A by A2;

        hence P is bounded;

      end;

      

       A4: for x,B be set st x in F & B c= F & P[B] holds P[(B \/ {x})]

      proof

        let x,B be set such that

         A5: x in F and B c= F and

         A6: P[B];

        consider A be Subset of X such that

         A7: A = ( union B) & A is bounded by A6;

        reconsider x as Subset of X by A5;

        

         A8: ( union (B \/ {x})) = (( union B) \/ ( union {x})) by ZFMISC_1: 78

        .= (( union B) \/ x) by ZFMISC_1: 25;

        

         A9: x is bounded by A3, A5;

        ex Y be Subset of X st Y = ( union (B \/ {x})) & Y is bounded

        proof

          take (A \/ x);

          thus thesis by A7, A8, A9, Th41;

        end;

        hence thesis;

      end;

      ( {} X) = ( union {} ) by ZFMISC_1: 2;

      then

       A10: P[ {} ];

       P[F] from FINSET_1:sch 2( A1, A10, A4);

      hence thesis;

    end;

    theorem :: RLTOPSP1:44

    

     Th44: for X be LinearTopSpace, P be Subset-Family of X st P = the set of all U where U be a_neighborhood of ( 0. X) holds P is local_base of X

    proof

      let X be LinearTopSpace, P be Subset-Family of X such that

       A1: P = the set of all U where U be a_neighborhood of ( 0. X);

      let A be a_neighborhood of ( 0. X);

      take A;

      thus thesis by A1;

    end;

    theorem :: RLTOPSP1:45

    for X be LinearTopSpace, O be local_base of X, P be Subset-Family of X st P = { (a + U) where a be Point of X, U be Subset of X : U in O } holds P is basis of X

    proof

      let X be LinearTopSpace, O be basis of ( 0. X), P be Subset-Family of X such that

       A1: P = { (a + U) where a be Point of X, U be Subset of X : U in O };

      let p be Point of X;

      let A be a_neighborhood of p;

      p in ( Int A) by CONNSP_2:def 1;

      then (( - p) + ( Int A)) is a_neighborhood of ( 0. X) by Th9, CONNSP_2: 3;

      then

      consider V be a_neighborhood of ( 0. X) such that

       A2: V in O and

       A3: V c= (( - p) + ( Int A)) by YELLOW13:def 2;

      take U = (p + V);

      ( 0. X) in ( Int V) by CONNSP_2:def 1;

      then (p + ( 0. X)) in (p + ( Int V)) by Lm1;

      then

       A4: p in (p + ( Int V));

      (p + ( Int V)) c= ( Int U) by Th37;

      hence U is a_neighborhood of p by A4, CONNSP_2:def 1;

      thus U in P by A1, A2;

      U c= (p + (( - p) + ( Int A))) by A3, Th8;

      then U c= ((p + ( - p)) + ( Int A)) by Th6;

      then U c= (( 0. X) + ( Int A)) by RLVECT_1: 5;

      then ( Int A) c= A & U c= ( Int A) by Th5, TOPS_1: 16;

      hence thesis;

    end;

    definition

      let X be non empty RLTopStruct, r be Real;

      :: RLTOPSP1:def13

      func mlt (r,X) -> Function of X, X means

      : Def13: for x be Point of X holds (it . x) = (r * x);

      existence

      proof

        deffunc F( Point of X) = (r * $1);

        consider F be Function of the carrier of X, the carrier of X such that

         A1: for x be Point of X holds (F . x) = F(x) from FUNCT_2:sch 4;

        reconsider F as Function of X, X;

        take F;

        thus thesis by A1;

      end;

      uniqueness

      proof

        let F,G be Function of X, X such that

         A2: for x be Point of X holds (F . x) = (r * x) and

         A3: for x be Point of X holds (G . x) = (r * x);

        now

          let x be Point of X;

          

          thus (F . x) = (r * x) by A2

          .= (G . x) by A3;

        end;

        hence F = G by FUNCT_2: 63;

      end;

    end

    theorem :: RLTOPSP1:46

    

     Th46: for X be non empty RLTopStruct, V be Subset of X, r be non zero Real holds (( mlt (r,X)) .: V) = (r * V)

    proof

      let X be non empty RLTopStruct, V be Subset of X, r be non zero Real;

      thus (( mlt (r,X)) .: V) c= (r * V)

      proof

        let y be object;

        assume y in (( mlt (r,X)) .: V);

        then

        consider c be Point of X such that

         A1: c in V and

         A2: y = (( mlt (r,X)) . c) by FUNCT_2: 65;

        y = (r * c) by A2, Def13;

        hence thesis by A1;

      end;

      let x be object;

      assume x in (r * V);

      then

      consider u be Point of X such that

       A3: x = (r * u) and

       A4: u in V;

      x = (( mlt (r,X)) . u) by A3, Def13;

      hence thesis by A4, FUNCT_2: 35;

    end;

    theorem :: RLTOPSP1:47

    

     Th47: for X be LinearTopSpace, r be non zero Real holds ( rng ( mlt (r,X))) = ( [#] X)

    proof

      let X be LinearTopSpace, r be non zero Real;

      thus ( rng ( mlt (r,X))) c= ( [#] X);

      let y be object;

      assume y in ( [#] X);

      then

      reconsider y as Point of X;

      (( mlt (r,X)) . ((r " ) * y)) = (r * ((r " ) * y)) by Def13

      .= ((r * (r " )) * y) by RLVECT_1:def 7

      .= (1 * y) by XCMPLX_0:def 7

      .= y by RLVECT_1:def 8;

      hence thesis by FUNCT_2: 4;

    end;

    

     Lm13: for X be LinearTopSpace, r be non zero Real holds ( mlt (r,X)) is one-to-one

    proof

      let X be LinearTopSpace, r be non zero Real;

      now

        let x1,x2 be object such that

         A1: x1 in the carrier of X & x2 in the carrier of X and

         A2: (( mlt (r,X)) . x1) = (( mlt (r,X)) . x2);

        reconsider x19 = x1, x29 = x2 as Point of X by A1;

        (( mlt (r,X)) . x1) = (r * x19) & (( mlt (r,X)) . x2) = (r * x29) by Def13;

        hence x1 = x2 by A2, RLVECT_1: 36;

      end;

      hence thesis by FUNCT_2: 19;

    end;

    theorem :: RLTOPSP1:48

    

     Th48: for X be LinearTopSpace, r be non zero Real holds (( mlt (r,X)) " ) = ( mlt ((r " ),X))

    proof

      let X be LinearTopSpace, r be non zero Real;

      

       A1: ( rng ( mlt (r,X))) = ( [#] X) by Th47;

      now

        let x be Point of X;

        consider u be object such that

         A2: u in ( dom ( mlt (r,X))) and

         A3: x = (( mlt (r,X)) . u) by A1, FUNCT_1:def 3;

        reconsider u as Point of X by A2;

        

         A4: x = (r * u) by A3, Def13;

        ( mlt (r,X)) is onto one-to-one by A1, Lm13, FUNCT_2:def 3;

        

        hence ((( mlt (r,X)) " ) . x) = ((( mlt (r,X)) qua Function " ) . x) by TOPS_2:def 4

        .= u by A3, Lm13, FUNCT_2: 26

        .= (1 * u) by RLVECT_1:def 8

        .= ((r * (r " )) * u) by XCMPLX_0:def 7

        .= ((r " ) * x) by A4, RLVECT_1:def 7

        .= (( mlt ((r " ),X)) . x) by Def13;

      end;

      hence thesis by FUNCT_2: 63;

    end;

    

     Lm14: for X be LinearTopSpace, r be non zero Real holds ( mlt (r,X)) is continuous

    proof

      let X be LinearTopSpace, r be non zero Real;

       A1:

      now

        let P be Subset of X;

        defpred P[ Subset of X] means $1 is open & (r * $1) c= P;

        consider F be Subset-Family of X such that

         A2: for A be Subset of X holds A in F iff P[A] from SUBSET_1:sch 3;

        reconsider F as Subset-Family of X;

        assume

         A3: P is open;

        

         A4: ( union F) = (( mlt (r,X)) " P)

        proof

          thus ( union F) c= (( mlt (r,X)) " P)

          proof

            let x be object;

            assume x in ( union F);

            then

            consider A be set such that

             A5: x in A and

             A6: A in F by TARSKI:def 4;

            reconsider A as Subset of X by A6;

            A is Subset of X;

            then

            reconsider x as Point of X by A5;

            

             A7: (( mlt (r,X)) . x) = (r * x) by Def13;

            (r * A) c= P & (r * x) in (r * A) by A2, A5, A6;

            hence thesis by A7, FUNCT_2: 38;

          end;

          let x be object;

          assume

           A8: x in (( mlt (r,X)) " P);

          then

          reconsider x as Point of X;

          (( mlt (r,X)) . x) in P by A8, FUNCT_2: 38;

          then (r * x) in P by Def13;

          then

          consider e be positive Real, W be Subset of X such that

           A9: W is open and

           A10: x in W and

           A11: for s be Real st |.(s - r).| < e holds (s * W) c= P by A3, Def9;

           |.(r - r).| < e by ABSVALUE: 2;

          then (r * W) c= P by A11;

          then W in F by A2, A9;

          hence thesis by A10, TARSKI:def 4;

        end;

        F is open by A2;

        hence (( mlt (r,X)) " P) is open by A4, TOPS_2: 19;

      end;

      ( [#] X) <> {} ;

      hence thesis by A1, TOPS_2: 43;

    end;

    registration

      let X be LinearTopSpace, r be non zero Real;

      cluster ( mlt (r,X)) -> being_homeomorphism;

      coherence

      proof

        thus ( dom ( mlt (r,X))) = ( [#] X) by FUNCT_2:def 1;

        thus ( rng ( mlt (r,X))) = ( [#] X) by Th47;

        thus ( mlt (r,X)) is one-to-one by Lm13;

        thus ( mlt (r,X)) is continuous by Lm14;

        (( mlt (r,X)) " ) = ( mlt ((r " ),X)) by Th48;

        hence thesis by Lm14;

      end;

    end

    theorem :: RLTOPSP1:49

    

     Th49: for X be LinearTopSpace, V be open Subset of X, r be non zero Real holds (r * V) is open

    proof

      let X be LinearTopSpace, V be open Subset of X, r be non zero Real;

      reconsider r as non zero Real;

      (( mlt (r,X)) .: V) = (r * V) by Th46;

      hence thesis by TOPGRP_1: 25;

    end;

    theorem :: RLTOPSP1:50

    

     Th50: for X be LinearTopSpace, V be closed Subset of X, r be non zero Real holds (r * V) is closed

    proof

      let X be LinearTopSpace, V be closed Subset of X, r be non zero Real;

      reconsider r as non zero Real;

      (( mlt (r,X)) .: V) = (r * V) by Th46;

      hence thesis by TOPS_2: 58;

    end;

    theorem :: RLTOPSP1:51

    

     Th51: for X be LinearTopSpace, V be Subset of X, r be non zero Real holds (r * ( Int V)) = ( Int (r * V))

    proof

      let X be LinearTopSpace, V be Subset of X, r be non zero Real;

      (r * ( Int V)) c= (r * V) by CONVEX1: 39, TOPS_1: 16;

      hence (r * ( Int V)) c= ( Int (r * V)) by Th49, TOPS_1: 24;

      let x be object;

      assume

       A1: x in ( Int (r * V));

      then

      reconsider x as Point of X;

      consider Q be Subset of X such that

       A2: Q is open and

       A3: Q c= (r * V) and

       A4: x in Q by A1, TOPS_1: 22;

      ((r " ) * Q) c= ((r " ) * (r * V)) by A3, CONVEX1: 39;

      then ((r " ) * Q) c= (((r " ) * r) * V) by CONVEX1: 37;

      then ((r " ) * Q) c= (1 * V) by XCMPLX_0:def 7;

      then

       A5: ((r " ) * Q) c= V by CONVEX1: 32;

      ((r " ) * x) in ((r " ) * Q) & ((r " ) * Q) is open by A2, A4, Th49;

      then ((r " ) * x) in ( Int V) by A5, TOPS_1: 22;

      then (r * ((r " ) * x)) in (r * ( Int V));

      then ((r * (r " )) * x) in (r * ( Int V)) by RLVECT_1:def 7;

      then (1 * x) in (r * ( Int V)) by XCMPLX_0:def 7;

      hence thesis by RLVECT_1:def 8;

    end;

    theorem :: RLTOPSP1:52

    

     Th52: for X be LinearTopSpace, A be Subset of X, r be non zero Real holds (r * ( Cl A)) = ( Cl (r * A))

    proof

      let X be LinearTopSpace, A be Subset of X, r be non zero Real;

      thus (r * ( Cl A)) c= ( Cl (r * A))

      proof

        let z be object;

        assume

         A1: z in (r * ( Cl A));

        then

        reconsider z as Point of X;

        now

          let G be Subset of X;

          assume G is open & z in G;

          then

           A2: ((r " ) * z) in ((r " ) * G) & ((r " ) * G) is open by Th49;

          consider v be Point of X such that

           A3: z = (r * v) and

           A4: v in ( Cl A) by A1;

          ((r " ) * z) = (((r " ) * r) * v) by A3, RLVECT_1:def 7

          .= (1 * v) by XCMPLX_0:def 7

          .= v by RLVECT_1:def 8;

          then A meets ((r " ) * G) by A4, A2, PRE_TOPC: 24;

          then

          consider x be object such that

           A5: x in A and

           A6: x in ((r " ) * G) by XBOOLE_0: 3;

          reconsider x as Point of X by A5;

          consider u be Point of X such that

           A7: x = ((r " ) * u) and

           A8: u in G by A6;

          

           A9: (r * x) in (r * A) by A5;

          (r * x) = ((r * (r " )) * u) by A7, RLVECT_1:def 7

          .= (1 * u) by XCMPLX_0:def 7

          .= u by RLVECT_1:def 8;

          hence (r * A) meets G by A8, A9, XBOOLE_0: 3;

        end;

        hence thesis by PRE_TOPC: 24;

      end;

      (r * A) c= (r * ( Cl A)) by CONVEX1: 39, PRE_TOPC: 18;

      hence thesis by Th50, TOPS_1: 5;

    end;

    theorem :: RLTOPSP1:53

    for X be LinearTopSpace, A be Subset of X st X is T_1 holds ( 0 * ( Cl A)) = ( Cl ( 0 * A))

    proof

      let X be LinearTopSpace, A be Subset of X such that

       A1: X is T_1;

      per cases ;

        suppose

         A2: A is empty;

        then

         A3: ( Cl A) = ( {} X) by PRE_TOPC: 22;

        

        hence ( 0 * ( Cl A)) = ( {} X) by CONVEX1: 33

        .= ( Cl ( 0 * A)) by A2, A3, CONVEX1: 33;

      end;

        suppose

         A4: A is non empty;

        then ( Cl A) is non empty by PRE_TOPC: 18, XBOOLE_1: 3;

        

        hence ( 0 * ( Cl A)) = {( 0. X)} by CONVEX1: 34

        .= ( Cl {( 0. X)}) by A1, YELLOW_8: 26

        .= ( Cl ( 0 * A)) by A4, CONVEX1: 34;

      end;

    end;

    theorem :: RLTOPSP1:54

    

     Th54: for X be LinearTopSpace, x be Point of X, V be a_neighborhood of x, r be non zero Real holds (r * V) is a_neighborhood of (r * x)

    proof

      let X be LinearTopSpace, x be Point of X, V be a_neighborhood of x, r be non zero Real;

      x in ( Int V) by CONNSP_2:def 1;

      then (r * x) in (r * ( Int V));

      hence (r * x) in ( Int (r * V)) by Th51;

    end;

    theorem :: RLTOPSP1:55

    

     Th55: for X be LinearTopSpace, V be a_neighborhood of ( 0. X), r be non zero Real holds (r * V) is a_neighborhood of ( 0. X)

    proof

      let X be LinearTopSpace, V be a_neighborhood of ( 0. X), r be non zero Real;

      (r * V) is a_neighborhood of (r * ( 0. X)) by Th54;

      hence thesis;

    end;

    

     Lm15: for X be LinearTopSpace, V be bounded Subset of X, r be Real holds (r * V) is bounded

    proof

      let X be LinearTopSpace, V be bounded Subset of X;

      let r be Real;

      per cases ;

        suppose

         A1: r = 0 ;

        per cases ;

          suppose V is empty;

          hence thesis by CONVEX1: 33;

        end;

          suppose

           A2: V is non empty;

          let U be a_neighborhood of ( 0. X);

          take s = 1;

          thus s > 0 ;

          let t;

          assume t > s;

          then (t * U) is a_neighborhood of ( 0. X) by Th55;

          then

           A3: ( 0. X) in (t * U) by CONNSP_2: 4;

          (r * V) = {( 0. X)} by A1, A2, CONVEX1: 34;

          hence thesis by A3, ZFMISC_1: 31;

        end;

      end;

        suppose

         A4: r <> 0 ;

        let U be a_neighborhood of ( 0. X);

        ((1 / r) * U) is a_neighborhood of ( 0. X) by A4, Th55;

        then

        consider s such that

         A5: s > 0 and

         A6: for t st t > s holds V c= (t * ((1 / r) * U)) by Def12;

        take s;

        thus s > 0 by A5;

        let t;

        assume t > s;

        then (r * V) c= (r * (t * ((1 / r) * U))) by A6, CONVEX1: 39;

        then (r * V) c= (r * ((t * (1 / r)) * U)) by CONVEX1: 37;

        then (r * V) c= (r * ((1 / r) * (t * U))) by CONVEX1: 37;

        then (r * V) c= ((r * (1 / r)) * (t * U)) by CONVEX1: 37;

        then (r * V) c= (1 * (t * U)) by A4, XCMPLX_1: 87;

        then

         A7: (r * V) c= (t * U) by CONVEX1: 32;

        let x be object;

        assume x in (r * V);

        hence thesis by A7;

      end;

    end;

    registration

      let X be LinearTopSpace, V be bounded Subset of X, r be Real;

      cluster (r * V) -> bounded;

      coherence by Lm15;

    end

    theorem :: RLTOPSP1:56

    

     Th56: for X be LinearTopSpace, W be a_neighborhood of ( 0. X) holds ex U be open a_neighborhood of ( 0. X) st U is symmetric & (U + U) c= W

    proof

      let X be LinearTopSpace, W be a_neighborhood of ( 0. X);

      (( 0. X) + ( 0. X)) = ( 0. X);

      then

      consider V1 be a_neighborhood of ( 0. X), V2 be a_neighborhood of ( 0. X) such that

       A1: (V1 + V2) c= W by Th31;

      set U = (((( Int V1) /\ ( Int V2)) /\ (( - 1) * ( Int V1))) /\ (( - 1) * ( Int V2)));

      

       A2: (( - 1) * ( Int V1)) is open & (( - 1) * ( Int V2)) is open by Th49;

      (( - 1) * V2) is a_neighborhood of ( 0. X) by Th55;

      then ( 0. X) in ( Int (( - 1) * V2)) by CONNSP_2:def 1;

      then

       A3: ( 0. X) in (( - 1) * ( Int V2)) by Th51;

      (( - 1) * V1) is a_neighborhood of ( 0. X) by Th55;

      then ( 0. X) in ( Int (( - 1) * V1)) by CONNSP_2:def 1;

      then

       A4: ( 0. X) in (( - 1) * ( Int V1)) by Th51;

      ( 0. X) in ( Int V1) & ( 0. X) in ( Int V2) by CONNSP_2:def 1;

      then ( 0. X) in (( Int V1) /\ ( Int V2)) by XBOOLE_0:def 4;

      then ( 0. X) in ((( Int V1) /\ ( Int V2)) /\ (( - 1) * ( Int V1))) by A4, XBOOLE_0:def 4;

      then ( 0. X) in U by A3, XBOOLE_0:def 4;

      then ( 0. X) in ( Int U) by A2, TOPS_1: 23;

      then

      reconsider U as open a_neighborhood of ( 0. X) by A2, CONNSP_2:def 1;

      take U;

      ((( - 1) * ( - 1)) * ( Int V1)) = ( Int V1) by CONVEX1: 32;

      then

       A5: (( - 1) * (( - 1) * ( Int V1))) = ( Int V1) by CONVEX1: 37;

      ((( - 1) * ( - 1)) * ( Int V2)) = ( Int V2) by CONVEX1: 32;

      then

       A6: (( - 1) * (( - 1) * ( Int V2))) = ( Int V2) by CONVEX1: 37;

      

      thus U = ((( Int V1) /\ ( Int V2)) /\ ((( - 1) * ( Int V1)) /\ (( - 1) * ( Int V2)))) by XBOOLE_1: 16

      .= ((( - 1) * (( Int V1) /\ ( Int V2))) /\ (( Int V1) /\ ( Int V2))) by Th15

      .= ((( - 1) * (( Int V1) /\ ( Int V2))) /\ (( - 1) * ((( - 1) * ( Int V1)) /\ (( - 1) * ( Int V2))))) by A5, A6, Th15

      .= (( - 1) * ((( Int V1) /\ ( Int V2)) /\ ((( - 1) * ( Int V1)) /\ (( - 1) * ( Int V2))))) by Th15

      .= ( - U) by XBOOLE_1: 16;

      let x be object;

      assume x in (U + U);

      then x in { (u + v) where u,v be Point of X : u in U & v in U } by RUSUB_4:def 9;

      then

      consider u,v be Point of X such that

       A7: (u + v) = x and

       A8: u in U and

       A9: v in U;

      

       A10: U = ((( Int V1) /\ ( Int V2)) /\ ((( - 1) * ( Int V1)) /\ (( - 1) * ( Int V2)))) by XBOOLE_1: 16;

      then v in (( Int V1) /\ ( Int V2)) by A9, XBOOLE_0:def 4;

      then

       A11: v in ( Int V2) by XBOOLE_0:def 4;

      ( Int V1) c= V1 & ( Int V2) c= V2 by TOPS_1: 16;

      then

       A12: (( Int V1) + ( Int V2)) c= (V1 + V2) by Th11;

      u in (( Int V1) /\ ( Int V2)) by A8, A10, XBOOLE_0:def 4;

      then u in ( Int V1) by XBOOLE_0:def 4;

      then (u + v) in { (u9 + v9) where u9,v9 be Point of X : u9 in ( Int V1) & v9 in ( Int V2) } by A11;

      then (u + v) in (( Int V1) + ( Int V2)) by RUSUB_4:def 9;

      then (u + v) in (V1 + V2) by A12;

      hence thesis by A1, A7;

    end;

    theorem :: RLTOPSP1:57

    

     Th57: for X be LinearTopSpace, K be compact Subset of X, C be closed Subset of X st K misses C holds ex V be a_neighborhood of ( 0. X) st (K + V) misses (C + V)

    proof

      let X be LinearTopSpace, K be compact Subset of X, C be closed Subset of X such that

       A1: K misses C;

      per cases ;

        suppose

         A2: K = {} ;

        take V = ( [#] X);

        thus V is a_neighborhood of ( 0. X) by TOPGRP_1: 21;

        (K + V) = {} by A2, CONVEX1: 40;

        hence thesis;

      end;

        suppose

         A3: K <> {} ;

        set xV = { [x, Vx] where x be Point of X, Vx be open a_neighborhood of ( 0. X) : x in K & Vx is symmetric & (((x + Vx) + Vx) + Vx) misses C };

         A4:

        now

          let x be Point of X such that

           A5: x in K;

          (( - x) + (C ` )) = { (( - x) + u) where u be Point of X : u in (C ` ) } & K c= (C ` ) by A1, RUSUB_4:def 8, SUBSET_1: 23;

          then (( - x) + x) in (( - x) + (C ` )) by A5;

          then ( 0. X) in (( - x) + (C ` )) by RLVECT_1: 5;

          then (( - x) + (C ` )) is a_neighborhood of ( 0. X) by CONNSP_2: 3;

          then

          consider V9 be open a_neighborhood of ( 0. X) such that V9 is symmetric and

           A6: (V9 + V9) c= (( - x) + (C ` )) by Th56;

          consider Vx be open a_neighborhood of ( 0. X) such that

           A7: Vx is symmetric and

           A8: (Vx + Vx) c= V9 by Th56;

          take Vx;

          thus Vx is symmetric by A7;

          Vx c= V9

          proof

            let z be object;

            assume

             A9: z in Vx;

            then

            reconsider z as Point of X;

            ( 0. X) in Vx by CONNSP_2: 4;

            then (z + ( 0. X)) in (Vx + Vx) by A9, Th3;

            then z in (Vx + Vx);

            hence thesis by A8;

          end;

          then (Vx + (Vx + Vx)) c= (V9 + V9) by A8, Th11;

          then ((Vx + Vx) + Vx) c= (( - x) + (C ` )) by A6;

          then (x + ((Vx + Vx) + Vx)) c= (x + (( - x) + (C ` ))) by Th8;

          then ((x + Vx) + (Vx + Vx)) c= (x + (( - x) + (C ` ))) by Th7;

          then (((x + Vx) + Vx) + Vx) c= (x + (( - x) + (C ` ))) by CONVEX1: 36;

          then (((x + Vx) + Vx) + Vx) c= ((x + ( - x)) + (C ` )) by Th6;

          then (((x + Vx) + Vx) + Vx) c= (( 0. X) + (C ` )) by RLVECT_1:def 10;

          then (((x + Vx) + Vx) + Vx) c= (C ` ) by Th5;

          hence (((x + Vx) + Vx) + Vx) misses C by SUBSET_1: 23;

        end;

         A10:

        now

          consider x be object such that

           A11: x in K by A3, XBOOLE_0:def 1;

          reconsider x as Point of X by A11;

          consider Vx be open a_neighborhood of ( 0. X) such that

           A12: Vx is symmetric & (((x + Vx) + Vx) + Vx) misses C by A4, A11;

          take z = [x, Vx];

          thus z in xV by A11, A12;

        end;

        defpred P[ object, object] means ex v1,v2 be Point of X, V1,V2 be open a_neighborhood of ( 0. X) st $1 = [v1, V1] & $2 = [v2, V2] & (v1 + V1) = (v2 + V2);

        

         A13: for x,y,z be object st P[x, y] & P[y, z] holds P[x, z]

        proof

          let x,y,z be object;

          given v1,v2 be Point of X, V1,V2 be open a_neighborhood of ( 0. X) such that

           A14: x = [v1, V1] and

           A15: y = [v2, V2] and

           A16: (v1 + V1) = (v2 + V2);

          given w1,w2 be Point of X, W1,W2 be open a_neighborhood of ( 0. X) such that

           A17: y = [w1, W1] and

           A18: z = [w2, W2] & (w1 + W1) = (w2 + W2);

          take v1, w2, V1, W2;

          v2 = w1 by A15, A17, XTUPLE_0: 1;

          hence thesis by A14, A15, A16, A17, A18, XTUPLE_0: 1;

        end;

        reconsider xV as non empty set by A10;

        

         A19: for x be object st x in xV holds P[x, x]

        proof

          let x be object;

          assume x in xV;

          then ex v be Point of X, V be open a_neighborhood of ( 0. X) st x = [v, V] & v in K & V is symmetric & (((v + V) + V) + V) misses C;

          hence thesis;

        end;

        

         A20: for x,y be object st P[x, y] holds P[y, x];

        consider eqR be Equivalence_Relation of xV such that

         A21: for x,y be object holds [x, y] in eqR iff x in xV & y in xV & P[x, y] from EQREL_1:sch 1( A19, A20, A13);

        now

          let X be set;

          assume X in ( Class eqR);

          then ex x be object st x in xV & X = ( Class (eqR,x)) by EQREL_1:def 3;

          hence X <> {} by EQREL_1: 20;

        end;

        then

        consider g be Function such that

         A22: ( dom g) = ( Class eqR) and

         A23: for X be set st X in ( Class eqR) holds (g . X) in X by FUNCT_1: 111;

        set xVV = ( rng g);

        set F = { (x + Vx) where x be Point of X, Vx be open a_neighborhood of ( 0. X) : [x, Vx] in xVV };

        F c= ( bool the carrier of X)

        proof

          let A be object;

          assume A in F;

          then ex x be Point of X, Vx be open a_neighborhood of ( 0. X) st A = (x + Vx) & [x, Vx] in xVV;

          hence thesis;

        end;

        then

        reconsider F as Subset-Family of X;

        

         A24: F is Cover of K

        proof

          let x be object;

          assume

           A25: x in K;

          then

          reconsider x as Point of X;

          consider Vx be open a_neighborhood of ( 0. X) such that

           A26: Vx is symmetric & (((x + Vx) + Vx) + Vx) misses C by A4, A25;

           [x, Vx] in xV by A25, A26;

          then

           A27: ( Class (eqR, [x, Vx])) in ( Class eqR) by EQREL_1:def 3;

          then

           A28: (g . ( Class (eqR, [x, Vx]))) in xVV by A22, FUNCT_1:def 3;

          (x + ( 0. X)) in (x + Vx) by Lm1, CONNSP_2: 4;

          then

           A29: x in (x + Vx);

          (g . ( Class (eqR, [x, Vx]))) in ( Class (eqR, [x, Vx])) by A23, A27;

          then [(g . ( Class (eqR, [x, Vx]))), [x, Vx]] in eqR by EQREL_1: 19;

          then

          consider v1,v2 be Point of X, V1,V2 be open a_neighborhood of ( 0. X) such that

           A30: (g . ( Class (eqR, [x, Vx]))) = [v1, V1] and

           A31: [x, Vx] = [v2, V2] and

           A32: (v1 + V1) = (v2 + V2) by A21;

          x = v2 & Vx = V2 by A31, XTUPLE_0: 1;

          then (x + Vx) in F by A30, A32, A28;

          hence thesis by A29, TARSKI:def 4;

        end;

        F is open

        proof

          let P be Subset of X;

          assume P in F;

          then ex x be Point of X, Vx be open a_neighborhood of ( 0. X) st P = (x + Vx) & [x, Vx] in xVV;

          hence thesis;

        end;

        then

        consider G be Subset-Family of X such that

         A33: G c= F and

         A34: G is Cover of K and

         A35: G is finite by A24, COMPTS_1:def 4;

        set FVx = { Vx where Vx be open a_neighborhood of ( 0. X) : ex x be Point of X st (x + Vx) in G & [x, Vx] in xVV };

        FVx c= ( bool the carrier of X)

        proof

          let A be object;

          assume A in FVx;

          then ex Vx be open a_neighborhood of ( 0. X) st A = Vx & ex x be Point of X st (x + Vx) in G & [x, Vx] in xVV;

          hence thesis;

        end;

        then

        reconsider FVx as Subset-Family of X;

        defpred P[ object, object] means ex x be Point of X, Vx be open a_neighborhood of ( 0. X) st $1 = (x + Vx) & (x + Vx) in G & [x, Vx] in xVV & $2 = Vx;

        

         A36: for x be object st x in G holds ex y be object st y in FVx & P[x, y]

        proof

          let x be object;

          assume

           A37: x in G;

          then x in F by A33;

          then

          consider z be Point of X, Vz be open a_neighborhood of ( 0. X) such that

           A38: x = (z + Vz) & [z, Vz] in xVV;

          take Vz;

          thus thesis by A37, A38;

        end;

        consider f be Function of G, FVx such that

         A39: for x be object st x in G holds P[x, (f . x)] from FUNCT_2:sch 1( A36);

        set FxVxVx = { ((x + Vx) + Vx) where x be Point of X, Vx be open a_neighborhood of ( 0. X) : (x + Vx) in G & [x, Vx] in xVV };

        take V = ( meet FVx);

        

         A40: ( rng g) c= xV

        proof

          let x be object;

          assume x in ( rng g);

          then

          consider y be object such that

           A41: y in ( dom g) and

           A42: x = (g . y) by FUNCT_1:def 3;

          reconsider y as set by TARSKI: 1;

          x in y by A22, A23, A41, A42;

          hence thesis by A22, A41;

        end;

        

         A43: for A be Subset of X st A in G holds ex x be Point of X, Vx be open a_neighborhood of ( 0. X) st A = (x + Vx) & [x, Vx] in xVV

        proof

          let A be Subset of X;

          assume A in G;

          then A in F by A33;

          hence thesis;

        end;

         A44:

        now

          consider y be Point of X such that

           A45: y in K by A3, SUBSET_1: 4;

          consider W be Subset of X such that y in W and

           A46: W in G by A34, A45, Th2;

          consider x be Point of X, Vx be open a_neighborhood of ( 0. X) such that

           A47: W = (x + Vx) & [x, Vx] in xVV by A43, A46;

          Vx in FVx by A46, A47;

          hence ex z be set st z in FVx;

        end;

        then

         A48: ( dom f) = G by FUNCT_2:def 1;

        

         A49: FVx c= ( rng f)

        proof

          let z be object;

          assume z in FVx;

          then

          consider Vx be open a_neighborhood of ( 0. X) such that

           A50: z = Vx and

           A51: ex x be Point of X st (x + Vx) in G & [x, Vx] in xVV;

          consider x be Point of X such that

           A52: (x + Vx) in G and

           A53: [x, Vx] in xVV by A51;

          consider v be Point of X, Vv be open a_neighborhood of ( 0. X) such that

           A54: (x + Vx) = (v + Vv) and (v + Vv) in G and

           A55: [v, Vv] in xVV and

           A56: (f . (x + Vx)) = Vv by A39, A52;

           [ [x, Vx], [v, Vv]] in eqR by A21, A40, A53, A54, A55;

          then [x, Vx] in ( Class (eqR, [v, Vv])) by EQREL_1: 19;

          then

           A57: ( Class (eqR, [v, Vv])) = ( Class (eqR, [x, Vx])) by A40, A55, EQREL_1: 23;

          consider A be object such that

           A58: A in ( dom g) and

           A59: [x, Vx] = (g . A) by A53, FUNCT_1:def 3;

          consider a be object such that

           A60: a in xV and

           A61: A = ( Class (eqR,a)) by A22, A58, EQREL_1:def 3;

           [x, Vx] in ( Class (eqR,a)) by A22, A23, A58, A59, A61;

          then

           A62: ( Class (eqR,a)) = ( Class (eqR, [x, Vx])) by A60, EQREL_1: 23;

          consider B be object such that

           A63: B in ( dom g) and

           A64: [v, Vv] = (g . B) by A55, FUNCT_1:def 3;

          consider b be object such that

           A65: b in xV and

           A66: B = ( Class (eqR,b)) by A22, A63, EQREL_1:def 3;

           [v, Vv] in ( Class (eqR,b)) by A22, A23, A63, A64, A66;

          then [x, Vx] = [v, Vv] by A57, A59, A64, A61, A65, A66, A62, EQREL_1: 23;

          then Vx = Vv by XTUPLE_0: 1;

          hence thesis by A48, A50, A52, A56, FUNCT_1: 3;

        end;

        

         A67: for x be Point of X, Vx be open a_neighborhood of ( 0. X) st (x + Vx) in G & [x, Vx] in xVV holds x in K & Vx is symmetric & (((x + Vx) + Vx) + Vx) misses C

        proof

          let x be Point of X, Vx be open a_neighborhood of ( 0. X) such that

           A68: (x + Vx) in G and

           A69: [x, Vx] in xVV;

          consider A be object such that

           A70: A in ( dom g) and

           A71: [x, Vx] = (g . A) by A69, FUNCT_1:def 3;

          consider a be object such that

           A72: a in xV and

           A73: A = ( Class (eqR,a)) by A22, A70, EQREL_1:def 3;

           [x, Vx] in ( Class (eqR,a)) by A22, A23, A70, A71, A73;

          then

           A74: ( Class (eqR,a)) = ( Class (eqR, [x, Vx])) by A72, EQREL_1: 23;

          (x + Vx) in F by A33, A68;

          then

          consider v be Point of X, Vv be open a_neighborhood of ( 0. X) such that

           A75: (x + Vx) = (v + Vv) and

           A76: [v, Vv] in xVV;

           [ [x, Vx], [v, Vv]] in eqR by A21, A40, A69, A75, A76;

          then [x, Vx] in ( Class (eqR, [v, Vv])) by EQREL_1: 19;

          then

           A77: ( Class (eqR, [v, Vv])) = ( Class (eqR, [x, Vx])) by A40, A76, EQREL_1: 23;

          consider B be object such that

           A78: B in ( dom g) and

           A79: [v, Vv] = (g . B) by A76, FUNCT_1:def 3;

          consider b be object such that

           A80: b in xV and

           A81: B = ( Class (eqR,b)) by A22, A78, EQREL_1:def 3;

           [v, Vv] in ( Class (eqR,b)) by A22, A23, A78, A79, A81;

          then

           A82: [x, Vx] = [v, Vv] by A77, A71, A79, A73, A80, A81, A74, EQREL_1: 23;

          then

           A83: Vx = Vv by XTUPLE_0: 1;

           [v, Vv] in xV by A40, A76;

          then

          consider u be Point of X, Vu be open a_neighborhood of ( 0. X) such that

           A84: [u, Vu] = [v, Vv] and

           A85: u in K & Vu is symmetric & (((u + Vu) + Vu) + Vu) misses C;

          Vv = Vu by A84, XTUPLE_0: 1;

          hence thesis by A84, A85, A82, A83, XTUPLE_0: 1;

        end;

        now

          let Z be set;

          hereby

            reconsider A = (C + V) as set;

            assume Z in { {} };

            then

             A86: Z = {} by TARSKI:def 1;

            consider y be Point of X such that

             A87: y in K by A3, SUBSET_1: 4;

            consider W be Subset of X such that y in W and

             A88: W in G by A34, A87, Th2;

            consider x be Point of X, Vx be open a_neighborhood of ( 0. X) such that

             A89: W = (x + Vx) & [x, Vx] in xVV by A43, A88;

            

             A90: (((x + Vx) + Vx) + Vx) misses C by A67, A88, A89;

            reconsider B = ((x + Vx) + Vx) as set;

            take A, B;

            thus A in {(C + V)} by TARSKI:def 1;

            thus B in FxVxVx by A88, A89;

            

             A91: Vx is symmetric by A67, A88, A89;

            now

              

               A92: (C + V) = { (u + v) where u,v be Point of X : u in C & v in V } by RUSUB_4:def 9;

              assume A meets B;

              then

              consider z be object such that

               A93: z in A and

               A94: z in B by XBOOLE_0: 3;

              reconsider z as Point of X by A93;

              consider u,v be Point of X such that

               A95: z = (u + v) and

               A96: u in C and

               A97: v in V by A93, A92;

              Vx in FVx by A88, A89;

              then v in Vx by A97, SETFAM_1:def 1;

              then ( - v) in Vx by A91, Th25;

              then

               A98: (z + ( - v)) in (((x + Vx) + Vx) + Vx) by A94, Th3;

              (z + ( - v)) = (u + (v + ( - v))) by A95, RLVECT_1:def 3

              .= (u + ( 0. X)) by RLVECT_1: 5

              .= u;

              hence contradiction by A90, A96, A98, XBOOLE_0: 3;

            end;

            hence Z = (A /\ B) by A86;

          end;

          given A,B be set such that

           A99: A in {(C + V)} and

           A100: B in FxVxVx and

           A101: Z = (A /\ B);

          

           A102: A = (C + V) by A99, TARSKI:def 1;

          consider x be Point of X, Vx be open a_neighborhood of ( 0. X) such that

           A103: B = ((x + Vx) + Vx) and

           A104: (x + Vx) in G & [x, Vx] in xVV by A100;

          

           A105: (((x + Vx) + Vx) + Vx) misses C by A67, A104;

          

           A106: Vx is symmetric by A67, A104;

          now

            

             A107: (C + V) = { (u + v) where u,v be Point of X : u in C & v in V } by RUSUB_4:def 9;

            assume A meets B;

            then

            consider z be object such that

             A108: z in A and

             A109: z in B by XBOOLE_0: 3;

            reconsider z as Point of X by A99, A108;

            consider u,v be Point of X such that

             A110: z = (u + v) and

             A111: u in C and

             A112: v in V by A102, A108, A107;

            Vx in FVx by A104;

            then v in Vx by A112, SETFAM_1:def 1;

            then ( - v) in Vx by A106, Th25;

            then

             A113: (z + ( - v)) in (((x + Vx) + Vx) + Vx) by A103, A109, Th3;

            (z + ( - v)) = (u + (v + ( - v))) by A110, RLVECT_1:def 3

            .= (u + ( 0. X)) by RLVECT_1: 5

            .= u;

            hence contradiction by A105, A111, A113, XBOOLE_0: 3;

          end;

          then (A /\ B) = {} ;

          hence Z in { {} } by A101, TARSKI:def 1;

        end;

        then ( INTERSECTION ( {(C + V)},FxVxVx)) = { {} } by SETFAM_1:def 5;

        then ( union ( INTERSECTION ( {(C + V)},FxVxVx))) = {} by ZFMISC_1: 25;

        then ((C + V) /\ ( union FxVxVx)) = {} by SETFAM_1: 25;

        then

         A114: (C + V) misses ( union FxVxVx);

        

         A115: FVx is open

        proof

          let P be Subset of X;

          assume P in FVx;

          then ex Vx be open a_neighborhood of ( 0. X) st P = Vx & ex x be Point of X st (x + Vx) in G & [x, Vx] in xVV;

          hence thesis;

        end;

        (f " FVx) is finite by A35, FINSET_1: 1;

        then FVx is finite by A49, FINSET_1: 9;

        then V is open by A115, TOPS_2: 20;

        then

         A116: ( Int V) = V by TOPS_1: 23;

        now

          let A be set;

          assume

           A117: A in FVx;

          then

          reconsider A9 = A as Subset of X;

          ex Vx be open a_neighborhood of ( 0. X) st A = Vx & ex x be Point of X st (x + Vx) in G & [x, Vx] in xVV by A117;

          then ( Int A9) c= A9 & ( 0. X) in ( Int A9) by CONNSP_2:def 1, TOPS_1: 16;

          hence ( 0. X) in A;

        end;

        then ( 0. X) in V by A44, SETFAM_1:def 1;

        hence V is a_neighborhood of ( 0. X) by A116, CONNSP_2:def 1;

        set FxVxV = { ((x + Vx) + V) where x be Point of X, Vx be open a_neighborhood of ( 0. X) : (x + Vx) in G & [x, Vx] in xVV };

        

         A118: ( union FxVxV) c= ( union FxVxVx)

        proof

          let z be object;

          assume z in ( union FxVxV);

          then

          consider Y be set such that

           A119: z in Y and

           A120: Y in FxVxV by TARSKI:def 4;

          consider x be Point of X, Vx be open a_neighborhood of ( 0. X) such that

           A121: Y = ((x + Vx) + V) and

           A122: (x + Vx) in G & [x, Vx] in xVV by A120;

          

           A123: ((x + Vx) + Vx) in FxVxVx by A122;

          ((x + Vx) + V) = { (u + v) where u,v be Point of X : u in (x + Vx) & v in V } by RUSUB_4:def 9;

          then

          consider u,v be Point of X such that

           A124: z = (u + v) and

           A125: u in (x + Vx) and

           A126: v in V by A119, A121;

          Vx in FVx by A122;

          then v in Vx by A126, SETFAM_1:def 1;

          then (u + v) in ((x + Vx) + Vx) by A125, Th3;

          hence thesis by A124, A123, TARSKI:def 4;

        end;

        (K + V) c= ( union FxVxV)

        proof

          let z be object;

          

           A127: (K + V) = { (u + v) where u,v be Point of X : u in K & v in V } by RUSUB_4:def 9;

          assume z in (K + V);

          then

          consider u,v be Point of X such that

           A128: z = (u + v) and

           A129: u in K and

           A130: v in V by A127;

          consider Vu be Subset of X such that

           A131: u in Vu and

           A132: Vu in G by A34, A129, Th2;

          consider x be Point of X, Vx be open a_neighborhood of ( 0. X) such that

           A133: Vu = (x + Vx) and

           A134: [x, Vx] in xVV by A43, A132;

          

           A135: ((x + Vx) + V) in FxVxV by A132, A133, A134;

          z in ((x + Vx) + V) by A128, A130, A131, A133, Th3;

          hence thesis by A135, TARSKI:def 4;

        end;

        hence thesis by A118, A114, XBOOLE_1: 1, XBOOLE_1: 63;

      end;

    end;

    theorem :: RLTOPSP1:58

    

     Th58: for X be LinearTopSpace, B be local_base of X, V be a_neighborhood of ( 0. X) holds ex W be a_neighborhood of ( 0. X) st W in B & ( Cl W) c= V

    proof

      let X be LinearTopSpace, B be local_base of X;

      let V be a_neighborhood of ( 0. X);

      set C = (( Int V) ` );

      set K = {( 0. X)};

      ( 0. X) in ( Int V) by CONNSP_2:def 1;

      then not ( 0. X) in (( Int V) ` ) by XBOOLE_0:def 5;

      then

      consider P be a_neighborhood of ( 0. X) such that

       A1: (K + P) misses (C + P) by Th57, ZFMISC_1: 50;

      

       A2: ( 0. X) in ( Int P) by CONNSP_2:def 1;

      then

      reconsider P9 = ( Int P) as open a_neighborhood of ( 0. X) by CONNSP_2: 3;

      (K + P9) c= (K + P) & (C + P9) c= (C + P) by Lm3, TOPS_1: 16;

      then (K + P9) misses (C + P9) by A1, XBOOLE_1: 64;

      then ( Cl (K + P9)) misses (C + P9) by TSEP_1: 36;

      then ( Cl (K + P9)) misses C by A2, Th12, XBOOLE_1: 63;

      then ( Cl P9) misses C by CONVEX1: 35;

      then

       A3: ( Cl P9) c= ( Int V) by SUBSET_1: 24;

      consider W be a_neighborhood of ( 0. X) such that

       A4: W in B and

       A5: W c= P9 by YELLOW13:def 2;

      take W;

      thus W in B by A4;

      

       A6: ( Cl W) c= ( Cl P9) by A5, PRE_TOPC: 19;

      ( Int V) c= V by TOPS_1: 16;

      then ( Cl P9) c= V by A3;

      hence thesis by A6;

    end;

    theorem :: RLTOPSP1:59

    

     Th59: for X be LinearTopSpace, V be a_neighborhood of ( 0. X) holds ex W be a_neighborhood of ( 0. X) st ( Cl W) c= V

    proof

      let X be LinearTopSpace, V be a_neighborhood of ( 0. X);

      set B = the set of all U where U be a_neighborhood of ( 0. X);

      B c= ( bool the carrier of X)

      proof

        let A be object;

        assume A in B;

        then ex U be a_neighborhood of ( 0. X) st A = U;

        hence thesis;

      end;

      then B is local_base of X by Th44;

      then

      consider W be a_neighborhood of ( 0. X) such that W in B and

       A1: ( Cl W) c= V by Th58;

      take W;

      thus thesis by A1;

    end;

    registration

      cluster T_1 -> Hausdorff for LinearTopSpace;

      coherence

      proof

        let X be LinearTopSpace;

        assume

         A1: X is T_1;

        let p,q be Point of X;

        assume

         A2: p <> q;

         {q} is closed by A1, URYSOHN1: 19;

        then

        consider V be a_neighborhood of ( 0. X) such that

         A3: ( {p} + V) misses ( {q} + V) by A2, Th57, ZFMISC_1: 11;

        take (p + ( Int V)), (q + ( Int V));

        

         A4: ( {p} + V) = (p + V) & ( {q} + V) = (q + V) by RUSUB_4: 33;

        thus (p + ( Int V)) is open & (q + ( Int V)) is open;

        ( 0. X) in ( Int V) by CONNSP_2:def 1;

        then (p + ( 0. X)) in (p + ( Int V)) & (q + ( 0. X)) in (q + ( Int V)) by Lm1;

        hence p in (p + ( Int V)) & q in (q + ( Int V));

        (p + ( Int V)) c= (p + V) & (q + ( Int V)) c= (q + V) by Th8, TOPS_1: 16;

        hence thesis by A3, A4, XBOOLE_1: 64;

      end;

    end

    theorem :: RLTOPSP1:60

    for X be LinearTopSpace, A be Subset of X holds ( Cl A) = ( meet the set of all (A + V) where V be a_neighborhood of ( 0. X))

    proof

      let X be LinearTopSpace, A be Subset of X;

      set AV = the set of all (A + V) where V be a_neighborhood of ( 0. X);

      set V = the a_neighborhood of ( 0. X);

      

       A1: for x be Point of X, V be a_neighborhood of ( 0. X) holds A meets (x + ( Int V)) iff x in (A + (( - 1) * ( Int V)))

      proof

        let x be Point of X, V be a_neighborhood of ( 0. X);

        

         A2: (A + (( - 1) * ( Int V))) = { (a + v) where a,v be Point of X : a in A & v in (( - 1) * ( Int V)) } by RUSUB_4:def 9;

        hereby

          assume A meets (x + ( Int V));

          then x in (A + ( - ( Int V))) by Th24;

          hence x in (A + (( - 1) * ( Int V)));

        end;

        assume x in (A + (( - 1) * ( Int V)));

        then

        consider a,v be Point of X such that

         A3: x = (a + v) and

         A4: a in A and

         A5: v in (( - 1) * ( Int V)) by A2;

        consider v9 be Point of X such that

         A6: v = (( - 1) * v9) and

         A7: v9 in ( Int V) by A5;

        ( - v) = (( - 1) * v) by RLVECT_1: 16

        .= ((( - 1) * ( - 1)) * v9) by A6, RLVECT_1:def 7

        .= v9 by RLVECT_1:def 8;

        

        then

         A8: (x + v9) = (a + (v + ( - v))) by A3, RLVECT_1:def 3

        .= (a + ( 0. X)) by RLVECT_1: 5

        .= a;

        (x + ( Int V)) = { (x + w) where w be Point of X : w in ( Int V) } by RUSUB_4:def 8;

        then (x + v9) in (x + ( Int V)) by A7;

        hence thesis by A4, A8, XBOOLE_0: 3;

      end;

      AV c= ( bool the carrier of X)

      proof

        let x be object;

        assume x in AV;

        then ex V be a_neighborhood of ( 0. X) st x = (A + V);

        hence thesis;

      end;

      then

      reconsider AV9 = AV as Subset-Family of X;

      

       A9: for x be Point of X holds x in ( Cl A) iff for V be a_neighborhood of ( 0. X) holds A meets (x + ( Int V))

      proof

        let x be Point of X;

        hereby

          assume

           A10: x in ( Cl A);

          let V be a_neighborhood of ( 0. X);

          ( 0. X) in ( Int V) by CONNSP_2:def 1;

          then (x + ( 0. X)) in (x + ( Int V)) by Lm1;

          then x in (x + ( Int V));

          hence A meets (x + ( Int V)) by A10, TOPS_1: 12;

        end;

        assume

         A11: for V be a_neighborhood of ( 0. X) holds A meets (x + ( Int V));

        now

          let V be Subset of X such that

           A12: V is open and

           A13: x in V;

          

           A14: ( Int (( - x) + V)) = (( - x) + V) by A12, TOPS_1: 23;

          (( - x) + x) in (( - x) + V) by A13, Lm1;

          then ( 0. X) in (( - x) + V) by RLVECT_1: 5;

          then (( - x) + V) is a_neighborhood of ( 0. X) by A14, CONNSP_2:def 1;

          then A meets (x + (( - x) + V)) by A11, A14;

          then A meets ((x + ( - x)) + V) by Th6;

          then A meets (( 0. X) + V) by RLVECT_1: 5;

          hence A meets V by Th5;

        end;

        hence thesis by TOPS_1: 12;

      end;

      

       A15: (A + V) in AV;

      thus ( Cl A) c= ( meet AV)

      proof

        let x be object;

        assume

         A16: x in ( Cl A);

        then

        reconsider x as Point of X;

        now

          let Y be set;

          assume Y in AV;

          then

          consider V be a_neighborhood of ( 0. X) such that

           A17: Y = (A + V);

          

           A18: (A + V) = { (a + v) where a,v be Point of X : a in A & v in V } by RUSUB_4:def 9;

          

           A19: (( - 1) * V) is a_neighborhood of ( 0. X) by Th55;

          then A meets (x + ( Int (( - 1) * V))) by A9, A16;

          then (A + (( - 1) * ( Int (( - 1) * V)))) = { (a + v) where a,v be Point of X : a in A & v in (( - 1) * ( Int (( - 1) * V))) } & x in (A + (( - 1) * ( Int (( - 1) * V)))) by A1, A19, RUSUB_4:def 9;

          then

          consider a,v be Point of X such that

           A20: x = (a + v) & a in A and

           A21: v in (( - 1) * ( Int (( - 1) * V)));

          consider v9 be Point of X such that

           A22: v = (( - 1) * v9) and

           A23: v9 in ( Int (( - 1) * V)) by A21;

          ( Int (( - 1) * V)) c= (( - 1) * V) by TOPS_1: 16;

          then v9 in (( - 1) * V) by A23;

          then

          consider v99 be Point of X such that

           A24: v9 = (( - 1) * v99) and

           A25: v99 in V;

          v = ((( - 1) * ( - 1)) * v99) by A22, A24, RLVECT_1:def 7

          .= v99 by RLVECT_1:def 8;

          hence x in Y by A17, A18, A20, A25;

        end;

        hence thesis by A15, SETFAM_1:def 1;

      end;

      let x be object;

      assume

       A26: x in ( meet AV);

      ( meet AV9) c= the carrier of X;

      then

      reconsider x as Point of X by A26;

      now

        let V be a_neighborhood of ( 0. X);

        ( 0. X) in ( Int V) by CONNSP_2:def 1;

        then ( Int V) is a_neighborhood of ( 0. X) by CONNSP_2: 3;

        then (( - 1) * ( Int V)) is a_neighborhood of ( 0. X) by Th55;

        then (A + (( - 1) * ( Int V))) in AV;

        then x in (A + (( - 1) * ( Int V))) by A26, SETFAM_1:def 1;

        hence A meets (x + ( Int V)) by A1;

      end;

      hence thesis by A9;

    end;

    theorem :: RLTOPSP1:61

    

     Th61: for X be LinearTopSpace, A,B be Subset of X holds (( Int A) + ( Int B)) c= ( Int (A + B))

    proof

      let X be LinearTopSpace, A,B be Subset of X;

      ( Int A) c= A & ( Int B) c= B by TOPS_1: 16;

      then (( Int A) + ( Int B)) c= (A + B) by Th11;

      hence thesis by TOPS_1: 24;

    end;

    theorem :: RLTOPSP1:62

    

     Th62: for X be LinearTopSpace, A,B be Subset of X holds (( Cl A) + ( Cl B)) c= ( Cl (A + B))

    proof

      let X be LinearTopSpace, A,B be Subset of X;

      let z be object;

      assume

       A1: z in (( Cl A) + ( Cl B));

      then

      reconsider z as Point of X;

      { (u + v) where u,v be Point of X : u in ( Cl A) & v in ( Cl B) } = (( Cl A) + ( Cl B)) by RUSUB_4:def 9;

      then

      consider a,b be Point of X such that

       A2: z = (a + b) and

       A3: a in ( Cl A) and

       A4: b in ( Cl B) by A1;

      now

        let W be Subset of X such that

         A5: W is open and

         A6: z in W;

        W is a_neighborhood of z by A5, A6, CONNSP_2: 3;

        then

        consider W1 be a_neighborhood of a, W2 be a_neighborhood of b such that

         A7: (W1 + W2) c= W by A2, Th31;

        a in ( Int W1) by CONNSP_2:def 1;

        then A meets ( Int W1) by A3, TOPS_1: 12;

        then

        consider x be object such that

         A8: x in A and

         A9: x in ( Int W1) by XBOOLE_0: 3;

        reconsider x as Point of X by A8;

        

         A10: (( Int W1) + ( Int W2)) c= ( Int W) by A7, Th36;

        b in ( Int W2) by CONNSP_2:def 1;

        then B meets ( Int W2) by A4, TOPS_1: 12;

        then

        consider y be object such that

         A11: y in B and

         A12: y in ( Int W2) by XBOOLE_0: 3;

        reconsider y as Point of X by A11;

        (x + y) in (A + B) & (x + y) in (( Int W1) + ( Int W2)) by A8, A9, A11, A12, Th3;

        then (A + B) meets ( Int W) by A10, XBOOLE_0: 3;

        hence (A + B) meets W by A5, TOPS_1: 23;

      end;

      hence thesis by TOPS_1: 12;

    end;

    

     Lm16: for X be LinearTopSpace, C be convex Subset of X holds ( Cl C) is convex

    proof

      let X be LinearTopSpace, C be convex Subset of X;

      now

        let r be Real such that

         A1: 0 < r and

         A2: r < 1;

        ((r * C) + ((1 - r) * C)) c= C by A1, A2, CONVEX1: 4;

        then

         A3: ( Cl ((r * C) + ((1 - r) * C))) c= ( Cl C) by PRE_TOPC: 19;

        ( 0 + r) < 1 by A2;

        then 0 < (1 - r) by XREAL_1: 20;

        then

         A4: ((1 - r) * ( Cl C)) = ( Cl ((1 - r) * C)) by Th52;

        

         A5: (( Cl (r * C)) + ( Cl ((1 - r) * C))) c= ( Cl ((r * C) + ((1 - r) * C))) by Th62;

        ( Cl (r * C)) = (r * ( Cl C)) by A1, Th52;

        hence ((r * ( Cl C)) + ((1 - r) * ( Cl C))) c= ( Cl C) by A3, A5, A4;

      end;

      hence thesis by CONVEX1: 4;

    end;

    registration

      let X be LinearTopSpace, C be convex Subset of X;

      cluster ( Cl C) -> convex;

      coherence by Lm16;

    end

    

     Lm17: for X be LinearTopSpace, C be convex Subset of X holds ( Int C) is convex

    proof

      let X be LinearTopSpace, C be convex Subset of X;

      now

        let r be Real such that

         A1: 0 < r and

         A2: r < 1;

        ((r * C) + ((1 - r) * C)) c= C by A1, A2, CONVEX1: 4;

        then

         A3: ( Int ((r * C) + ((1 - r) * C))) c= ( Int C) by TOPS_1: 19;

        ( 0 + r) < 1 by A2;

        then 0 < (1 - r) by XREAL_1: 20;

        then

         A4: ((1 - r) * ( Int C)) = ( Int ((1 - r) * C)) by Th51;

        

         A5: (( Int (r * C)) + ( Int ((1 - r) * C))) c= ( Int ((r * C) + ((1 - r) * C))) by Th61;

        ( Int (r * C)) = (r * ( Int C)) by A1, Th51;

        hence ((r * ( Int C)) + ((1 - r) * ( Int C))) c= ( Int C) by A3, A5, A4;

      end;

      hence thesis by CONVEX1: 4;

    end;

    registration

      let X be LinearTopSpace, C be convex Subset of X;

      cluster ( Int C) -> convex;

      coherence by Lm17;

    end

    

     Lm18: for X be LinearTopSpace, B be circled Subset of X holds ( Cl B) is circled

    proof

      let X be LinearTopSpace, B be circled Subset of X;

      let r be Real such that

       A1: |.r.| <= 1;

      per cases ;

        suppose

         A2: r = 0 ;

        now

          per cases ;

            suppose B = ( {} X);

            then ( Cl B) = ( {} X) by PRE_TOPC: 22;

            hence thesis by CONVEX1: 33;

          end;

            suppose

             A3: B <> ( {} X);

            

             A4: B c= ( Cl B) by PRE_TOPC: 18;

            

             A5: ( 0. X) in B by A3, Th27;

            then (r * ( Cl B)) = {( 0. X)} by A2, A4, CONVEX1: 34;

            hence thesis by A5, A4, ZFMISC_1: 31;

          end;

        end;

        hence thesis;

      end;

        suppose

         A6: r <> 0 ;

        (r * B) c= B by A1, Def6;

        then ( Cl (r * B)) c= ( Cl B) by PRE_TOPC: 19;

        hence thesis by A6, Th52;

      end;

    end;

    registration

      let X be LinearTopSpace, B be circled Subset of X;

      cluster ( Cl B) -> circled;

      coherence by Lm18;

    end

    theorem :: RLTOPSP1:63

    for X be LinearTopSpace, B be circled Subset of X st ( 0. X) in ( Int B) holds ( Int B) is circled

    proof

      let X be LinearTopSpace, B be circled Subset of X such that

       A1: ( 0. X) in ( Int B);

      let r be Real;

      assume |.r.| <= 1;

      then (r * B) c= B by Def6;

      then

       A2: ( Int (r * B)) c= ( Int B) by TOPS_1: 19;

      per cases ;

        suppose r = 0 ;

        then (r * ( Int B)) = {( 0. X)} by A1, CONVEX1: 34;

        hence thesis by A1, ZFMISC_1: 31;

      end;

        suppose r <> 0 ;

        hence thesis by A2, Th51;

      end;

    end;

    

     Lm19: for X be LinearTopSpace, E be bounded Subset of X holds ( Cl E) is bounded

    proof

      let X be LinearTopSpace, E be bounded Subset of X;

      let V be a_neighborhood of ( 0. X);

      consider W be a_neighborhood of ( 0. X) such that

       A1: ( Cl W) c= V by Th59;

      consider s such that

       A2: s > 0 and

       A3: for t st t > s holds E c= (t * W) by Def12;

      take s;

      thus s > 0 by A2;

      let t;

      assume t > s;

      then

       A4: ( Cl E) c= ( Cl (t * W)) & ( Cl (t * W)) = (t * ( Cl W)) by A2, A3, Th52, PRE_TOPC: 19;

      (t * ( Cl W)) c= (t * V) by A1, CONVEX1: 39;

      hence thesis by A4;

    end;

    registration

      let X be LinearTopSpace, E be bounded Subset of X;

      cluster ( Cl E) -> bounded;

      coherence by Lm19;

    end

    

     Lm20: for X be LinearTopSpace, U,V be a_neighborhood of ( 0. X), F be Subset-Family of X, r be positive Real st (for s be Real st |.s.| < r holds (s * V) c= U) & F = { (a * V) where a be Real : |.a.| < r } holds ( union F) is a_neighborhood of ( 0. X) & ( union F) is circled & ( union F) c= U

    proof

      let X be LinearTopSpace, U,V be a_neighborhood of ( 0. X), F be Subset-Family of X, r be positive Real such that

       A1: for s be Real st |.s.| < r holds (s * V) c= U and

       A2: F = { (a * V) where a be Real : |.a.| < r };

      set W = ( union F);

      thus W is a_neighborhood of ( 0. X)

      proof

        set F9 = { (a * ( Int V)) where a be non zero Real : |.a.| < r };

        consider a be Real such that

         A3: 0 < a and

         A4: a < r by XREAL_1: 5;

        reconsider a as Real;

        ( 0. X) in ( Int V) by CONNSP_2:def 1;

        then (a * ( 0. X)) in (a * ( Int V));

        then

         A5: ( 0. X) in (a * ( Int V));

        

         A6: F9 c= ( bool the carrier of X)

        proof

          let A be object;

          assume A in F9;

          then ex a be non zero Real st A = (a * ( Int V)) & |.a.| < r;

          hence thesis;

        end;

         |.a.| < r by A3, A4, ABSVALUE:def 1;

        then (a * ( Int V)) in F9 by A3;

        then

         A7: ( 0. X) in ( union F9) by A5, TARSKI:def 4;

        reconsider F9 as Subset-Family of X by A6;

        ( union F9) c= W

        proof

          let x be object;

          

           A8: ( Int V) c= V by TOPS_1: 16;

          assume x in ( union F9);

          then

          consider P be set such that

           A9: x in P and

           A10: P in F9 by TARSKI:def 4;

          consider a be non zero Real such that

           A11: P = (a * ( Int V)) and

           A12: |.a.| < r by A10;

          ex v be Point of X st x = (a * v) & v in ( Int V) by A9, A11;

          then

           A13: x in (a * V) by A8;

          (a * V) in F by A2, A12;

          hence thesis by A13, TARSKI:def 4;

        end;

        then

         A14: ( Int ( union F9)) c= ( Int W) by TOPS_1: 19;

        F9 is open

        proof

          let P be Subset of X;

          assume P in F9;

          then ex a be non zero Real st P = (a * ( Int V)) & |.a.| < r;

          hence thesis by Th49;

        end;

        then ( union F9) is open by TOPS_2: 19;

        then ( 0. X) in ( Int ( union F9)) by A7, TOPS_1: 23;

        hence ( 0. X) in ( Int W) by A14;

      end;

      thus W is circled

      proof

        let s be Real;

        assume |.s.| <= 1;

        then

         A15: ( |.s.| * r) <= r by XREAL_1: 153;

        let z be object;

        assume z in (s * W);

        then

        consider u be Point of X such that

         A16: z = (s * u) and

         A17: u in W;

        consider Y be set such that

         A18: u in Y and

         A19: Y in F by A17, TARSKI:def 4;

        consider a be Real such that

         A20: Y = (a * V) and

         A21: |.a.| < r by A2, A19;

        consider v be Point of X such that

         A22: u = (a * v) and

         A23: v in V by A18, A20;

        z = ((s * a) * v) by A16, A22, RLVECT_1:def 7;

        then

         A24: z in ((s * a) * V) by A23;

        per cases ;

          suppose 0 <> |.s.|;

          then s <> 0 by ABSVALUE: 2;

          then 0 < |.s.| by COMPLEX1: 47;

          then ( |.s.| * |.a.|) < ( |.s.| * r) by A21, XREAL_1: 68;

          then ( |.s.| * |.a.|) < r by A15, XXREAL_0: 2;

          then |.(s * a).| < r by COMPLEX1: 65;

          then ((s * a) * V) in F by A2;

          hence thesis by A24, TARSKI:def 4;

        end;

          suppose |.s.| = 0 ;

          then s = 0 by ABSVALUE: 2;

          then |.(s * a).| = 0 by ABSVALUE:def 1;

          then ((s * a) * V) in F by A2;

          hence thesis by A24, TARSKI:def 4;

        end;

      end;

      let z be object;

      assume

       A25: z in W;

      then

      reconsider z as Point of X;

      consider Y be set such that

       A26: z in Y and

       A27: Y in F by A25, TARSKI:def 4;

      consider a be Real such that

       A28: Y = (a * V) and

       A29: |.a.| < r by A2, A27;

      (a * V) c= U by A1, A29;

      hence thesis by A26, A28;

    end;

    theorem :: RLTOPSP1:64

    

     Th64: for X be LinearTopSpace, U be a_neighborhood of ( 0. X) holds ex W be a_neighborhood of ( 0. X) st W is circled & W c= U

    proof

      let X be LinearTopSpace, U be a_neighborhood of ( 0. X);

      ( 0. X) = ( 0 * ( 0. X));

      then

      consider r be positive Real, V be a_neighborhood of ( 0. X) such that

       A1: for s be Real st |.(s - 0 ).| < r holds (s * V) c= U by Th32;

      set F = { (a * V) where a be Real : |.a.| < r };

      F c= ( bool the carrier of X)

      proof

        let A be object;

        assume A in F;

        then ex a be Real st A = (a * V) & |.a.| < r;

        hence thesis;

      end;

      then

      reconsider F as Subset-Family of X;

      take ( union F);

      now

        let s be Real;

        assume |.s.| < r;

        then |.(s - 0 ).| < r;

        hence (s * V) c= U by A1;

      end;

      hence thesis by Lm20;

    end;

    theorem :: RLTOPSP1:65

    for X be LinearTopSpace, U be a_neighborhood of ( 0. X) st U is convex holds ex W be a_neighborhood of ( 0. X) st W is circled convex & W c= U

    proof

      let X be LinearTopSpace, U be a_neighborhood of ( 0. X) such that

       A1: U is convex;

      set V = (U /\ ( - U));

      ( - U) is a_neighborhood of ( 0. X) by Th55;

      then

      reconsider V as a_neighborhood of ( 0. X) by CONNSP_2: 2;

      take V;

      

       A2: ( - U) is convex by A1, CONVEX1: 1;

      thus V is circled

      proof

        ( 0. X) in V by CONNSP_2: 4;

        then

         A3: ( 0. X) in ( - U) by XBOOLE_0:def 4;

        

         A4: ( 0. X) in U by CONNSP_2: 4;

        let r be Real such that

         A5: |.r.| <= 1;

        let u be object;

        assume u in (r * V);

        then

        consider v be Point of X such that

         A6: u = (r * v) and

         A7: v in V;

        

         A8: v in ( - U) by A7, XBOOLE_0:def 4;

        

         A9: v in U by A7, XBOOLE_0:def 4;

        per cases ;

          suppose

           A10: r < 0 ;

          then

           A11: ( - r) <= 1 by A5, ABSVALUE:def 1;

          then ((( - r) * v) + ((1 - ( - r)) * ( 0. X))) in ( - U) by A2, A8, A3, A10;

          then ((( - r) * v) + ( 0. X)) in ( - U);

          then (( - r) * v) in ( - U);

          then

          consider u9 be Point of X such that

           A12: (( - r) * v) = (( - 1) * u9) and

           A13: u9 in U;

          ((( - r) * v) + ((1 - ( - r)) * ( 0. X))) in U by A1, A9, A4, A10, A11;

          then ((( - r) * v) + ( 0. X)) in U;

          then (( - r) * v) in U;

          then (( - 1) * ((( - 1) * r) * v)) in (( - 1) * U);

          then

           A14: ((( - 1) * (( - 1) * r)) * v) in (( - 1) * U) by RLVECT_1:def 7;

          u9 = ((( - 1) * ( - 1)) * u9) by RLVECT_1:def 8

          .= (( - 1) * (( - 1) * u9)) by RLVECT_1:def 7

          .= ((( - r) * ( - 1)) * v) by A12, RLVECT_1:def 7

          .= (r * v);

          hence thesis by A6, A13, A14, XBOOLE_0:def 4;

        end;

          suppose

           A15: r >= 0 ;

          

           A16: r <= 1 by A5, ABSVALUE:def 1;

          then ((r * v) + ((1 - r) * ( 0. X))) in ( - U) by A2, A8, A3, A15;

          then ((r * v) + ( 0. X)) in ( - U);

          then

           A17: (r * v) in ( - U);

          ((r * v) + ((1 - r) * ( 0. X))) in U by A1, A9, A4, A15, A16;

          then ((r * v) + ( 0. X)) in U;

          then (r * v) in U;

          hence thesis by A6, A17, XBOOLE_0:def 4;

        end;

      end;

      thus V is convex by A1, A2;

      thus thesis by XBOOLE_1: 17;

    end;

    theorem :: RLTOPSP1:66

    for X be LinearTopSpace holds ex P be local_base of X st P is circled-membered

    proof

      let X be LinearTopSpace;

      defpred P[ Subset of X] means $1 is circled;

      consider P be Subset-Family of X such that

       A1: for V be Subset of X holds V in P iff P[V] from SUBSET_1:sch 3;

      reconsider P as Subset-Family of X;

      take P;

      thus P is local_base of X

      proof

        let V be a_neighborhood of ( 0. X);

        consider W be a_neighborhood of ( 0. X) such that

         A2: W is circled and

         A3: W c= V by Th64;

        take W;

        thus W in P by A1, A2;

        thus thesis by A3;

      end;

      let V be Subset of X;

      assume V in P;

      hence thesis by A1;

    end;

    theorem :: RLTOPSP1:67

    for X be LinearTopSpace st X is locally-convex holds ex P be local_base of X st P is convex-membered;

    begin

    reserve V for RealLinearSpace,

v,w for Point of V;

    theorem :: RLTOPSP1:68

    

     Th68: v in ( LSeg (v,w))

    proof

      v = ((1 - 0 ) * v) by RLVECT_1:def 8

      .= (((1 - 0 ) * v) + ( 0. V))

      .= (((1 - 0 ) * v) + ( 0 * w)) by RLVECT_1: 10;

      hence thesis;

    end;

    theorem :: RLTOPSP1:69

    ((1 / 2) * (v + w)) in ( LSeg (v,w))

    proof

      ((1 / 2) * (v + w)) = (((1 - (1 / 2)) * v) + ((1 / 2) * w)) by RLVECT_1:def 5;

      hence thesis;

    end;

    theorem :: RLTOPSP1:70

    ( LSeg (v,v)) = {v}

    proof

      thus ( LSeg (v,v)) c= {v}

      proof

        let a be object;

        assume a in ( LSeg (v,v));

        then

        consider r such that

         A1: a = (((1 - r) * v) + (r * v)) and 0 <= r and r <= 1;

        a = (((1 - r) + r) * v) by A1, RLVECT_1:def 6

        .= v by RLVECT_1:def 8;

        hence thesis by TARSKI:def 1;

      end;

      v in ( LSeg (v,v)) by Th68;

      hence thesis by ZFMISC_1: 31;

    end;

    theorem :: RLTOPSP1:71

    ( 0. V) in ( LSeg (v,w)) implies ex r st v = (r * w) or w = (r * v)

    proof

      assume ( 0. V) in ( LSeg (v,w));

      then

      consider s be Real such that

       A1: ( 0. V) = (((1 - s) * v) + (s * w)) and 0 <= s and s <= 1;

      ( - (s * w)) = ((1 - s) * v) by A1, RLVECT_1: 6;

      then

       A2: (( - s) * w) = ((1 - s) * v) by RLVECT_1: 79;

      per cases ;

        suppose

         A3: ( - s) <> 0 ;

        take r = ((( - s) " ) * (1 - s));

        w = (1 * w) by RLVECT_1:def 8

        .= (((( - s) " ) * ( - s)) * w) by A3, XCMPLX_0:def 7

        .= ((( - s) " ) * (( - s) * w)) by RLVECT_1:def 7

        .= (r * v) by A2, RLVECT_1:def 7;

        hence thesis;

      end;

        suppose

         A4: ( - s) = 0 ;

        take ( - s);

        thus thesis by A2, A4, RLVECT_1:def 8;

      end;

    end;

    definition

      let V, v, w;

      :: RLTOPSP1:def14

      func Line (v,w) -> Subset of V equals the set of all (((1 - r) * v) + (r * w));

      coherence

      proof

        set A = the set of all (((1 - r) * v) + (r * w));

        A c= the carrier of V

        proof

          let x be object;

          assume x in A;

          then ex r st x = (((1 - r) * v) + (r * w));

          hence x in the carrier of V;

        end;

        hence thesis;

      end;

      commutativity

      proof

        let S be Subset of V;

        let v, w;

        set A = the set of all (((1 - r) * w) + (r * v));

        assume

         A1: S = the set of all (((1 - r) * v) + (r * w));

        thus S c= A

        proof

          let e be object;

          assume e in S;

          then

          consider r such that

           A2: e = (((1 - r) * v) + (r * w)) by A1;

          e = (((1 - (1 - r)) * w) + ((1 - r) * v)) by A2;

          hence e in A;

        end;

        let e be object;

        assume e in A;

        then

        consider r such that

         A3: e = (((1 - r) * w) + (r * v));

        e = (((1 - (1 - r)) * v) + ((1 - r) * w)) by A3;

        hence e in S by A1;

      end;

    end

    theorem :: RLTOPSP1:72

    

     Th72: v in ( Line (v,w))

    proof

      v = (((1 - 0 ) * v) + ( 0. V)) by RLVECT_1:def 8

      .= (((1 - 0 ) * v) + ( 0 * w)) by RLVECT_1: 10;

      hence thesis;

    end;

    registration

      let V, v, w;

      cluster ( Line (v,w)) -> non empty;

      coherence by Th72;

    end

    theorem :: RLTOPSP1:73

    ( LSeg (v,w)) c= ( Line (v,w))

    proof

      let e be object;

      assume e in ( LSeg (v,w));

      then ex r st e = (((1 - r) * v) + (r * w)) & 0 <= r & r <= 1;

      hence e in ( Line (v,w));

    end;

    reserve x1,x2,x3,x4,y1,y2 for Element of V;

    theorem :: RLTOPSP1:74

    

     Th74: y1 in ( Line (x1,x2)) & y2 in ( Line (x1,x2)) implies ( Line (y1,y2)) c= ( Line (x1,x2))

    proof

      assume y1 in ( Line (x1,x2));

      then

      consider t such that

       A1: y1 = (((1 - t) * x1) + (t * x2));

      assume y2 in ( Line (x1,x2));

      then

      consider s such that

       A2: y2 = (((1 - s) * x1) + (s * x2));

      let z be object;

      assume z in ( Line (y1,y2));

      then

      consider u such that

       A3: z = (((1 - u) * y1) + (u * y2));

      z = ((((1 - u) * ((1 - t) * x1)) + ((1 - u) * (t * x2))) + (u * (((1 - s) * x1) + (s * x2)))) by A1, A2, A3, RLVECT_1:def 5

      .= ((((1 - u) * ((1 - t) * x1)) + ((1 - u) * (t * x2))) + ((u * ((1 - s) * x1)) + (u * (s * x2)))) by RLVECT_1:def 5

      .= (((((1 - u) * (1 - t)) * x1) + ((1 - u) * (t * x2))) + ((u * ((1 - s) * x1)) + (u * (s * x2)))) by RLVECT_1:def 7

      .= (((((1 - u) * (1 - t)) * x1) + (((1 - u) * t) * x2)) + ((u * ((1 - s) * x1)) + (u * (s * x2)))) by RLVECT_1:def 7

      .= (((((1 - u) * (1 - t)) * x1) + (((1 - u) * t) * x2)) + (((u * (1 - s)) * x1) + (u * (s * x2)))) by RLVECT_1:def 7

      .= (((((1 - u) * (1 - t)) * x1) + (((1 - u) * t) * x2)) + (((u * (1 - s)) * x1) + ((u * s) * x2))) by RLVECT_1:def 7

      .= ((((1 - u) * (1 - t)) * x1) + ((((1 - u) * t) * x2) + (((u * (1 - s)) * x1) + ((u * s) * x2)))) by RLVECT_1:def 3

      .= ((((1 - u) * (1 - t)) * x1) + (((u * (1 - s)) * x1) + ((((1 - u) * t) * x2) + ((u * s) * x2)))) by RLVECT_1:def 3

      .= (((((1 - u) * (1 - t)) * x1) + ((u * (1 - s)) * x1)) + ((((1 - u) * t) * x2) + ((u * s) * x2))) by RLVECT_1:def 3

      .= (((((1 - u) * (1 - t)) + (u * (1 - s))) * x1) + ((((1 - u) * t) * x2) + ((u * s) * x2))) by RLVECT_1:def 6

      .= (((1 - (((1 * t) - (u * t)) + (u * s))) * x1) + ((((1 * t) - (u * t)) + (u * s)) * x2)) by RLVECT_1:def 6;

      hence z in ( Line (x1,x2));

    end;

    theorem :: RLTOPSP1:75

    

     Th75: y1 in ( Line (x1,x2)) & y2 in ( Line (x1,x2)) & y1 <> y2 implies ( Line (y1,y2)) = ( Line (x1,x2))

    proof

      assume

       A1: y1 in ( Line (x1,x2));

      then

      consider t such that

       A2: y1 = (((1 - t) * x1) + (t * x2));

      assume

       A3: y2 in ( Line (x1,x2));

      then

      consider s such that

       A4: y2 = (((1 - s) * x1) + (s * x2));

      assume y1 <> y2;

      then

       A5: (t - s) <> 0 by A2, A4;

      thus ( Line (y1,y2)) c= ( Line (x1,x2)) by A1, A3, Th74;

      (((1 - ((t - 1) / (t - s))) * y1) + (((t - 1) / (t - s)) * y2)) = (((((1 * (t - s)) - (t - 1)) / (t - s)) * y1) + (((t - 1) / (t - s)) * y2)) by A5, XCMPLX_1: 127

      .= (((((( - s) + 1) / (t - s)) * ((1 - t) * x1)) + (((( - s) + 1) / (t - s)) * (t * x2))) + (((t - 1) / (t - s)) * (((1 - s) * x1) + (s * x2)))) by A2, A4, RLVECT_1:def 5

      .= (((((( - s) + 1) / (t - s)) * ((1 - t) * x1)) + (((( - s) + 1) / (t - s)) * (t * x2))) + ((((t - 1) / (t - s)) * ((1 - s) * x1)) + (((t - 1) / (t - s)) * (s * x2)))) by RLVECT_1:def 5

      .= ((((((( - s) + 1) / (t - s)) * (1 - t)) * x1) + (((( - s) + 1) / (t - s)) * (t * x2))) + ((((t - 1) / (t - s)) * ((1 - s) * x1)) + (((t - 1) / (t - s)) * (s * x2)))) by RLVECT_1:def 7

      .= ((((((( - s) + 1) / (t - s)) * (1 - t)) * x1) + ((((( - s) + 1) / (t - s)) * t) * x2)) + ((((t - 1) / (t - s)) * ((1 - s) * x1)) + (((t - 1) / (t - s)) * (s * x2)))) by RLVECT_1:def 7

      .= ((((((( - s) + 1) / (t - s)) * (1 - t)) * x1) + ((((( - s) + 1) / (t - s)) * t) * x2)) + (((((t - 1) / (t - s)) * (1 - s)) * x1) + (((t - 1) / (t - s)) * (s * x2)))) by RLVECT_1:def 7

      .= ((((((( - s) + 1) / (t - s)) * (1 - t)) * x1) + ((((( - s) + 1) / (t - s)) * t) * x2)) + (((((t - 1) / (t - s)) * (1 - s)) * x1) + ((((t - 1) / (t - s)) * s) * x2))) by RLVECT_1:def 7

      .= (((((( - s) + 1) * (1 - t)) / (t - s)) * x1) + (((((( - s) + 1) * t) / (t - s)) * x2) + (((((t - 1) * (1 - s)) / (t - s)) * x1) + ((((t - 1) * s) / (t - s)) * x2)))) by RLVECT_1:def 3

      .= (((((( - s) + 1) * (1 - t)) / (t - s)) * x1) + (((((t - 1) * (1 - s)) / (t - s)) * x1) + (((((( - s) + 1) * t) / (t - s)) * x2) + ((((t - 1) * s) / (t - s)) * x2)))) by RLVECT_1:def 3

      .= ((((((( - s) + 1) * (1 - t)) / (t - s)) * x1) + ((((t - 1) * (1 - s)) / (t - s)) * x1)) + (((((( - s) + 1) * t) / (t - s)) * x2) + ((((t - 1) * s) / (t - s)) * x2))) by RLVECT_1:def 3

      .= ((((((( - s) + 1) * (1 - t)) / (t - s)) + (((t - 1) * (1 - s)) / (t - s))) * x1) + (((((( - s) + 1) * t) / (t - s)) * x2) + ((((t - 1) * s) / (t - s)) * x2))) by RLVECT_1:def 6

      .= ((((((( - s) + 1) * (1 - t)) / (t - s)) + (((t - 1) * (1 - s)) / (t - s))) * x1) + (((((( - s) + 1) * t) / (t - s)) + (((t - 1) * s) / (t - s))) * x2)) by RLVECT_1:def 6

      .= (( 0. V) + (((((( - s) + 1) * t) + ((t - 1) * s)) / (t - s)) * x2)) by RLVECT_1: 10

      .= (((1 * (t - s)) / (t - s)) * x2)

      .= (1 * x2) by A5, XCMPLX_1: 89

      .= x2 by RLVECT_1:def 8;

      then

       A6: x2 in ( Line (y1,y2));

      (((1 - (t / (t - s))) * y1) + ((t / (t - s)) * y2)) = (((((1 * (t - s)) - t) / (t - s)) * y1) + ((t / (t - s)) * y2)) by A5, XCMPLX_1: 127

      .= ((((( - s) / (t - s)) * ((1 - t) * x1)) + ((( - s) / (t - s)) * (t * x2))) + ((t / (t - s)) * (((1 - s) * x1) + (s * x2)))) by A2, A4, RLVECT_1:def 5

      .= ((((( - s) / (t - s)) * ((1 - t) * x1)) + ((( - s) / (t - s)) * (t * x2))) + (((t / (t - s)) * ((1 - s) * x1)) + ((t / (t - s)) * (s * x2)))) by RLVECT_1:def 5

      .= (((((( - s) / (t - s)) * (1 - t)) * x1) + ((( - s) / (t - s)) * (t * x2))) + (((t / (t - s)) * ((1 - s) * x1)) + ((t / (t - s)) * (s * x2)))) by RLVECT_1:def 7

      .= (((((( - s) / (t - s)) * (1 - t)) * x1) + (((( - s) / (t - s)) * t) * x2)) + (((t / (t - s)) * ((1 - s) * x1)) + ((t / (t - s)) * (s * x2)))) by RLVECT_1:def 7

      .= (((((( - s) / (t - s)) * (1 - t)) * x1) + (((( - s) / (t - s)) * t) * x2)) + ((((t / (t - s)) * (1 - s)) * x1) + ((t / (t - s)) * (s * x2)))) by RLVECT_1:def 7

      .= (((((( - s) / (t - s)) * (1 - t)) * x1) + (((( - s) / (t - s)) * t) * x2)) + ((((t / (t - s)) * (1 - s)) * x1) + (((t / (t - s)) * s) * x2))) by RLVECT_1:def 7

      .= ((((( - s) * (1 - t)) / (t - s)) * x1) + ((((( - s) * t) / (t - s)) * x2) + ((((t * (1 - s)) / (t - s)) * x1) + (((t * s) / (t - s)) * x2)))) by RLVECT_1:def 3

      .= ((((( - s) * (1 - t)) / (t - s)) * x1) + ((((t * (1 - s)) / (t - s)) * x1) + ((((( - s) * t) / (t - s)) * x2) + (((t * s) / (t - s)) * x2)))) by RLVECT_1:def 3

      .= (((((( - s) * (1 - t)) / (t - s)) * x1) + (((t * (1 - s)) / (t - s)) * x1)) + ((((( - s) * t) / (t - s)) * x2) + (((t * s) / (t - s)) * x2))) by RLVECT_1:def 3

      .= (((((( - s) * (1 - t)) / (t - s)) + ((t * (1 - s)) / (t - s))) * x1) + ((((( - s) * t) / (t - s)) * x2) + (((t * s) / (t - s)) * x2))) by RLVECT_1:def 6

      .= (((((( - s) * (1 - t)) + (t * (1 - s))) / (t - s)) * x1) + ((((( - s) * t) / (t - s)) + ((t * s) / (t - s))) * x2)) by RLVECT_1:def 6

      .= (((((( - s) * (1 - t)) + (t * (1 - s))) / (t - s)) * x1) + ( 0. V)) by RLVECT_1: 10

      .= (((1 * (t - s)) / (t - s)) * x1)

      .= (1 * x1) by A5, XCMPLX_1: 89

      .= x1 by RLVECT_1:def 8;

      then x1 in ( Line (y1,y2));

      hence thesis by A6, Th74;

    end;

    definition

      let V;

      let A be Subset of V;

      :: RLTOPSP1:def15

      attr A is being_line means

      : Def15: ex x1, x2 st A = ( Line (x1,x2));

    end

    registration

      let V;

      cluster being_line for Subset of V;

      existence

      proof

        set v = the Point of V;

        take ( Line (v,v)), v, v;

        thus thesis;

      end;

    end

    registration

      let V be non trivial RealLinearSpace;

      cluster non trivial being_line for Subset of V;

      existence

      proof

        consider v,w be Point of V such that

         A1: v <> w by STRUCT_0:def 10;

        take L = ( Line (v,w));

        thus L is non trivial

        proof

          take v, w;

          thus v in L & w in L by Th72;

          thus v <> w by A1;

        end;

        take v, w;

        thus thesis;

      end;

    end

    definition

      let V;

      mode line of V is being_line Subset of V;

    end

    definition

      let V;

      let x1,x2,x3 be Point of V;

      :: RLTOPSP1:def16

      pred x1,x2,x3 are_collinear means ex L be line of V st x1 in L & x2 in L & x3 in L;

    end

    definition

      let V;

      let x1,x2,x3,x4 be Point of V;

      :: RLTOPSP1:def17

      pred x1,x2,x3,x4 are_collinear means ex L be line of V st x1 in L & x2 in L & x3 in L & x4 in L;

    end

    theorem :: RLTOPSP1:76

    for x be object st x in ( LSeg (v,w)) holds ex r st 0 <= r & r <= 1 & x = (((1 - r) * v) + (r * w))

    proof

      let x be object;

      assume x in ( LSeg (v,w));

      then ex r st x = (((1 - r) * v) + (r * w)) & 0 <= r & r <= 1;

      hence ex r st 0 <= r & r <= 1 & x = (((1 - r) * v) + (r * w));

    end;

    theorem :: RLTOPSP1:77

    

     Th77: ( Line (v,v)) = {v}

    proof

      for x be object holds x in ( Line (v,v)) iff x = v

      proof

        let x be object;

        thus x in ( Line (v,v)) implies x = v

        proof

          assume

           A1: x in ( Line (v,v));

          then

          reconsider w = x as Point of V;

          consider r such that

           A2: w = (((1 - r) * v) + (r * v)) by A1;

          w = (((1 - r) + r) * v) by A2, RLVECT_1:def 6;

          hence x = v by RLVECT_1:def 8;

        end;

        assume x = v;

        hence thesis by Th72;

      end;

      hence thesis by TARSKI:def 1;

    end;

    registration

      let V, v;

      cluster {v} -> being_line;

      coherence

      proof

        let A be Subset of V such that

         A1: A = {v};

        take v, v;

        thus thesis by A1, Th77;

      end;

      let w;

      cluster ( Line (v,w)) -> being_line;

      coherence ;

    end

    theorem :: RLTOPSP1:78

    for V be non trivial RealLinearSpace, L be non trivial line of V holds ex p,q be Point of V st p <> q & L = ( Line (p,q))

    proof

      let V be non trivial RealLinearSpace, L be non trivial line of V;

      consider p,q be object such that

       A1: p in L & q in L and

       A2: p <> q by ZFMISC_1:def 10;

      reconsider p, q as Point of V by A1;

      take p, q;

      thus p <> q by A2;

      ex x1,x2 be Element of V st L = ( Line (x1,x2)) by Def15;

      hence L = ( Line (p,q)) by A2, Th75, A1;

    end;

    theorem :: RLTOPSP1:79

    for x1,x2,x3,x4 be Point of V st (x1,x2,x3,x4) are_collinear holds (x1,x2,x3) are_collinear & (x1,x2,x4) are_collinear ;

    theorem :: RLTOPSP1:80

    

     Th80: for L be line of V, x1, x2 st x1 <> x2 & x1 in L & x2 in L holds L = ( Line (x1,x2))

    proof

      let L be line of V;

      ex x3, x4 st L = ( Line (x3,x4)) by Def15;

      hence thesis by Th75;

    end;

    theorem :: RLTOPSP1:81

    for x1,x2,x3,x4 be Point of V st x1 <> x2 & (x1,x2,x3) are_collinear & (x1,x2,x4) are_collinear holds (x1,x2,x3,x4) are_collinear

    proof

      let x1,x2,x3,x4 be Point of V such that

       A1: x1 <> x2;

      given L1 be line of V such that

       A2: x1 in L1 & x2 in L1 & x3 in L1;

      given L2 be line of V such that

       A3: x1 in L2 & x2 in L2 & x4 in L2;

      L1 = ( Line (x1,x2)) & L2 = ( Line (x1,x2)) by A1, A2, A3, Th80;

      hence ex L be line of V st x1 in L & x2 in L & x3 in L & x4 in L by A2, A3;

    end;