:: RLTOPSP1 semantic presentation

begin


theorem :: RLTOPSP1:1
for X being non empty RLSStruct
for M being Subset of X
for x being Point of X
for r being Real st x in M holds
r * x in r * M ;

registration
cluster non zero ext-real complex real for Element of REAL ;
existence
 not for b1 being Real holds b1 is zero
proof
take  1 ; ::_thesis: not 1 is zero
thus  not 1 is zero ; ::_thesis: verum
end;
end;

theorem Th2: :: RLTOPSP1:2
for T being non empty TopSpace
for X being non empty Subset of T
for FX being Subset-Family of T st FX is Cover of X holds
for x being Point of T st x in X holds
ex W being Subset of T st
( x in W & W in FX )
proof
let T be non empty TopSpace; ::_thesis: for X being non empty Subset of T
for FX being Subset-Family of T st FX is Cover of X holds
for x being Point of T st x in X holds
ex W being Subset of T st
( x in W & W in FX )
let X be non empty Subset of T; ::_thesis: for FX being Subset-Family of T st FX is Cover of X holds
for x being Point of T st x in X holds
ex W being Subset of T st
( x in W & W in FX )
let FX be Subset-Family of T; ::_thesis: ( FX is Cover of X implies for x being Point of T st x in X holds
ex W being Subset of T st
( x in W & W in FX ) )
assume  FX is Cover of X ; ::_thesis: for x being Point of T st x in X holds
ex W being Subset of T st
( x in W & W in FX )
then A1: X c= union FX by SETFAM_1:def_11;
let x be Point of T; ::_thesis: ( x in X implies ex W being Subset of T st
( x in W & W in FX ) )
assume  x in X ; ::_thesis: ex W being Subset of T st
( x in W & W in FX )
then consider W being set  such that
A2: x in W and
A3: W in FX by A1, TARSKI:def_4;
reconsider W = W as Subset of T by A3;
take  W ; ::_thesis: ( x in W & W in FX )
thus  ( x in W & W in FX ) by A2, A3; ::_thesis: verum
end;

theorem Th3: :: RLTOPSP1:3
for X being non empty addLoopStr
for M, N being Subset of X
for x, y being Point of X st x in M & y in N holds
x + y in M + N
proof
let X be non empty addLoopStr ; ::_thesis: for M, N being Subset of X
for x, y being Point of X st x in M & y in N holds
x + y in M + N
let M, N be Subset of X; ::_thesis: for x, y being Point of X st x in M & y in N holds
x + y in M + N
let x, y be Point of X; ::_thesis: ( x in M & y in N implies x + y in M + N )
 M + N =  {  (u + v) where u, v is Point of X : ( u in M & v in N )  }  by RUSUB_4:def_9;
hence  ( x in M & y in N implies x + y in M + N ) ; ::_thesis: verum
end;

Lm1:  for X being non empty addLoopStr
for M being Subset of X
for x, y being Point of X st y in M holds
x + y in x + M
proof
let X be non empty addLoopStr ; ::_thesis: for M being Subset of X
for x, y being Point of X st y in M holds
x + y in x + M
let M be Subset of X; ::_thesis: for x, y being Point of X st y in M holds
x + y in x + M
let x, y be Point of X; ::_thesis: ( y in M implies x + y in x + M )
 x + M =  {  (x + u) where u is Point of X : u in M  }  by RUSUB_4:def_8;
hence  ( y in M implies x + y in x + M ) ; ::_thesis: verum
end;

Lm2:  for X being non empty addLoopStr
for M, N being Subset of X holds  {  (x + N) where x is Point of X : x in M  }  is Subset-Family of X
proof
let X be non empty addLoopStr ; ::_thesis: for M, N being Subset of X holds  {  (x + N) where x is Point of X : x in M  }  is Subset-Family of X
let M, N be Subset of X; ::_thesis:  {  (x + N) where x is Point of X : x in M  }  is Subset-Family of X
set F =  {  (u + N) where u is Point of X : u in M  }  ;
  {  (u + N) where u is Point of X : u in M  }  c= bool the carrier of X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (u + N) where u is Point of X : u in M  }  or x in bool the carrier of X )
assume  x in  {  (u + N) where u is Point of X : u in M  }  ; ::_thesis: x in bool the carrier of X
then  ex u being Point of X st
( x = u + N & u in M ) ;
hence  x in bool the carrier of X ; ::_thesis: verum
end;
hence   {  (x + N) where x is Point of X : x in M  }  is Subset-Family of X ; ::_thesis: verum
end;

theorem Th4: :: RLTOPSP1:4
for X being non empty addLoopStr
for M, N being Subset of X
for F being Subset-Family of X st F =  {  (x + N) where x is Point of X : x in M  }  holds
M + N = union F
proof
let X be non empty addLoopStr ; ::_thesis: for M, N being Subset of X
for F being Subset-Family of X st F =  {  (x + N) where x is Point of X : x in M  }  holds
M + N = union F
let M, N be Subset of X; ::_thesis: for F being Subset-Family of X st F =  {  (x + N) where x is Point of X : x in M  }  holds
M + N = union F
let F be Subset-Family of X; ::_thesis: ( F =  {  (x + N) where x is Point of X : x in M  }  implies M + N = union F )
assume A1: F =  {  (x + N) where x is Point of X : x in M  }  ; ::_thesis: M + N = union F
thus  M + N c= union F :: according to XBOOLE_0:def_10 ::_thesis: union F c= M + N
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in M + N or x in union F )
assume  x in M + N ; ::_thesis: x in union F
then  x in  {  (u + v) where u, v is Point of X : ( u in M & v in N )  }  by RUSUB_4:def_9;
then consider u, v being 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 is 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  x in union F by A5, TARSKI:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union F or x in M + N )
assume  x in union F ; ::_thesis: x in M + N
then consider Y being set  such that
A6: x in Y and
A7: Y in F by TARSKI:def_4;
consider u being Point of X such that
A8: Y = u + N and
A9: u in M by A1, A7;
 u + N =  {  (u + v) where v is Point of X : v in N  }  by RUSUB_4:def_8;
then  ex v being Point of X st
( x = u + v & v in N ) by A6, A8;
then  x in  {  (u9 + v9) where u9, v9 is Point of X : ( u9 in M & v9 in N )  }  by A9;
hence  x in M + N by RUSUB_4:def_9; ::_thesis: verum
end;

theorem Th5: :: RLTOPSP1:5
for X being non empty right_complementable add-associative right_zeroed addLoopStr
for M being Subset of X holds (0. X) + M = M
proof
let X be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for M being Subset of X holds (0. X) + M = M
let M be Subset of X; ::_thesis: (0. X) + M = M
A1: (0. X) + M =  {  ((0. X) + u) where u is Point of X : u in M  }  by RUSUB_4:def_8;
thus  (0. X) + M c= M :: according to XBOOLE_0:def_10 ::_thesis: M c= (0. X) + M
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (0. X) + M or x in M )
assume  x in (0. X) + M ; ::_thesis: x in M
then  ex u being Point of X st
( x = (0. X) + u & u in M ) by A1;
hence  x in M by RLVECT_1:4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in M or x in (0. X) + M )
assume A2: x in M ; ::_thesis: x in (0. X) + M
then reconsider x = x as Point of X ;
 (0. X) + x = x by RLVECT_1:4;
hence  x in (0. X) + M by A1, A2; ::_thesis: verum
end;

theorem Th6: :: RLTOPSP1:6
for X being non empty add-associative addLoopStr
for x, y being Point of X
for M being Subset of X holds (x + y) + M = x + (y + M)
proof
let X be non empty add-associative addLoopStr ; ::_thesis: for x, y being Point of X
for M being Subset of X holds (x + y) + M = x + (y + M)
let x, y be Point of X; ::_thesis: for M being Subset of X holds (x + y) + M = x + (y + M)
let M be Subset of X; ::_thesis: (x + y) + M = x + (y + M)
A1: x + (y + M) =  {  (x + u) where u is Point of X : u in y + M  }  by RUSUB_4:def_8;
A2: y + M =  {  (y + u) where u is Point of X : u in M  }  by RUSUB_4:def_8;
A3: (x + y) + M =  {  ((x + y) + u) where u is Point of X : u in M  }  by RUSUB_4:def_8;
thus  (x + y) + M c= x + (y + M) :: according to XBOOLE_0:def_10 ::_thesis: x + (y + M) c= (x + y) + M
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in (x + y) + M or z in x + (y + M) )
assume  z in (x + y) + M ; ::_thesis: z in x + (y + M)
then consider u being 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  z in x + (y + M) by A1; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in x + (y + M) or z in (x + y) + M )
assume  z in x + (y + M) ; ::_thesis: z in (x + y) + M
then consider u being Point of X such that
A5: x + u = z and
A6: u in y + M by A1;
consider v being 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  z in (x + y) + M by A3, A8; ::_thesis: verum
end;

theorem Th7: :: RLTOPSP1:7
for X being non empty add-associative addLoopStr
for x being Point of X
for M, N being Subset of X holds (x + M) + N = x + (M + N)
proof
let X be non empty add-associative addLoopStr ; ::_thesis: for x being Point of X
for M, N being Subset of X holds (x + M) + N = x + (M + N)
let x be Point of X; ::_thesis: for M, N being Subset of X holds (x + M) + N = x + (M + N)
let M, N be Subset of X; ::_thesis: (x + M) + N = x + (M + N)
A1: x + (M + N) =  {  (x + u) where u is Point of X : u in M + N  }  by RUSUB_4:def_8;
A2: x + M =  {  (x + u) where u is Point of X : u in M  }  by RUSUB_4:def_8;
A3: M + N =  {  (u + v) where u, v is Point of X : ( u in M & v in N )  }  by RUSUB_4:def_9;
A4: (x + M) + N =  {  (u + v) where u, v is Point of X : ( u in x + M & v in N )  }  by RUSUB_4:def_9;
thus  (x + M) + N c= x + (M + N) :: according to XBOOLE_0:def_10 ::_thesis: x + (M + N) c= (x + M) + N
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in (x + M) + N or z in x + (M + N) )
assume  z in (x + M) + N ; ::_thesis: z in x + (M + N)
then consider u, v being Point of X such that
A5: u + v = z and
A6: u in x + M and
A7: v in N by A4;
consider u9 being 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  z in x + (M + N) by A1; ::_thesis: verum
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in x + (M + N) or z in (x + M) + N )
assume  z in x + (M + N) ; ::_thesis: z in (x + M) + N
then consider u being Point of X such that
A9: x + u = z and
A10: u in M + N by A1;
consider w, v being 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  z in (x + M) + N by A4, A13, A14; ::_thesis: verum
end;

theorem Th8: :: RLTOPSP1:8
for X being non empty addLoopStr
for M, N being Subset of X
for x being Point of X st M c= N holds
x + M c= x + N
proof
let X be non empty addLoopStr ; ::_thesis: for M, N being Subset of X
for x being Point of X st M c= N holds
x + M c= x + N
let M, N be Subset of X; ::_thesis: for x being Point of X st M c= N holds
x + M c= x + N
let x be Point of X; ::_thesis: ( M c= N implies x + M c= x + N )
assume A1: M c= N ; ::_thesis: x + M c= x + N
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in x + M or z in x + N )
assume A2: z in x + M ; ::_thesis: z in x + N
then reconsider z = z as Point of X ;
 x + M =  {  (x + u) where u is Element of X : u in M  }  by RUSUB_4:def_8;
then  ex u being Point of X st
( x + u = z & u in M ) by A2;
hence  z in x + N by A1, Lm1; ::_thesis: verum
end;

theorem Th9: :: RLTOPSP1:9
for X being non empty right_complementable add-associative right_zeroed addLoopStr
for M being Subset of X
for x being Point of X st x in M holds
0. X in (- x) + M
proof
let X be non empty right_complementable add-associative right_zeroed addLoopStr ; ::_thesis: for M being Subset of X
for x being Point of X st x in M holds
0. X in (- x) + M
let M be Subset of X; ::_thesis: for x being Point of X st x in M holds
0. X in (- x) + M
let x be Point of X; ::_thesis: ( x in M implies 0. X in (- x) + M )
assume  x in M ; ::_thesis: 0. X in (- x) + M
then  (- x) + x in (- x) + M by Lm1;
hence  0. X in (- x) + M by RLVECT_1:5; ::_thesis: verum
end;

theorem Th10: :: RLTOPSP1:10
for X being non empty addLoopStr
for M, N, V being Subset of X st M c= N holds
M + V c= N + V
proof
let X be non empty addLoopStr ; ::_thesis: for M, N, V being Subset of X st M c= N holds
M + V c= N + V
let M, N, V be Subset of X; ::_thesis: ( M c= N implies M + V c= N + V )
assume A1: M c= N ; ::_thesis: M + V c= N + V
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in M + V or x in N + V )
assume  x in M + V ; ::_thesis: x in N + V
then  x in  {  (u + v) where u, v is Point of X : ( u in M & v in V )  }  by RUSUB_4:def_9;
then  ex u, v being Point of X st
( u + v = x & u in M & v in V ) ;
then  x in  {  (u9 + v9) where u9, v9 is Point of X : ( u9 in N & v9 in V )  }  by A1;
hence  x in N + V by RUSUB_4:def_9; ::_thesis: verum
end;

Lm3:  for X being non empty addLoopStr
for M, N, V being Subset of X st M c= N holds
V + M c= V + N
proof
let X be non empty addLoopStr ; ::_thesis: for M, N, V being Subset of X st M c= N holds
V + M c= V + N
let M, N, V be Subset of X; ::_thesis: ( M c= N implies V + M c= V + N )
assume A1: M c= N ; ::_thesis: V + M c= V + N
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in V + M or x in V + N )
assume  x in V + M ; ::_thesis: x in V + N
then  x in  {  (u + v) where u, v is Point of X : ( u in V & v in M )  }  by RUSUB_4:def_9;
then  ex u, v being Point of X st
( u + v = x & u in V & v in M ) ;
then  x in  {  (u9 + v9) where u9, v9 is Point of X : ( u9 in V & v9 in N )  }  by A1;
hence  x in V + N by RUSUB_4:def_9; ::_thesis: verum
end;

theorem Th11: :: RLTOPSP1:11
for X being non empty addLoopStr
for V1, V2, W1, W2 being Subset of X st V1 c= W1 & V2 c= W2 holds
V1 + V2 c= W1 + W2
proof
let X be non empty addLoopStr ; ::_thesis: for V1, V2, W1, W2 being Subset of X st V1 c= W1 & V2 c= W2 holds
V1 + V2 c= W1 + W2
let V1, V2, W1, W2 be Subset of X; ::_thesis: ( V1 c= W1 & V2 c= W2 implies V1 + V2 c= W1 + W2 )
assume A1: ( V1 c= W1 & V2 c= W2 ) ; ::_thesis: V1 + V2 c= W1 + W2
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in V1 + V2 or x in W1 + W2 )
assume  x in V1 + V2 ; ::_thesis: x in W1 + W2
then  x in  {  (u + v) where u, v is Point of X : ( u in V1 & v in V2 )  }  by RUSUB_4:def_9;
then  ex u, v being Point of X st
( u + v = x & u in V1 & v in V2 ) ;
then  x in  {  (u9 + v9) where u9, v9 is Point of X : ( u9 in W1 & v9 in W2 )  }  by A1;
hence  x in W1 + W2 by RUSUB_4:def_9; ::_thesis: verum
end;

theorem Th12: :: RLTOPSP1:12
for X being non empty right_zeroed addLoopStr
for V1, V2 being Subset of X st 0. X in V2 holds
V1 c= V1 + V2
proof
let X be non empty right_zeroed addLoopStr ; ::_thesis: for V1, V2 being Subset of X st 0. X in V2 holds
V1 c= V1 + V2
let V1, V2 be Subset of X; ::_thesis: ( 0. X in V2 implies V1 c= V1 + V2 )
assume A1: 0. X in V2 ; ::_thesis: V1 c= V1 + V2
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in V1 or x in V1 + V2 )
assume A2: x in V1 ; ::_thesis: x in V1 + V2
then reconsider x = x as Point of X ;
 x + (0. X) = x by RLVECT_1:def_4;
then  x in  {  (u + v) where u, v is Point of X : ( u in V1 & v in V2 )  }  by A1, A2;
hence  x in V1 + V2 by RUSUB_4:def_9; ::_thesis: verum
end;

theorem Th13: :: RLTOPSP1:13
for X being RealLinearSpace
for r being Real holds r * {(0. X)} = {(0. X)}
proof
let X be RealLinearSpace; ::_thesis: for r being Real holds r * {(0. X)} = {(0. X)}
let r be Real; ::_thesis: r * {(0. X)} = {(0. X)}
thus  r * {(0. X)} c= {(0. X)} :: according to XBOOLE_0:def_10 ::_thesis: {(0. X)} c= r * {(0. X)}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in r * {(0. X)} or x in {(0. X)} )
assume A1: x in r * {(0. X)} ; ::_thesis: x in {(0. X)}
then reconsider x = x as Point of X ;
consider v being 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 by RLVECT_1:10;
hence  x in {(0. X)} by A2, TARSKI:def_1; ::_thesis: verum
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)} by RLVECT_1:10;
hence  {(0. X)} c= r * {(0. X)} by ZFMISC_1:31; ::_thesis: verum
end;

theorem :: RLTOPSP1:14
for X being RealLinearSpace
for M being Subset of X
for r being non zero Real st 0. X in r * M holds
0. X in M
proof
let X be RealLinearSpace; ::_thesis: for M being Subset of X
for r being non zero Real st 0. X in r * M holds
0. X in M
let M be Subset of X; ::_thesis: for r being non zero Real st 0. X in r * M holds
0. X in M
let r be non zero Real; ::_thesis: ( 0. X in r * M implies 0. X in M )
assume  0. X in r * M ; ::_thesis: 0. X in M
then A1: ex v being Point of X st
( r * v = 0. X & v in M ) ;
 r * (0. X) = 0. X by RLVECT_1:10;
hence  0. X in M by A1, RLVECT_1:36; ::_thesis: verum
end;

theorem Th15: :: RLTOPSP1:15
for X being RealLinearSpace
for M, N being Subset of X
for r being non zero Real holds (r * M) /\ (r * N) = r * (M /\ N)
proof
let X be RealLinearSpace; ::_thesis: for M, N being Subset of X
for r being non zero Real holds (r * M) /\ (r * N) = r * (M /\ N)
let M, N be Subset of X; ::_thesis: for r being non zero Real holds (r * M) /\ (r * N) = r * (M /\ N)
let r be non zero Real; ::_thesis: (r * M) /\ (r * N) = r * (M /\ N)
thus  for x being set st x in (r * M) /\ (r * N) holds
x in r * (M /\ N) :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: r * (M /\ N) c= (r * M) /\ (r * N)
proof
let x be set ; ::_thesis: ( x in (r * M) /\ (r * N) implies x in r * (M /\ N) )
assume A1: x in (r * M) /\ (r * N) ; ::_thesis: x in r * (M /\ N)
then  x in r * M by XBOOLE_0:def_4;
then consider v1 being 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 being 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  x in r * (M /\ N) by A2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in r * (M /\ N) or x in (r * M) /\ (r * N) )
assume  x in r * (M /\ N) ; ::_thesis: x in (r * M) /\ (r * N)
then consider v being 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  x in (r * M) /\ (r * N) by A8, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem :: RLTOPSP1:16
for X being non empty TopSpace
for x being Point of X
for A being a_neighborhood of x
for B being Subset of X st A c= B holds
B is a_neighborhood of x
proof
let X be non empty TopSpace; ::_thesis: for x being Point of X
for A being a_neighborhood of x
for B being Subset of X st A c= B holds
B is a_neighborhood of x
let x be Point of X; ::_thesis: for A being a_neighborhood of x
for B being Subset of X st A c= B holds
B is a_neighborhood of x
let A be a_neighborhood of x; ::_thesis: for B being Subset of X st A c= B holds
B is a_neighborhood of x
let B be Subset of X; ::_thesis: ( A c= B implies B is a_neighborhood of x )
assume  A c= B ; ::_thesis: B is a_neighborhood of x
then  ( x in Int A & Int A c= Int B ) by CONNSP_2:def_1, TOPS_1:19;
hence  B is a_neighborhood of x by CONNSP_2:def_1; ::_thesis: verum
end;

definition
let V be RealLinearSpace;
let M be Subset of V;
redefine attr M is convex  means :Def1: :: RLTOPSP1:def 1
 for u, v being Point of V
for r being Real st 0 <= r & r <= 1 & u in M & v in M holds
(r * u) + ((1 - r) * v) in M;
compatibility
 ( M is convex iff for u, v being Point of V
for r being Real st 0 <= r & r <= 1 & u in M & v in M holds
(r * u) + ((1 - r) * v) in M )
proof
hereby  ::_thesis: ( ( for u, v being Point of V
for r being Real st 0 <= r & r <= 1 & u in M & v in M holds
(r * u) + ((1 - r) * v) in M ) implies M is convex )
assume A1: M is convex ; ::_thesis: for u, v being Point of V
for r being Real st 0 <= r & r <= 1 & u in M & v in M holds
(b6 * b4) + ((1 - b6) * b5) in M
let u, v be Point of V; ::_thesis: for r being Real st 0 <= r & r <= 1 & u in M & v in M holds
(b4 * b2) + ((1 - b4) * b3) in M
let r be Real; ::_thesis: ( 0 <= r & r <= 1 & u in M & v in M implies (b3 * b1) + ((1 - b3) * b2) in M )
assume that
A2: ( 0 <= r & r <= 1 ) and
A3: u in M and
A4: v in M ; ::_thesis: (b3 * b1) + ((1 - b3) * b2) in M
percases ( ( 0 < r & r < 1 ) or 0 = r or r = 1 ) by A2, XXREAL_0:1;
suppose ( 0 < r & r < 1 ) ; ::_thesis: (b3 * b1) + ((1 - b3) * b2) in M
hence  (r * u) + ((1 - r) * v) in M by A1, A3, A4, CONVEX1:def_2; ::_thesis: verum
end;
suppose 0 = r ; ::_thesis: (b3 * b1) + ((1 - b3) * b2) in M
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, RLVECT_1:def_4; ::_thesis: verum
end;
suppose r = 1 ; ::_thesis: (b3 * b1) + ((1 - b3) * b2) in M
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, RLVECT_1:def_4; ::_thesis: verum
end;
end;
end;
assume A5: for u, v being Point of V
for r being Real st 0 <= r & r <= 1 & u in M & v in M holds
(r * u) + ((1 - r) * v) in M ; ::_thesis: M is convex
let u, v be Point of V; :: according to CONVEX1:def_2 ::_thesis: for b1 being Element of REAL holds
( b1 <= 0 or 1 <= b1 or not u in M or not v in M or (b1 * u) + ((1 - b1) * v) in M )
let r be Real; ::_thesis: ( r <= 0 or 1 <= r or not u in M or not v in M or (r * u) + ((1 - r) * v) in M )
thus  ( r <= 0 or 1 <= r or not u in M or not v in M or (r * u) + ((1 - r) * v) in M ) by A5; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines convex RLTOPSP1:def_1_:_
 for V being RealLinearSpace
for M being Subset of V holds
( M is convex iff for u, v being Point of V
for r being Real st 0 <= r & r <= 1 & u in M & v in M holds
(r * u) + ((1 - r) * v) in M );

Lm4:  for X being RealLinearSpace holds conv ({} X) = {}
proof
let X be RealLinearSpace; ::_thesis: conv ({} X) = {}
 {} X is convex by CONVEX1:10;
then  {} X in Convex-Family ({} X) by CONVEX1:def_4;
hence  conv ({} X) = {} by SETFAM_1:4; ::_thesis: verum
end;

registration
let X be RealLinearSpace;
let M be empty Subset of X;
cluster conv M ->  empty ;
coherence
 conv M is empty
proof
 M = {} X ;
hence  conv M is empty by Lm4; ::_thesis: verum
end;
end;

theorem :: RLTOPSP1:17
for X being RealLinearSpace
for M being convex Subset of X holds conv M = M
proof
let X be RealLinearSpace; ::_thesis: for M being convex Subset of X holds conv M = M
let M be convex Subset of X; ::_thesis: conv M = M
thus  conv M c= M by CONVEX1:30; :: according to XBOOLE_0:def_10 ::_thesis: M c= conv M
thus  M c= conv M by CONVEX1:41; ::_thesis: verum
end;

theorem Th18: :: RLTOPSP1:18
for X being RealLinearSpace
for M being Subset of X
for r being Real holds r * (conv M) = conv (r * M)
proof
let X be RealLinearSpace; ::_thesis: for M being Subset of X
for r being Real holds r * (conv M) = conv (r * M)
let M be Subset of X; ::_thesis: for r being Real holds r * (conv M) = conv (r * M)
let r be Real; ::_thesis: r * (conv M) = conv (r * M)
thus  r * (conv M) c= conv (r * M) :: according to XBOOLE_0:def_10 ::_thesis: conv (r * M) c= r * (conv M)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in r * (conv M) or x in conv (r * M) )
percases ( r = 0 or r <> 0 ) ;
supposeA1: r = 0 ; ::_thesis: ( not x in r * (conv M) or x in conv (r * M) )
percases ( M = {} or M <> {} ) ;
suppose M = {} ; ::_thesis: ( not x in r * (conv M) or x in conv (r * M) )
hence  ( not x in r * (conv M) or x in conv (r * M) ) by CONVEX1:33; ::_thesis: verum
end;
supposeA2: M <> {} ; ::_thesis: ( not x in r * (conv M) or x in conv (r * 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  ( not x in r * (conv M) or x in conv (r * M) ) by A3; ::_thesis: verum
end;
end;
end;
supposeA4: r <> 0 ; ::_thesis: ( not x in r * (conv M) or x in conv (r * M) )
assume  x in r * (conv M) ; ::_thesis: x in conv (r * M)
then consider v being Point of X such that
A5: x = r * v and
A6: v in conv M ;
 for V being set st V in Convex-Family (r * M) holds
r * v in V
proof
let V be set ; ::_thesis: ( V in Convex-Family (r * M) implies r * v in V )
assume A7: V in Convex-Family (r * M) ; ::_thesis: r * v in V
then reconsider V = 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 being 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  r * v in V by A10; ::_thesis: verum
end;
hence  x in conv (r * M) by A5, SETFAM_1:def_1; ::_thesis: verum
end;
end;
end;
 ( r * M c= r * (conv M) & r * (conv M) is convex ) by CONVEX1:1, CONVEX1:39, CONVEX1:41;
hence  conv (r * M) c= r * (conv M) by CONVEX1:30; ::_thesis: verum
end;

theorem Th19: :: RLTOPSP1:19
for X being RealLinearSpace
for M1, M2 being Subset of X st M1 c= M2 holds
Convex-Family M2 c= Convex-Family M1
proof
let X be RealLinearSpace; ::_thesis: for M1, M2 being Subset of X st M1 c= M2 holds
Convex-Family M2 c= Convex-Family M1
let M1, M2 be Subset of X; ::_thesis: ( M1 c= M2 implies Convex-Family M2 c= Convex-Family M1 )
assume A1: M1 c= M2 ; ::_thesis: Convex-Family M2 c= Convex-Family M1
let M be set ; :: according to TARSKI:def_3 ::_thesis: ( not M in Convex-Family M2 or M in Convex-Family M1 )
assume A2: M in Convex-Family M2 ; ::_thesis: M in Convex-Family M1
then reconsider M = M as Subset of X ;
 M2 c= M by A2, CONVEX1:def_4;
then A3: M1 c= M by A1, XBOOLE_1:1;
 M is convex by A2, CONVEX1:def_4;
hence  M in Convex-Family M1 by A3, CONVEX1:def_4; ::_thesis: verum
end;

theorem Th20: :: RLTOPSP1:20
for X being RealLinearSpace
for M1, M2 being Subset of X st M1 c= M2 holds
conv M1 c= conv M2
proof
let X be RealLinearSpace; ::_thesis: for M1, M2 being Subset of X st M1 c= M2 holds
conv M1 c= conv M2
let M1, M2 be Subset of X; ::_thesis: ( M1 c= M2 implies conv M1 c= conv M2 )
assume  M1 c= M2 ; ::_thesis: conv M1 c= conv 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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in conv M1 or x in conv M2 )
assume  x in conv M1 ; ::_thesis: x in conv M2
hence  x in conv M2 by A1; ::_thesis: verum
end;

theorem :: RLTOPSP1:21
for X being RealLinearSpace
for M being convex Subset of X
for r being Real st 0 <= r & r <= 1 & 0. X in M holds
r * M c= M
proof
let X be RealLinearSpace; ::_thesis: for M being convex Subset of X
for r being Real st 0 <= r & r <= 1 & 0. X in M holds
r * M c= M
let M be convex Subset of X; ::_thesis: for r being Real st 0 <= r & r <= 1 & 0. X in M holds
r * M c= M
let r be Real; ::_thesis: ( 0 <= r & r <= 1 & 0. X in M implies r * M c= M )
assume A1: ( 0 <= r & r <= 1 & 0. X in M ) ; ::_thesis: r * M c= M
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in r * M or x in M )
assume  x in r * M ; ::_thesis: x in M
then consider v being 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 by RLVECT_1:10;
hence  x in M by A2, RLVECT_1:def_4; ::_thesis: verum
end;

definition
let X be RealLinearSpace;
let v, w be Point of X;
func LSeg (v,w) ->  Subset of X equals :: RLTOPSP1:def 2
 {  (((1 - r) * v) + (r * w)) where r is Real : ( 0 <= r & r <= 1 )  }  ;
coherence
  {  (((1 - r) * v) + (r * w)) where r is Real : ( 0 <= r & r <= 1 )  }  is Subset of X
proof
  {  (((1 - r) * v) + (r * w)) where r is Real : ( 0 <= r & r <= 1 )  }  c= the carrier of X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (((1 - r) * v) + (r * w)) where r is Real : ( 0 <= r & r <= 1 )  }  or x in the carrier of X )
assume  x in  {  (((1 - r) * v) + (r * w)) where r is Real : ( 0 <= r & r <= 1 )  }  ; ::_thesis: x in the carrier of X
then  ex r being Real st
( x = ((1 - r) * v) + (r * w) & 0 <= r & r <= 1 ) ;
hence  x in the carrier of X ; ::_thesis: verum
end;
hence   {  (((1 - r) * v) + (r * w)) where r is Real : ( 0 <= r & r <= 1 )  }  is Subset of X ; ::_thesis: verum
end;
commutativity
 for b1 being Subset of X
for v, w being Point of X st b1 =  {  (((1 - r) * v) + (r * w)) where r is Real : ( 0 <= r & r <= 1 )  }  holds
b1 =  {  (((1 - r) * w) + (r * v)) where r is Real : ( 0 <= r & r <= 1 )  }
proof
let A be Subset of X; ::_thesis: for v, w being Point of X st A =  {  (((1 - r) * v) + (r * w)) where r is Real : ( 0 <= r & r <= 1 )  }  holds
A =  {  (((1 - r) * w) + (r * v)) where r is Real : ( 0 <= r & r <= 1 )  }
let v, w be Point of X; ::_thesis: ( A =  {  (((1 - r) * v) + (r * w)) where r is Real : ( 0 <= r & r <= 1 )  }  implies A =  {  (((1 - r) * w) + (r * v)) where r is Real : ( 0 <= r & r <= 1 )  }  )
assume A1: A =  {  (((1 - r) * v) + (r * w)) where r is Real : ( 0 <= r & r <= 1 )  }  ; ::_thesis: A =  {  (((1 - r) * w) + (r * v)) where r is Real : ( 0 <= r & r <= 1 )  }
thus  A c=  {  (((1 - r) * w) + (r * v)) where r is Real : ( 0 <= r & r <= 1 )  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  (((1 - r) * w) + (r * v)) where r is Real : ( 0 <= r & r <= 1 )  }  c= A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in  {  (((1 - r) * w) + (r * v)) where r is Real : ( 0 <= r & r <= 1 )  }  )
assume  x in A ; ::_thesis: x in  {  (((1 - r) * w) + (r * v)) where r is Real : ( 0 <= r & r <= 1 )  }
then consider r being Real 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  x in  {  (((1 - r) * w) + (r * v)) where r is Real : ( 0 <= r & r <= 1 )  }  by A2, A4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (((1 - r) * w) + (r * v)) where r is Real : ( 0 <= r & r <= 1 )  }  or x in A )
assume  x in  {  (((1 - r) * w) + (r * v)) where r is Real : ( 0 <= r & r <= 1 )  }  ; ::_thesis: x in A
then consider r being Real 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  x in A by A1, A5, A7; ::_thesis: verum
end;
end;

:: deftheorem  defines LSeg RLTOPSP1:def_2_:_
 for X being RealLinearSpace
for v, w being Point of X holds LSeg (v,w) =  {  (((1 - r) * v) + (r * w)) where r is Real : ( 0 <= r & r <= 1 )  }  ;

registration
let X be RealLinearSpace;
let v, w be Point of X;
cluster LSeg (v,w) ->  non empty convex ;
coherence
 ( not LSeg (v,w) is empty & LSeg (v,w) is convex )
proof
A1: ( 0 * w = 0. X & v + (0. X) = v ) by RLVECT_1:10, RLVECT_1:def_4;
 ( 1 - 0 = 1 & 1 * v = v ) by RLVECT_1:def_8;
then  v in LSeg (v,w) by A1;
hence  not LSeg (v,w) is empty ; ::_thesis: LSeg (v,w) is convex
let u, u9 be Point of X; :: according to RLTOPSP1:def_1 ::_thesis: for r being Real st 0 <= r & r <= 1 & u in LSeg (v,w) & u9 in LSeg (v,w) holds
(r * u) + ((1 - r) * u9) in LSeg (v,w)
let r be Real; ::_thesis: ( 0 <= r & r <= 1 & u in LSeg (v,w) & u9 in LSeg (v,w) implies (r * u) + ((1 - r) * u9) in LSeg (v,w) )
assume that
A2: 0 <= r and
A3: r <= 1 ; ::_thesis: ( not u in LSeg (v,w) or not u9 in LSeg (v,w) or (r * u) + ((1 - r) * u9) in LSeg (v,w) )
A4: 0 <= 1 - r by A3, XREAL_1:48;
assume  u in LSeg (v,w) ; ::_thesis: ( not u9 in LSeg (v,w) or (r * u) + ((1 - r) * u9) in LSeg (v,w) )
then consider s being 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) ; ::_thesis: (r * u) + ((1 - r) * u9) in LSeg (v,w)
then consider t being 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  (r * u) + ((1 - r) * u9) in LSeg (v,w) by A2, A6, A10, A12, A4; ::_thesis: verum
end;
end;

theorem :: RLTOPSP1:22
for X being RealLinearSpace
for M being Subset of X holds
( M is convex iff for u, w being Point of X st u in M & w in M holds
LSeg (u,w) c= M )
proof
let X be RealLinearSpace; ::_thesis: for M being Subset of X holds
( M is convex iff for u, w being Point of X st u in M & w in M holds
LSeg (u,w) c= M )
let M be Subset of X; ::_thesis: ( M is convex iff for u, w being Point of X st u in M & w in M holds
LSeg (u,w) c= M )
hereby  ::_thesis: ( ( for u, w being Point of X st u in M & w in M holds
LSeg (u,w) c= M ) implies M is convex )
assume A1: M is convex ; ::_thesis: for u, w being Point of X st u in M & w in M holds
LSeg (u,w) c= M
let u, w be Point of X; ::_thesis: ( u in M & w in M implies LSeg (u,w) c= M )
assume A2: ( u in M & w in M ) ; ::_thesis: LSeg (u,w) c= M
now__::_thesis:_for_x_being_set_st_x_in_LSeg_(u,w)_holds_
x_in_M
let x be set ; ::_thesis: ( x in LSeg (u,w) implies x in M )
assume  x in LSeg (u,w) ; ::_thesis: x in M
then  ex r being Real st
( x = ((1 - r) * u) + (r * w) & 0 <= r & r <= 1 ) ;
hence  x in M by A1, A2, Def1; ::_thesis: verum
end;
hence  LSeg (u,w) c= M by TARSKI:def_3; ::_thesis: verum
end;
assume A3: for w, u being Point of X st w in M & u in M holds
LSeg (w,u) c= M ; ::_thesis: M is convex
let u, w be Point of X; :: according to RLTOPSP1:def_1 ::_thesis: for r being Real st 0 <= r & r <= 1 & u in M & w in M holds
(r * u) + ((1 - r) * w) in M
let r be Real; ::_thesis: ( 0 <= r & r <= 1 & u in M & w in M implies (r * u) + ((1 - r) * w) in M )
assume that
A4: ( 0 <= r & r <= 1 ) and
A5: ( u in M & w in M ) ; ::_thesis: (r * u) + ((1 - r) * w) in M
A6: (r * u) + ((1 - r) * w) in LSeg (w,u) by A4;
 LSeg (w,u) c= M by A3, A5;
hence  (r * u) + ((1 - r) * w) in M by A6; ::_thesis: verum
end;

definition
let V be non empty RLSStruct ;
let P be Subset-Family of V;
attrP is convex-membered  means :Def3: :: RLTOPSP1:def 3
 for M being Subset of V st M in P holds
M is convex ;
end;

:: deftheorem Def3 defines convex-membered RLTOPSP1:def_3_:_
 for V being non empty RLSStruct
for P being Subset-Family of V holds
( P is convex-membered iff for M being Subset of V st M in P holds
M is convex );

registration
let V be non empty RLSStruct ;
cluster non empty convex-membered for Element of bool (bool the carrier of V);
existence
 ex b1 being Subset-Family of V st
( not b1 is empty & b1 is convex-membered )
proof
reconsider F = {({} V)} as Subset-Family of V ;
take  F ; ::_thesis: ( not F is empty & F is convex-membered )
thus  not F is empty ; ::_thesis: F is convex-membered
let M be Subset of V; :: according to RLTOPSP1:def_3 ::_thesis: ( M in F implies M is convex )
assume  M in F ; ::_thesis: M is convex
then  M = {} V by TARSKI:def_1;
hence  M is convex by CONVEX1:10; ::_thesis: verum
end;
end;

theorem :: RLTOPSP1:23
for V being non empty RLSStruct
for F being convex-membered Subset-Family of V holds meet F is convex
proof
let V be non empty RLSStruct ; ::_thesis: for F being convex-membered Subset-Family of V holds meet F is convex
let F be convex-membered Subset-Family of V; ::_thesis: meet F is convex
 for M being Subset of V st M in F holds
M is convex by Def3;
hence  meet F is convex by CONVEX1:15; ::_thesis: verum
end;

definition
let X be non empty RLSStruct ;
let A be Subset of X;
func - A ->  Subset of X equals :: RLTOPSP1:def 4
(- 1) * A;
coherence
 (- 1) * A is Subset of X ;
end;

:: deftheorem  defines - RLTOPSP1:def_4_:_
 for X being non empty RLSStruct
for A being Subset of X holds - A = (- 1) * A;

theorem Th24: :: RLTOPSP1:24
for X being RealLinearSpace
for M, N being Subset of X
for v being Point of X holds
( v + M meets N iff v in N + (- M) )
proof
let X be RealLinearSpace; ::_thesis: for M, N being Subset of X
for v being Point of X holds
( v + M meets N iff v in N + (- M) )
let M, N be Subset of X; ::_thesis: for v being Point of X holds
( v + M meets N iff v in N + (- M) )
let v be Point of X; ::_thesis: ( v + M meets N iff v in N + (- M) )
A1: N + ((- 1) * M) =  {  (u + w) where u, w is Point of X : ( u in N & w in (- 1) * M )  }  by RUSUB_4:def_9;
hereby  ::_thesis: ( v in N + (- M) implies v + M meets N )
A2: v + M =  {  (v + u) where u is Point of X : u in M  }  by RUSUB_4:def_8;
assume  v + M meets N ; ::_thesis: v in N + (- M)
then consider z being set  such that
A3: z in v + M and
A4: z in N by XBOOLE_0:3;
consider u being Point of X such that
A5: v + u = z and
A6: u in M by A3, A2;
reconsider z = 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 by RLVECT_1:4 ;
hence  v in N + (- M) by A4, A7, Th3; ::_thesis: verum
end;
assume  v in N + (- M) ; ::_thesis: v + M meets N
then consider u, w being Point of X such that
A8: v = u + w and
A9: u in N and
A10: w in (- 1) * M by A1;
consider w9 being 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 by RLVECT_1:4 ;
then  u in v + M by A12, Lm1;
hence  v + M meets N by A9, XBOOLE_0:3; ::_thesis: verum
end;

definition
let X be non empty RLSStruct ;
let A be Subset of X;
attrA is symmetric  means :Def5: :: RLTOPSP1:def 5
A = - A;
end;

:: deftheorem Def5 defines symmetric RLTOPSP1:def_5_:_
 for X being non empty RLSStruct
for A being Subset of X holds
( A is symmetric iff A = - A );

registration
let X be RealLinearSpace;
cluster non empty symmetric for Element of bool the carrier of X;
existence
 ex b1 being Subset of X st
( not b1 is empty & b1 is symmetric )
proof
take V = {(0. X)}; ::_thesis: ( not V is empty & V is symmetric )
thus  not V is empty ; ::_thesis: V is symmetric
thus  V = - V by Th13; :: according to RLTOPSP1:def_5 ::_thesis: verum
end;
end;

theorem Th25: :: RLTOPSP1:25
for X being RealLinearSpace
for A being symmetric Subset of X
for x being Point of X st x in A holds
- x in A
proof
let X be RealLinearSpace; ::_thesis: for A being symmetric Subset of X
for x being Point of X st x in A holds
- x in A
let A be symmetric Subset of X; ::_thesis: for x being Point of X st x in A holds
- x in A
let x be Point of X; ::_thesis: ( x in A implies - x in A )
assume A1: x in A ; ::_thesis: - x in A
A = - A by Def5
.= (- 1) * A ;
then consider v being 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  - x in A by A3, RLVECT_1:16; ::_thesis: verum
end;

definition
let X be non empty RLSStruct ;
let A be Subset of X;
attrA is circled  means :Def6: :: RLTOPSP1:def 6
 for r being Real st abs r <= 1 holds
r * A c= A;
end;

:: deftheorem Def6 defines circled RLTOPSP1:def_6_:_
 for X being non empty RLSStruct
for A being Subset of X holds
( A is circled iff for r being Real st abs r <= 1 holds
r * A c= A );

registration
let X be non empty RLSStruct ;
cluster empty  ->  circled for Element of bool the carrier of X;
coherence
 for b1 being Subset of X st b1 is empty holds
b1 is circled
proof
let S be Subset of X; ::_thesis: ( S is empty implies S is circled )
assume  S is empty ; ::_thesis: S is circled
then A1: S = {} X ;
let r be Real; :: according to RLTOPSP1:def_6 ::_thesis: ( abs r <= 1 implies r * S c= S )
thus  ( abs r <= 1 implies r * S c= S ) by A1, CONVEX1:33; ::_thesis: verum
end;
end;

theorem Th26: :: RLTOPSP1:26
for X being RealLinearSpace holds {(0. X)} is circled
proof
let X be RealLinearSpace; ::_thesis: {(0. X)} is circled
let r be Real; :: according to RLTOPSP1:def_6 ::_thesis: ( abs r <= 1 implies r * {(0. X)} c= {(0. X)} )
assume  abs r <= 1 ; ::_thesis: r * {(0. X)} c= {(0. X)}
thus  r * {(0. X)} c= {(0. X)} by Th13; ::_thesis: verum
end;

registration
let X be RealLinearSpace;
cluster non empty circled for Element of bool the carrier of X;
existence
 ex b1 being Subset of X st
( not b1 is empty & b1 is circled )
proof
take  {(0. X)} ; ::_thesis: ( not {(0. X)} is empty & {(0. X)} is circled )
thus  ( not {(0. X)} is empty & {(0. X)} is circled ) by Th26; ::_thesis: verum
end;
end;

theorem Th27: :: RLTOPSP1:27
for X being RealLinearSpace
for B being non empty circled Subset of X holds 0. X in B
proof
let X be RealLinearSpace; ::_thesis: for B being non empty circled Subset of X holds 0. X in B
let B be non empty circled Subset of X; ::_thesis: 0. X in B
 abs 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  0. X in B by A1; ::_thesis: verum
end;

Lm5:  for X being RealLinearSpace
for A, B being circled Subset of X holds A + B is circled
proof
let X be RealLinearSpace; ::_thesis: for A, B being circled Subset of X holds A + B is circled
let A, B be circled Subset of X; ::_thesis: A + B is circled
A1: A + B =  {  (u + v) where u, v is Point of X : ( u in A & v in B )  }  by RUSUB_4:def_9;
let r be Real; :: according to RLTOPSP1:def_6 ::_thesis: ( abs r <= 1 implies r * (A + B) c= A + B )
assume  abs r <= 1 ; ::_thesis: r * (A + B) c= A + B
then A2: ( r * A c= A & r * B c= B ) by Def6;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in r * (A + B) or x in A + B )
assume  x in r * (A + B) ; ::_thesis: x in A + B
then consider x9 being Point of X such that
A3: x = r * x9 and
A4: x9 in A + B ;
consider u, v being 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  x in A + B by A2, A7, Th3; ::_thesis: verum
end;

registration
let X be RealLinearSpace;
let A, B be circled Subset of X;
clusterA + B ->  circled ;
coherence
 A + B is circled by Lm5;
end;

theorem Th28: :: RLTOPSP1:28
for X being RealLinearSpace
for A being circled Subset of X
for r being Real st abs r = 1 holds
r * A = A
proof
let X be RealLinearSpace; ::_thesis: for A being circled Subset of X
for r being Real st abs r = 1 holds
r * A = A
let A be circled Subset of X; ::_thesis: for r being Real st abs r = 1 holds
r * A = A
let r be Real; ::_thesis: ( abs r = 1 implies r * A = A )
assume A1: abs r = 1 ; ::_thesis: r * A = A
hence A2: r * A c= A by Def6; :: according to XBOOLE_0:def_10 ::_thesis: A c= r * A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in r * A )
assume A3: x in A ; ::_thesis: x in r * A
then reconsider x = x as Point of X ;
A4: r * x in r * A by A3;
percases ( 0 <= r or r < 0 ) ;
suppose 0 <= r ; ::_thesis: x in r * A
then  r = 1 by A1, ABSVALUE:def_1;
hence  x in r * A by A3, CONVEX1:32; ::_thesis: verum
end;
suppose r < 0 ; ::_thesis: x in r * A
then  abs 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  x in r * A by RLVECT_1:def_8; ::_thesis: verum
end;
end;
end;

Lm6:  for X being RealLinearSpace
for A being circled Subset of X holds A is symmetric
proof
let X be RealLinearSpace; ::_thesis: for A being circled Subset of X holds A is symmetric
let A be circled Subset of X; ::_thesis: A is symmetric
abs (- 1) = - (- 1) by ABSVALUE:def_1
.= 1 ;
hence  A = - A by Th28; :: according to RLTOPSP1:def_5 ::_thesis: verum
end;

registration
let X be RealLinearSpace;
cluster circled  ->  symmetric for Element of bool the carrier of X;
coherence
 for b1 being Subset of X st b1 is circled holds
b1 is symmetric by Lm6;
end;

Lm7:  for X being RealLinearSpace
for M being circled Subset of X holds conv M is circled
proof
let X be RealLinearSpace; ::_thesis: for M being circled Subset of X holds conv M is circled
let M be circled Subset of X; ::_thesis: conv M is circled
let r be Real; :: according to RLTOPSP1:def_6 ::_thesis: ( abs r <= 1 implies r * (conv M) c= conv M )
assume  abs r <= 1 ; ::_thesis: r * (conv M) c= conv M
then A1: r * M c= M by Def6;
 r * (conv M) = conv (r * M) by Th18;
hence  r * (conv M) c= conv M by A1, Th20; ::_thesis: verum
end;

registration
let X be RealLinearSpace;
let M be circled Subset of X;
cluster conv M ->  circled ;
coherence
 conv M is circled by Lm7;
end;

definition
let X be non empty RLSStruct ;
let F be Subset-Family of X;
attrF is circled-membered  means :Def7: :: RLTOPSP1:def 7
 for V being Subset of X st V in F holds
V is circled ;
end;

:: deftheorem Def7 defines circled-membered RLTOPSP1:def_7_:_
 for X being non empty RLSStruct
for F being Subset-Family of X holds
( F is circled-membered iff for V being Subset of X st V in F holds
V is circled );

registration
let V be non empty RLSStruct ;
cluster non empty circled-membered for Element of bool (bool the carrier of V);
existence
 ex b1 being Subset-Family of V st
( not b1 is empty & b1 is circled-membered )
proof
reconsider F = {({} V)} as Subset-Family of V ;
take  F ; ::_thesis: ( not F is empty & F is circled-membered )
thus  not F is empty ; ::_thesis: F is circled-membered
let M be Subset of V; :: according to RLTOPSP1:def_7 ::_thesis: ( M in F implies M is circled )
assume  M in F ; ::_thesis: M is circled
hence  M is circled by TARSKI:def_1; ::_thesis: verum
end;
end;

theorem :: RLTOPSP1:29
for X being non empty RLSStruct
for F being circled-membered Subset-Family of X holds union F is circled
proof
let X be non empty RLSStruct ; ::_thesis: for F being circled-membered Subset-Family of X holds union F is circled
let F be circled-membered Subset-Family of X; ::_thesis: union F is circled
let r be Real; :: according to RLTOPSP1:def_6 ::_thesis: ( abs r <= 1 implies r * (union F) c= union F )
assume A1: abs r <= 1 ; ::_thesis: r * (union F) c= union F
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in r * (union F) or x in union F )
assume  x in r * (union F) ; ::_thesis: x in union F
then consider x9 being Point of X such that
A2: x = r * x9 and
A3: x9 in union F ;
consider Y being set  such that
A4: x9 in Y and
A5: Y in F by A3, TARSKI:def_4;
reconsider Y = Y as Subset of X by A5;
 Y is circled by A5, Def7;
then A6: r * Y c= Y by A1, Def6;
 r * x9 in r * Y by A4;
hence  x in union F by A2, A5, A6, TARSKI:def_4; ::_thesis: verum
end;

theorem :: RLTOPSP1:30
for X being non empty RLSStruct
for F being circled-membered Subset-Family of X holds meet F is circled
proof
let X be non empty RLSStruct ; ::_thesis: for F being circled-membered Subset-Family of X holds meet F is circled
let F be circled-membered Subset-Family of X; ::_thesis: meet F is circled
let r be Real; :: according to RLTOPSP1:def_6 ::_thesis: ( abs r <= 1 implies r * (meet F) c= meet F )
assume A1: abs r <= 1 ; ::_thesis: r * (meet F) c= meet F
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in r * (meet F) or x in meet F )
assume  x in r * (meet F) ; ::_thesis: x in meet F
then consider x9 being Point of X such that
A2: x = r * x9 and
A3: x9 in meet F ;
A4: now__::_thesis:_for_Y_being_set_st_Y_in_F_holds_
x_in_Y
let Y be set ; ::_thesis: ( Y in F implies x in Y )
assume A5: Y in F ; ::_thesis: x in Y
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, Def6;
hence  x in Y by A2, A6; ::_thesis: verum
end;
 F <> {} by A3, SETFAM_1:def_1;
hence  x in meet F by A4, SETFAM_1:def_1; ::_thesis: verum
end;

begin

definition
attrc1 is strict ;
struct RLTopStruct  ->  RLSStruct , TopStruct ;
aggrRLTopStruct(# carrier, ZeroF, addF, Mult, topology #) ->  RLTopStruct ;
end;

registration
let X be non empty set ;
let O be Element of X;
let F be BinOp of X;
let G be Function of [:REAL,X:],X;
let T be Subset-Family of X;
cluster RLTopStruct(# X,O,F,G,T #) ->  non empty ;
coherence
 not RLTopStruct(# X,O,F,G,T #) is empty ;
end;

registration
cluster non empty strict for RLTopStruct ;
existence
 ex b1 being RLTopStruct st
( b1 is strict & not b1 is empty )
proof
set X = {0};
reconsider O = 0 as Element of {0} by TARSKI:def_1;
set F = the BinOp of {0};
set G = the Function of [:REAL,{0}:],{0};
take RT = RLTopStruct(# {0},O, the BinOp of {0}, the Function of [:REAL,{0}:],{0},({} (bool {0})) #); ::_thesis: ( RT is strict & not RT is empty )
thus  RT is strict ; ::_thesis: not RT is empty
thus  not the carrier of RT is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;

definition
let X be non empty RLTopStruct ;
attrX is add-continuous  means :Def8: :: RLTOPSP1:def 8
 for x1, x2 being Point of X
for V being Subset of X st V is open & x1 + x2 in V holds
ex V1, V2 being Subset of X st
( V1 is open & V2 is open & x1 in V1 & x2 in V2 & V1 + V2 c= V );
attrX is Mult-continuous  means :Def9: :: RLTOPSP1:def 9
 for a being Real
for x being Point of X
for V being Subset of X st V is open & a * x in V holds
ex r being positive Real ex W being Subset of X st
( W is open & x in W & ( for s being Real st abs (s - a) < r holds
s * W c= V ) );
end;

:: deftheorem Def8 defines add-continuous RLTOPSP1:def_8_:_
 for X being non empty RLTopStruct holds
( X is add-continuous iff for x1, x2 being Point of X
for V being Subset of X st V is open & x1 + x2 in V holds
ex V1, V2 being Subset of X st
( V1 is open & V2 is open & x1 in V1 & x2 in V2 & V1 + V2 c= V ) );

:: deftheorem Def9 defines Mult-continuous RLTOPSP1:def_9_:_
 for X being non empty RLTopStruct holds
( X is Mult-continuous iff for a being Real
for x being Point of X
for V being Subset of X st V is open & a * x in V holds
ex r being positive Real ex W being Subset of X st
( W is open & x in W & ( for s being Real st abs (s - a) < r holds
s * W c= V ) ) );

registration
cluster non empty TopSpace-like right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital strict add-continuous Mult-continuous for RLTopStruct ;
existence
 ex b1 being non empty RLTopStruct st
( b1 is strict & b1 is add-continuous & b1 is Mult-continuous & b1 is TopSpace-like & b1 is Abelian & b1 is add-associative & b1 is right_zeroed & b1 is right_complementable & b1 is vector-distributive & b1 is scalar-distributive & b1 is scalar-associative & b1 is scalar-unital )
proof
set ZS = {0};
set T = {{},{0}};
 {{},{0}} c= bool {0}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {{},{0}} or x in bool {0} )
assume  x in {{},{0}} ; ::_thesis: x in bool {0}
then  ( x = {} or x = {0} ) by TARSKI:def_2;
then  x c= {0} by XBOOLE_1:2;
hence  x in bool {0} ; ::_thesis: verum
end;
then reconsider T = {{},{0}} as Subset-Family of {0} ;
reconsider O = 0 as Element of {0} by TARSKI:def_1;
deffunc H1( Element of {0}, Element of {0}) ->  Element of {0} = O;
consider F being BinOp of {0} such that
A1: for x, y being Element of {0} holds F . (x,y) = H1(x,y) from BINOP_1:sch_4();
deffunc H2( real number , Element of {0}) ->  Element of {0} = O;
consider G being Function of [:REAL,{0}:],{0} such that
A2: for a being Element of REAL
for x being Element of {0} holds G . (a,x) = H2(a,x) from BINOP_1:sch_4();
take W = RLTopStruct(# {0},O,F,G,T #); ::_thesis: ( W is strict & W is add-continuous & W is Mult-continuous & W is TopSpace-like & W is Abelian & W is add-associative & W is right_zeroed & W is right_complementable & W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is scalar-unital )
thus  W is strict ; ::_thesis: ( W is add-continuous & W is Mult-continuous & W is TopSpace-like & W is Abelian & W is add-associative & W is right_zeroed & W is right_complementable & W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is scalar-unital )
thus  W is add-continuous ::_thesis: ( W is Mult-continuous & W is TopSpace-like & W is Abelian & W is add-associative & W is right_zeroed & W is right_complementable & W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is scalar-unital )
proof
reconsider V1 = {O}, V2 = {O} as Subset of W ;
let x1, x2 be Point of W; :: according to RLTOPSP1:def_8 ::_thesis: for V being Subset of W st V is open & x1 + x2 in V holds
ex V1, V2 being Subset of W st
( V1 is open & V2 is open & x1 in V1 & x2 in V2 & V1 + V2 c= V )
let V be Subset of W; ::_thesis: ( V is open & x1 + x2 in V implies ex V1, V2 being Subset of W st
( V1 is open & V2 is open & x1 in V1 & x2 in V2 & V1 + V2 c= V ) )
assume that
A3: V is open and
A4: x1 + x2 in V ; ::_thesis: ex V1, V2 being Subset of W st
( V1 is open & V2 is open & x1 in V1 & x2 in V2 & V1 + V2 c= V )
take  V1 ; ::_thesis: ex V2 being Subset of W st
( V1 is open & V2 is open & x1 in V1 & x2 in V2 & V1 + V2 c= V )
take  V2 ; ::_thesis: ( V1 is open & V2 is open & x1 in V1 & x2 in V2 & V1 + V2 c= V )
 V1 in T by TARSKI:def_2;
hence  ( V1 is open & V2 is open ) by PRE_TOPC:def_2; ::_thesis: ( x1 in V1 & x2 in V2 & V1 + V2 c= V )
thus  ( x1 in V1 & x2 in V2 ) ; ::_thesis: V1 + V2 c= V
 V in T by A3, PRE_TOPC:def_2;
then  V = the carrier of W by A4, TARSKI:def_2;
hence  V1 + V2 c= V ; ::_thesis: verum
end;
thus  W is Mult-continuous ::_thesis: ( W is TopSpace-like & W is Abelian & W is add-associative & W is right_zeroed & W is right_complementable & W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is scalar-unital )
proof
reconsider V9 = {O} as Subset of W ;
let a be Real; :: according to RLTOPSP1:def_9 ::_thesis: for x being Point of W
for V being Subset of W st V is open & a * x in V holds
ex r being positive Real ex W being Subset of W st
( W is open & x in W & ( for s being Real st abs (s - a) < r holds
s * W c= V ) )
let x be Point of W; ::_thesis: for V being Subset of W st V is open & a * x in V holds
ex r being positive Real ex W being Subset of W st
( W is open & x in W & ( for s being Real st abs (s - a) < r holds
s * W c= V ) )
let V be Subset of W; ::_thesis: ( V is open & a * x in V implies ex r being positive Real ex W being Subset of W st
( W is open & x in W & ( for s being Real st abs (s - a) < r holds
s * W c= V ) ) )
assume that
A5: V is open and
A6: a * x in V ; ::_thesis: ex r being positive Real ex W being Subset of W st
( W is open & x in W & ( for s being Real st abs (s - a) < r holds
s * W c= V ) )
take  1 ; ::_thesis: ex W being Subset of W st
( W is open & x in W & ( for s being Real st abs (s - a) < 1 holds
s * W c= V ) )
take  V9 ; ::_thesis: ( V9 is open & x in V9 & ( for s being Real st abs (s - a) < 1 holds
s * V9 c= V ) )
 V9 in T by TARSKI:def_2;
hence  V9 is open by PRE_TOPC:def_2; ::_thesis: ( x in V9 & ( for s being Real st abs (s - a) < 1 holds
s * V9 c= V ) )
thus  x in V9 ; ::_thesis: for s being Real st abs (s - a) < 1 holds
s * V9 c= V
let s be Real; ::_thesis: ( abs (s - a) < 1 implies s * V9 c= V )
assume  abs (s - a) < 1 ; ::_thesis: s * V9 c= V
 V in T by A5, PRE_TOPC:def_2;
then  ( V = {} or V = {0} ) by TARSKI:def_2;
hence  s * V9 c= V by A6; ::_thesis: verum
end;
thus  W is TopSpace-like ::_thesis: ( W is Abelian & W is add-associative & W is right_zeroed & W is right_complementable & W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is scalar-unital )
proof
thus  the carrier of W in the topology of W by TARSKI:def_2; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of bool (bool the carrier of W) holds
( not b1 c= the topology of W or union b1 in the topology of W ) ) & ( for b1, b2 being Element of bool the carrier of W holds
( not b1 in the topology of W or not b2 in the topology of W or b1 /\ b2 in the topology of W ) ) )
hereby  ::_thesis: for b1, b2 being Element of bool the carrier of W holds
( not b1 in the topology of W or not b2 in the topology of W or b1 /\ b2 in the topology of W )
let a be Subset-Family of W; ::_thesis: ( a c= the topology of W implies union a in the topology of W )
assume  a c= the topology of W ; ::_thesis: union a in the topology of W
then  ( a = {} or a = {{}} or a = {{0}} or a = {{},{0}} ) by ZFMISC_1:36;
then  ( union a = {} or union a = {0} or union a = {} \/ {0} ) by ZFMISC_1:2, ZFMISC_1:25, ZFMISC_1:75;
hence  union a in the topology of W by TARSKI:def_2; ::_thesis: verum
end;
let a, b be Subset of W; ::_thesis: ( not a in the topology of W or not b in the topology of W or a /\ b in the topology of W )
assume that
A7: a in the topology of W and
A8: b in the topology of W ; ::_thesis: a /\ b in the topology of W
A9: ( b = {} or b = {0} ) by A8, TARSKI:def_2;
 ( a = {} or a = {0} ) by A7, TARSKI:def_2;
hence  a /\ b in the topology of W by A9, TARSKI:def_2; ::_thesis: verum
end;
thus  for x, y being Point of W holds x + y = y + x :: according to RLVECT_1:def_2 ::_thesis: ( W is add-associative & W is right_zeroed & W is right_complementable & W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is scalar-unital )
proof
let x, y be Point of W; ::_thesis: x + y = y + x
reconsider X = x, Y = y as Element of {0} ;
 x + y = H1(X,Y) by A1;
hence  x + y = y + x by A1; ::_thesis: verum
end;
thus  for x, y, z being Point of W holds (x + y) + z = x + (y + z) :: according to RLVECT_1:def_3 ::_thesis: ( W is right_zeroed & W is right_complementable & W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is scalar-unital )
proof
let x, y, z be Point of W; ::_thesis: (x + y) + z = x + (y + z)
reconsider X = x, Y = y, Z = z as Element of {0} ;
 (x + y) + z = H1(H1(X,Y),Z) by A1;
hence  (x + y) + z = x + (y + z) by A1; ::_thesis: verum
end;
thus  for x being Point of W holds x + (0. W) = x :: according to RLVECT_1:def_4 ::_thesis: ( W is right_complementable & W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is scalar-unital )
proof
let x be Point of W; ::_thesis: x + (0. W) = x
reconsider X = x as Element of {0} ;
 x + (0. W) = H1(X,O) by A1;
hence  x + (0. W) = x by TARSKI:def_1; ::_thesis: verum
end;
thus  for x being Point of W holds x is right_complementable :: according to ALGSTR_0:def_16 ::_thesis: ( W is vector-distributive & W is scalar-distributive & W is scalar-associative & W is scalar-unital )
proof
reconsider y = O as Point of W ;
let x be Point of W; ::_thesis: x is right_complementable
take  y ; :: according to ALGSTR_0:def_11 ::_thesis: x + y = 0. W
thus  x + y = 0. W by A1; ::_thesis: verum
end;
thus  for a being real number
for x, y being Point of W holds a * (x + y) = (a * x) + (a * y) :: according to RLVECT_1:def_5 ::_thesis: ( W is scalar-distributive & W is scalar-associative & W is scalar-unital )
proof
let a be real number ; ::_thesis: for x, y being Point of W holds a * (x + y) = (a * x) + (a * y)
reconsider a = a as Real by XREAL_0:def_1;
let x, y be Point of W; ::_thesis: a * (x + y) = (a * x) + (a * y)
reconsider X = x, Y = y as Element of {0} ;
(a * x) + (a * y) = H2(a,H1(X,Y)) by A1
.= G . (a,H1(X,Y)) by A2
.= G . (a,(F . (x,y))) by A1 ;
hence  a * (x + y) = (a * x) + (a * y) ; ::_thesis: verum
end;
thus  for a, b being real number
for x being Point of W holds (a + b) * x = (a * x) + (b * x) :: according to RLVECT_1:def_6 ::_thesis: ( W is scalar-associative & W is scalar-unital )
proof
let a, b be real number ; ::_thesis: for x being Point of W holds (a + b) * x = (a * x) + (b * x)
let x be Point of W; ::_thesis: (a + b) * x = (a * x) + (b * x)
reconsider a = a, b = b as Real by XREAL_0:def_1;
set c = a + b;
reconsider X = x as Element of {0} ;
 (a + b) * x = H2(a + b,X) by A2;
hence  (a + b) * x = (a * x) + (b * x) by A1; ::_thesis: verum
end;
thus  for a, b being real number
for x being Point of W holds (a * b) * x = a * (b * x) :: according to RLVECT_1:def_7 ::_thesis: W is scalar-unital
proof
let a, b be real number ; ::_thesis: for x being Point of W holds (a * b) * x = a * (b * x)
let x be Point of W; ::_thesis: (a * b) * x = a * (b * x)
reconsider a = a, b = b as Real by XREAL_0:def_1;
set c = a * b;
reconsider X = x as Element of {0} ;
 (a * b) * x = H2(a * b,X) by A2;
hence  (a * b) * x = a * (b * x) by A2; ::_thesis: verum
end;
thus  for x being Point of W holds 1 * x = x :: according to RLVECT_1:def_8 ::_thesis: verum
proof
reconsider A9 = 1 as Element of REAL ;
let x be Point of W; ::_thesis: 1 * x = x
reconsider X = x as Element of {0} ;
 1 * x = H2(A9,X) by A2;
hence  1 * x = x by TARSKI:def_1; ::_thesis: verum
end;
end;
end;

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

theorem Th31: :: RLTOPSP1:31
for X being LinearTopSpace
for x1, x2 being Point of X
for V being a_neighborhood of x1 + x2 ex V1 being a_neighborhood of x1 ex V2 being a_neighborhood of x2 st V1 + V2 c= V
proof
let X be LinearTopSpace; ::_thesis: for x1, x2 being Point of X
for V being a_neighborhood of x1 + x2 ex V1 being a_neighborhood of x1 ex V2 being a_neighborhood of x2 st V1 + V2 c= V
let x1, x2 be Point of X; ::_thesis: for V being a_neighborhood of x1 + x2 ex V1 being a_neighborhood of x1 ex V2 being a_neighborhood of x2 st V1 + V2 c= V
let V be a_neighborhood of x1 + x2; ::_thesis: ex V1 being a_neighborhood of x1 ex V2 being a_neighborhood of x2 st V1 + V2 c= V
 x1 + x2 in Int V by CONNSP_2:def_1;
then consider V1, V2 being 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 = V2 as a_neighborhood of x2 by A4, CONNSP_2:def_1;
 Int V1 = V1 by A1, TOPS_1:23;
then reconsider V1 = V1 as a_neighborhood of x1 by A3, CONNSP_2:def_1;
take  V1 ; ::_thesis: ex V2 being a_neighborhood of x2 st V1 + V2 c= V
take  V2 ; ::_thesis: V1 + V2 c= V
 Int V c= V by TOPS_1:16;
hence  V1 + V2 c= V by A5, XBOOLE_1:1; ::_thesis: verum
end;

theorem Th32: :: RLTOPSP1:32
for X being LinearTopSpace
for a being Real
for x being Point of X
for V being a_neighborhood of a * x ex r being positive Real ex W being a_neighborhood of x st
for s being Real st abs (s - a) < r holds
s * W c= V
proof
let X be LinearTopSpace; ::_thesis: for a being Real
for x being Point of X
for V being a_neighborhood of a * x ex r being positive Real ex W being a_neighborhood of x st
for s being Real st abs (s - a) < r holds
s * W c= V
let a be Real; ::_thesis: for x being Point of X
for V being a_neighborhood of a * x ex r being positive Real ex W being a_neighborhood of x st
for s being Real st abs (s - a) < r holds
s * W c= V
let x be Point of X; ::_thesis: for V being a_neighborhood of a * x ex r being positive Real ex W being a_neighborhood of x st
for s being Real st abs (s - a) < r holds
s * W c= V
let V be a_neighborhood of a * x; ::_thesis: ex r being positive Real ex W being a_neighborhood of x st
for s being Real st abs (s - a) < r holds
s * W c= V
 a * x in Int V by CONNSP_2:def_1;
then consider r being positive Real, W being Subset of X such that
A1: W is open and
A2: x in W and
A3: for s being Real st abs (s - a) < r holds
s * W c= Int V by Def9;
 Int W = W by A1, TOPS_1:23;
then reconsider W = W as a_neighborhood of x by A2, CONNSP_2:def_1;
take  r ; ::_thesis: ex W being a_neighborhood of x st
for s being Real st abs (s - a) < r holds
s * W c= V
take  W ; ::_thesis: for s being Real st abs (s - a) < r holds
s * W c= V
let s be Real; ::_thesis: ( abs (s - a) < r implies s * W c= V )
assume  abs (s - a) < r ; ::_thesis: s * W c= V
then A4: s * W c= Int V by A3;
 Int V c= V by TOPS_1:16;
hence  s * W c= V by A4, XBOOLE_1:1; ::_thesis: verum
end;

definition
let X be non empty RLTopStruct ;
let a be Point of X;
func transl (a,X) ->  Function of X,X means :Def10: :: RLTOPSP1:def 10
 for x being Point of X holds it . x = a + x;
existence
 ex b1 being Function of X,X st
for x being Point of X holds b1 . x = a + x
proof
deffunc H1( Point of X) ->  Element of the carrier of X = a + $1;
consider F being Function of the carrier of X, the carrier of X such that
A1: for x being Point of X holds F . x = H1(x) from FUNCT_2:sch_4();
reconsider F = F as Function of X,X ;
take  F ; ::_thesis: for x being Point of X holds F . x = a + x
thus  for x being Point of X holds F . x = a + x by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of X,X st ( for x being Point of X holds b1 . x = a + x ) & ( for x being Point of X holds b2 . x = a + x ) holds
b1 = b2
proof
let F, G be Function of X,X; ::_thesis: ( ( for x being Point of X holds F . x = a + x ) & ( for x being Point of X holds G . x = a + x ) implies F = G )
assume that
A2: for x being Point of X holds F . x = a + x and
A3: for x being Point of X holds G . x = a + x ; ::_thesis: F = G
now__::_thesis:_for_x_being_Point_of_X_holds_F_._x_=_G_._x
let x be Point of X; ::_thesis: F . x = G . x
thus F . x = a + x by A2
.= G . x by A3 ; ::_thesis: verum
end;
hence  F = G by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def10 defines transl RLTOPSP1:def_10_:_
 for X being non empty RLTopStruct
for a being Point of X
for b3 being Function of X,X holds
( b3 = transl (a,X) iff for x being Point of X holds b3 . x = a + x );

theorem Th33: :: RLTOPSP1:33
for X being non empty RLTopStruct
for a being Point of X
for V being Subset of X holds (transl (a,X)) .: V = a + V
proof
let X be non empty RLTopStruct ; ::_thesis: for a being Point of X
for V being Subset of X holds (transl (a,X)) .: V = a + V
let a be Point of X; ::_thesis: for V being Subset of X holds (transl (a,X)) .: V = a + V
let V be Subset of X; ::_thesis: (transl (a,X)) .: V = a + V
thus  (transl (a,X)) .: V c= a + V :: according to XBOOLE_0:def_10 ::_thesis: a + V c= (transl (a,X)) .: V
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (transl (a,X)) .: V or y in a + V )
assume  y in (transl (a,X)) .: V ; ::_thesis: y in a + V
then consider c being 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  y in a + V by A1, Lm1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in a + V or x in (transl (a,X)) .: V )
assume  x in a + V ; ::_thesis: x in (transl (a,X)) .: V
then  x in  {  (a + u) where u is Point of X : u in V  }  by RUSUB_4:def_8;
then consider u being Point of X such that
A3: x = a + u and
A4: u in V ;
 x = (transl (a,X)) . u by A3, Def10;
hence  x in (transl (a,X)) .: V by A4, FUNCT_2:35; ::_thesis: verum
end;

theorem Th34: :: RLTOPSP1:34
for X being LinearTopSpace
for a being Point of X holds rng (transl (a,X)) = [#] X
proof
let X be LinearTopSpace; ::_thesis: for a being Point of X holds rng (transl (a,X)) = [#] X
let a be Point of X; ::_thesis: rng (transl (a,X)) = [#] X
thus  rng (transl (a,X)) c= [#] X ; :: according to XBOOLE_0:def_10 ::_thesis: [#] X c= rng (transl (a,X))
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in [#] X or y in rng (transl (a,X)) )
assume  y in [#] X ; ::_thesis: y in rng (transl (a,X))
then reconsider y = 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 by RLVECT_1:4 ;
hence  y in rng (transl (a,X)) by FUNCT_2:4; ::_thesis: verum
end;

Lm8:  for X being LinearTopSpace
for a being Point of X holds transl (a,X) is one-to-one
proof
let X be LinearTopSpace; ::_thesis: for a being Point of X holds transl (a,X) is one-to-one
let a be Point of X; ::_thesis: transl (a,X) is one-to-one
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_the_carrier_of_X_&_x2_in_the_carrier_of_X_&_(transl_(a,X))_._x1_=_(transl_(a,X))_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in the carrier of X & x2 in the carrier of X & (transl (a,X)) . x1 = (transl (a,X)) . x2 implies x1 = x2 )
assume that
A1: ( x1 in the carrier of X & x2 in the carrier of X ) and
A2: (transl (a,X)) . x1 = (transl (a,X)) . x2 ; ::_thesis: x1 = 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; ::_thesis: verum
end;
hence  transl (a,X) is one-to-one by FUNCT_2:19; ::_thesis: verum
end;

theorem Th35: :: RLTOPSP1:35
for X being LinearTopSpace
for a being Point of X holds (transl (a,X)) " = transl ((- a),X)
proof
let X be LinearTopSpace; ::_thesis: for a being Point of X holds (transl (a,X)) " = transl ((- a),X)
let a be Point of X; ::_thesis: (transl (a,X)) " = transl ((- a),X)
A1: rng (transl (a,X)) = [#] X by Th34;
now__::_thesis:_for_x_being_Point_of_X_holds_((transl_(a,X))_")_._x_=_(transl_((-_a),X))_._x
let x be Point of X; ::_thesis: ((transl (a,X)) ") . x = (transl ((- a),X)) . x
consider u being set  such that
A2: u in dom (transl (a,X)) and
A3: x = (transl (a,X)) . u by A1, FUNCT_1:def_3;
reconsider u = u as Point of X by A2;
A4: x = a + u by A3, Def10;
 ( transl (a,X) is onto & transl (a,X) is one-to-one ) by A1, Lm8, FUNCT_2:def_3;
hence ((transl (a,X)) ") . x = ((transl (a,X)) ") . x by TOPS_2:def_4
.= u by A3, Lm8, FUNCT_2:26
.= (0. X) + u by RLVECT_1:4
.= ((- a) + a) + u by RLVECT_1:5
.= (- a) + x by A4, RLVECT_1:def_3
.= (transl ((- a),X)) . x by Def10 ;
::_thesis: verum
end;
hence  (transl (a,X)) " = transl ((- a),X) by FUNCT_2:63; ::_thesis: verum
end;

Lm9:  for X being LinearTopSpace
for a being Point of X holds transl (a,X) is continuous
proof
let X be LinearTopSpace; ::_thesis: for a being Point of X holds transl (a,X) is continuous
let a be Point of X; ::_thesis: transl (a,X) is continuous
A1: now__::_thesis:_for_P_being_Subset_of_X_st_P_is_open_holds_
(transl_(a,X))_"_P_is_open
reconsider X9 = X as TopStruct ;
let P be Subset of X; ::_thesis: ( P is open implies (transl (a,X)) " P is open )
defpred S1[ Subset of X9] means  ex D being Subset of X st
( D = $1 & D is open & a + D c= P );
consider F being Subset-Family of X9 such that
A2: for A being Subset of X9 holds
( A in F iff S1[A] ) from SUBSET_1:sch_3();
reconsider F = F as Subset-Family of X ;
assume A3: P is open ; ::_thesis: (transl (a,X)) " P is open
A4: union F = (transl (a,X)) " P
proof
thus  union F c= (transl (a,X)) " P :: according to XBOOLE_0:def_10 ::_thesis: (transl (a,X)) " P c= union F
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union F or x in (transl (a,X)) " P )
assume  x in union F ; ::_thesis: x in (transl (a,X)) " P
then consider A being set  such that
A5: x in A and
A6: A in F by TARSKI:def_4;
reconsider x = x as Point of X by A5, A6;
A7: (transl (a,X)) . x = a + x by Def10;
consider D being 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 is Point of X : u in D  }  by RUSUB_4:def_8;
then  a + x in a + D by A5, A8;
hence  x in (transl (a,X)) " P by A9, A7, FUNCT_2:38; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (transl (a,X)) " P or x in union F )
assume A10: x in (transl (a,X)) " P ; ::_thesis: x in union F
then reconsider x = 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 being 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, XBOOLE_1:1;
then  D in F by A2, A11;
hence  x in union F by A13, TARSKI:def_4; ::_thesis: verum
end;
 F is open
proof
let A be Subset of X; :: according to TOPS_2:def_1 ::_thesis: ( not A in F or A is open )
assume  A in F ; ::_thesis: A is open
then  ex D being Subset of X st
( D = A & D is open & a + D c= P ) by A2;
hence  A is open ; ::_thesis: verum
end;
hence  (transl (a,X)) " P is open by A4, TOPS_2:19; ::_thesis: verum
end;
 [#] X <> {} ;
hence  transl (a,X) is continuous by A1, TOPS_2:43; ::_thesis: verum
end;

registration
let X be LinearTopSpace;
let a be Point of X;
cluster transl (a,X) ->  being_homeomorphism ;
coherence
 transl (a,X) is being_homeomorphism
proof
thus  dom (transl (a,X)) = [#] X by FUNCT_2:def_1; :: according to TOPS_2:def_5 ::_thesis: ( rng (transl (a,X)) = [#] X & transl (a,X) is one-to-one & transl (a,X) is continuous & (transl (a,X)) " is continuous )
thus  rng (transl (a,X)) = [#] X by Th34; ::_thesis: ( transl (a,X) is one-to-one & transl (a,X) is continuous & (transl (a,X)) " is continuous )
thus  transl (a,X) is one-to-one by Lm8; ::_thesis: ( transl (a,X) is continuous & (transl (a,X)) " is continuous )
thus  transl (a,X) is continuous by Lm9; ::_thesis: (transl (a,X)) " is continuous
 (transl (a,X)) " = transl ((- a),X) by Th35;
hence  (transl (a,X)) " is continuous by Lm9; ::_thesis: verum
end;
end;

Lm10:  for X being LinearTopSpace
for E being Subset of X
for x being Point of X st E is open holds
x + E is open
proof
let X be LinearTopSpace; ::_thesis: for E being Subset of X
for x being Point of X st E is open holds
x + E is open
let E be Subset of X; ::_thesis: for x being Point of X st E is open holds
x + E is open
let x be Point of X; ::_thesis: ( E is open implies x + E is open )
assume A1: E is open ; ::_thesis: x + E is open
 (transl (x,X)) .: E = x + E by Th33;
hence  x + E is open by A1, TOPGRP_1:25; ::_thesis: verum
end;

registration
let X be LinearTopSpace;
let E be open Subset of X;
let x be Point of X;
clusterx + E ->  open ;
coherence
 x + E is open by Lm10;
end;

Lm11:  for X being LinearTopSpace
for E being open Subset of X
for K being Subset of X holds K + E is open
proof
let X be LinearTopSpace; ::_thesis: for E being open Subset of X
for K being Subset of X holds K + E is open
let E be open Subset of X; ::_thesis: for K being Subset of X holds K + E is open
let K be Subset of X; ::_thesis: K + E is open
reconsider F =  {  (a + E) where a is Point of X : a in K  }  as Subset-Family of X by Lm2;
A1: F is open
proof
let P be Subset of X; :: according to TOPS_2:def_1 ::_thesis: ( not P in F or P is open )
assume  P in F ; ::_thesis: P is open
then  ex a being Point of X st
( P = a + E & a in K ) ;
hence  P is open ; ::_thesis: verum
end;
 K + E = union F by Th4;
hence  K + E is open by A1, TOPS_2:19; ::_thesis: verum
end;

registration
let X be LinearTopSpace;
let E be open Subset of X;
let K be Subset of X;
clusterK + E ->  open ;
coherence
 K + E is open by Lm11;
end;

Lm12:  for X being LinearTopSpace
for D being closed Subset of X
for x being Point of X holds x + D is closed
proof
let X be LinearTopSpace; ::_thesis: for D being closed Subset of X
for x being Point of X holds x + D is closed
let D be closed Subset of X; ::_thesis: for x being Point of X holds x + D is closed
let x be Point of X; ::_thesis: x + D is closed
 (transl (x,X)) .: D = x + D by Th33;
hence  x + D is closed by TOPS_2:58; ::_thesis: verum
end;

registration
let X be LinearTopSpace;
let D be closed Subset of X;
let x be Point of X;
clusterx + D ->  closed ;
coherence
 x + D is closed by Lm12;
end;

theorem Th36: :: RLTOPSP1:36
for X being LinearTopSpace
for V1, V2, V being Subset of X st V1 + V2 c= V holds
(Int V1) + (Int V2) c= Int V
proof
let X be LinearTopSpace; ::_thesis: for V1, V2, V being Subset of X st V1 + V2 c= V holds
(Int V1) + (Int V2) c= Int V
let V1, V2, V be Subset of X; ::_thesis: ( V1 + V2 c= V implies (Int V1) + (Int V2) c= Int V )
assume A1: V1 + V2 c= V ; ::_thesis: (Int V1) + (Int V2) c= Int 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, XBOOLE_1:1;
hence  (Int V1) + (Int V2) c= Int V by TOPS_1:24; ::_thesis: verum
end;

theorem Th37: :: RLTOPSP1:37
for X being LinearTopSpace
for x being Point of X
for V being Subset of X holds x + (Int V) = Int (x + V)
proof
let X be LinearTopSpace; ::_thesis: for x being Point of X
for V being Subset of X holds x + (Int V) = Int (x + V)
let x be Point of X; ::_thesis: for V being Subset of X holds x + (Int V) = Int (x + V)
let V be Subset of X; ::_thesis: x + (Int V) = Int (x + V)
 x + (Int V) c= x + V by Th8, TOPS_1:16;
hence  x + (Int V) c= Int (x + V) by TOPS_1:24; :: according to XBOOLE_0:def_10 ::_thesis: Int (x + V) c= x + (Int V)
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in Int (x + V) or v in x + (Int V) )
assume A1: v in Int (x + V) ; ::_thesis: v in x + (Int V)
then reconsider v = v as Point of X ;
consider Q being 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 is 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  v in x + (Int V) by RLVECT_1:4; ::_thesis: verum
end;

theorem :: RLTOPSP1:38
for X being LinearTopSpace
for x being Point of X
for V being Subset of X holds x + (Cl V) = Cl (x + V)
proof
let X be LinearTopSpace; ::_thesis: for x being Point of X
for V being Subset of X holds x + (Cl V) = Cl (x + V)
let x be Point of X; ::_thesis: for V being Subset of X holds x + (Cl V) = Cl (x + V)
let V be Subset of X; ::_thesis: x + (Cl V) = Cl (x + V)
thus  x + (Cl V) c= Cl (x + V) :: according to XBOOLE_0:def_10 ::_thesis: Cl (x + V) c= x + (Cl V)
proof
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in x + (Cl V) or v in Cl (x + V) )
assume A1: v in x + (Cl V) ; ::_thesis: v in Cl (x + V)
then reconsider v = v as Point of X ;
now__::_thesis:_for_G_being_Subset_of_X_st_G_is_open_&_v_in_G_holds_
x_+_V_meets_G
A2: x + (Cl V) =  {  (x + u) where u is Point of X : u in Cl V  }  by RUSUB_4:def_8;
A3: x + V =  {  (x + u) where u is Point of X : u in V  }  by RUSUB_4:def_8;
let G be Subset of X; ::_thesis: ( G is open & v in G implies x + V meets G )
assume that
A4: G is open and
A5: v in G ; ::_thesis: x + V meets G
A6: (- x) + G =  {  ((- x) + u) where u is Point of X : u in G  }  by RUSUB_4:def_8;
then A7: (- x) + v in (- x) + G by A5;
consider u being 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 by RLVECT_1:4 ;
then  V meets (- x) + G by A4, A9, A7, PRE_TOPC:24;
then consider z being set  such that
A10: z in V and
A11: z in (- x) + G by XBOOLE_0:3;
reconsider z = z as Point of X by A10;
consider w being 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 by RLVECT_1:4 ;
hence  x + V meets G by A13, A14, XBOOLE_0:3; ::_thesis: verum
end;
hence  v in Cl (x + V) by PRE_TOPC:24; ::_thesis: verum
end;
 x + V c= x + (Cl V) by Th8, PRE_TOPC:18;
hence  Cl (x + V) c= x + (Cl V) by TOPS_1:5; ::_thesis: verum
end;

theorem :: RLTOPSP1:39
for X being LinearTopSpace
for x, v being Point of X
for V being a_neighborhood of x holds v + V is a_neighborhood of v + x
proof
let X be LinearTopSpace; ::_thesis: for x, v being Point of X
for V being a_neighborhood of x holds v + V is a_neighborhood of v + x
let x, v be Point of X; ::_thesis: for V being a_neighborhood of x holds v + V is a_neighborhood of v + x
let V be a_neighborhood of x; ::_thesis: v + V is a_neighborhood of v + x
 ( v + (Int V) =  {  (v + u) where u is 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  v + V is a_neighborhood of v + x by A1, CONNSP_2:def_1; ::_thesis: verum
end;

theorem :: RLTOPSP1:40
for X being LinearTopSpace
for x being Point of X
for V being a_neighborhood of x holds (- x) + V is a_neighborhood of 0. X
proof
let X be LinearTopSpace; ::_thesis: for x being Point of X
for V being a_neighborhood of x holds (- x) + V is a_neighborhood of 0. X
let x be Point of X; ::_thesis: for V being a_neighborhood of x holds (- x) + V is a_neighborhood of 0. X
let V be a_neighborhood of x; ::_thesis: (- x) + V is a_neighborhood of 0. X
 ( (- x) + (Int V) =  {  ((- x) + v) where v is 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  (- x) + V is a_neighborhood of 0. X by A1, CONNSP_2:def_1; ::_thesis: verum
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 ;
attrX is locally-convex  means :Def11: :: RLTOPSP1:def 11
 ex P being local_base of X st P is convex-membered ;
end;

:: deftheorem Def11 defines locally-convex RLTOPSP1:def_11_:_
 for X being non empty RLTopStruct holds
( X is locally-convex iff ex P being local_base of X st P is convex-membered );

definition
let X be LinearTopSpace;
let E be Subset of X;
attrE is bounded  means :Def12: :: RLTOPSP1:def 12
 for V being a_neighborhood of 0. X ex s being Real st
( s > 0 & ( for t being Real st t > s holds
E c= t * V ) );
end;

:: deftheorem Def12 defines bounded RLTOPSP1:def_12_:_
 for X being LinearTopSpace
for E being Subset of X holds
( E is bounded iff for V being a_neighborhood of 0. X ex s being Real st
( s > 0 & ( for t being Real st t > s holds
E c= t * V ) ) );

registration
let X be LinearTopSpace;
cluster empty  ->  bounded for Element of bool the carrier of X;
coherence
 for b1 being Subset of X st b1 is empty holds
b1 is bounded
proof
let S be Subset of X; ::_thesis: ( S is empty implies S is bounded )
assume  S is empty ; ::_thesis: S is bounded
then A1: S = {} X ;
let V be a_neighborhood of 0. X; :: according to RLTOPSP1:def_12 ::_thesis: ex s being Real st
( s > 0 & ( for t being Real st t > s holds
S c= t * V ) )
take  1 ; ::_thesis: ( 1 > 0 & ( for t being Real st t > 1 holds
S c= t * V ) )
thus  ( 1 > 0 & ( for t being Real st t > 1 holds
S c= t * V ) ) by A1, XBOOLE_1:2; ::_thesis: verum
end;
end;

registration
let X be LinearTopSpace;
cluster bounded for Element of bool the carrier of X;
existence
 ex b1 being Subset of X st b1 is bounded
proof
take  {} X ; ::_thesis: {} X is bounded
thus  {} X is bounded ; ::_thesis: verum
end;
end;

theorem Th41: :: RLTOPSP1:41
for X being LinearTopSpace
for V1, V2 being bounded Subset of X holds V1 \/ V2 is bounded
proof
let X be LinearTopSpace; ::_thesis: for V1, V2 being bounded Subset of X holds V1 \/ V2 is bounded
let V1, V2 be bounded Subset of X; ::_thesis: V1 \/ V2 is bounded
thus  V1 \/ V2 is bounded ::_thesis: verum
proof
let V be a_neighborhood of 0. X; :: according to RLTOPSP1:def_12 ::_thesis: ex s being Real st
( s > 0 & ( for t being Real st t > s holds
V1 \/ V2 c= t * V ) )
consider s being Real such that
A1: s > 0 and
A2: for t being Real st t > s holds
V1 c= t * V by Def12;
consider r being Real such that
A3: r > 0 and
A4: for t being Real st t > r holds
V2 c= t * V by Def12;
percases ( r <= s or r > s ) ;
supposeA5: r <= s ; ::_thesis: ex s being Real st
( s > 0 & ( for t being Real st t > s holds
V1 \/ V2 c= t * V ) )
take  s ; ::_thesis: ( s > 0 & ( for t being Real st t > s holds
V1 \/ V2 c= t * V ) )
thus  s > 0 by A1; ::_thesis: for t being Real st t > s holds
V1 \/ V2 c= t * V
let t be Real; ::_thesis: ( t > s implies V1 \/ V2 c= t * V )
assume A6: t > s ; ::_thesis: V1 \/ V2 c= t * V
 t > r by A5, A6, XXREAL_0:2;
then A7: V2 c= t * V by A4;
 V1 c= t * V by A2, A6;
hence  V1 \/ V2 c= t * V by A7, XBOOLE_1:8; ::_thesis: verum
end;
supposeA8: r > s ; ::_thesis: ex s being Real st
( s > 0 & ( for t being Real st t > s holds
V1 \/ V2 c= t * V ) )
take  r ; ::_thesis: ( r > 0 & ( for t being Real st t > r holds
V1 \/ V2 c= t * V ) )
thus  r > 0 by A3; ::_thesis: for t being Real st t > r holds
V1 \/ V2 c= t * V
let t be Real; ::_thesis: ( t > r implies V1 \/ V2 c= t * V )
assume A9: t > r ; ::_thesis: V1 \/ V2 c= t * V
 t > s by A8, A9, XXREAL_0:2;
then A10: V1 c= t * V by A2;
 V2 c= t * V by A4, A9;
hence  V1 \/ V2 c= t * V by A10, XBOOLE_1:8; ::_thesis: verum
end;
end;
end;
end;

theorem :: RLTOPSP1:42
for X being LinearTopSpace
for P being bounded Subset of X
for Q being Subset of X st Q c= P holds
Q is bounded
proof
let X be LinearTopSpace; ::_thesis: for P being bounded Subset of X
for Q being Subset of X st Q c= P holds
Q is bounded
let P be bounded Subset of X; ::_thesis: for Q being Subset of X st Q c= P holds
Q is bounded
let Q be Subset of X; ::_thesis: ( Q c= P implies Q is bounded )
assume A1: Q c= P ; ::_thesis: Q is bounded
let V be a_neighborhood of 0. X; :: according to RLTOPSP1:def_12 ::_thesis: ex s being Real st
( s > 0 & ( for t being Real st t > s holds
Q c= t * V ) )
consider s being Real such that
A2: s > 0 and
A3: for t being Real st t > s holds
P c= t * V by Def12;
take  s ; ::_thesis: ( s > 0 & ( for t being Real st t > s holds
Q c= t * V ) )
thus  s > 0 by A2; ::_thesis: for t being Real st t > s holds
Q c= t * V
let t be Real; ::_thesis: ( t > s implies Q c= t * V )
assume  t > s ; ::_thesis: Q c= t * V
then  P c= t * V by A3;
hence  Q c= t * V by A1, XBOOLE_1:1; ::_thesis: verum
end;

theorem :: RLTOPSP1:43
for X being LinearTopSpace
for F being Subset-Family of X st F is finite & F =  {  P where P is bounded Subset of X : verum  }  holds
union F is bounded
proof
let X be LinearTopSpace; ::_thesis: for F being Subset-Family of X st F is finite & F =  {  P where P is bounded Subset of X : verum  }  holds
union F is bounded
let F be Subset-Family of X; ::_thesis: ( F is finite & F =  {  P where P is bounded Subset of X : verum  }  implies union F is bounded )
assume that
A1: F is finite and
A2: F =  {  P where P is bounded Subset of X : verum  }  ; ::_thesis: union F is bounded
defpred S1[ set ] means  ex A being Subset of X st
( A = union $1 & A is bounded );
A3: now__::_thesis:_for_P_being_Subset_of_X_st_P_in_F_holds_
P_is_bounded
let P be Subset of X; ::_thesis: ( P in F implies P is bounded )
assume  P in F ; ::_thesis: P is bounded
then  ex A being bounded Subset of X st P = A by A2;
hence  P is bounded ; ::_thesis: verum
end;
A4: for x, B being set st x in F & B c= F & S1[B] holds
S1[B \/ {x}]
proof
let x, B be set ; ::_thesis: ( x in F & B c= F & S1[B] implies S1[B \/ {x}] )
assume that
A5: x in F and
 B c= F and
A6: S1[B] ; ::_thesis: S1[B \/ {x}]
consider A being Subset of X such that
A7: ( A = union B & A is bounded ) by A6;
reconsider x = 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 being Subset of X st
( Y = union (B \/ {x}) & Y is bounded )
proof
take  A \/ x ; ::_thesis: ( A \/ x = union (B \/ {x}) & A \/ x is bounded )
thus  ( A \/ x = union (B \/ {x}) & A \/ x is bounded ) by A7, A8, A9, Th41; ::_thesis: verum
end;
hence  S1[B \/ {x}] ; ::_thesis: verum
end;
 {} X = union {} by ZFMISC_1:2;
then A10: S1[ {} ] ;
 S1[F] from FINSET_1:sch_2(A1, A10, A4);
hence  union F is bounded ; ::_thesis: verum
end;

theorem Th44: :: RLTOPSP1:44
for X being LinearTopSpace
for P being Subset-Family of X st P =  {  U where U is a_neighborhood of 0. X : verum  }  holds
P is local_base of X
proof
let X be LinearTopSpace; ::_thesis: for P being Subset-Family of X st P =  {  U where U is a_neighborhood of 0. X : verum  }  holds
P is local_base of X
let P be Subset-Family of X; ::_thesis: ( P =  {  U where U is a_neighborhood of 0. X : verum  }  implies P is local_base of X )
assume A1: P =  {  U where U is a_neighborhood of 0. X : verum  }  ; ::_thesis: P is local_base of X
let A be a_neighborhood of 0. X; :: according to YELLOW13:def_2 ::_thesis: ex b1 being a_neighborhood of 0. X st
( b1 in P & b1 c= A )
take  A ; ::_thesis: ( A in P & A c= A )
thus  ( A in P & A c= A ) by A1; ::_thesis: verum
end;

theorem :: RLTOPSP1:45
for X being LinearTopSpace
for O being local_base of X
for P being Subset-Family of X st P =  {  (a + U) where a is Point of X, U is Subset of X : U in O  }  holds
P is basis of X
proof
let X be LinearTopSpace; ::_thesis: for O being local_base of X
for P being Subset-Family of X st P =  {  (a + U) where a is Point of X, U is Subset of X : U in O  }  holds
P is basis of X
let O be basis of 0. X; ::_thesis: for P being Subset-Family of X st P =  {  (a + U) where a is Point of X, U is Subset of X : U in O  }  holds
P is basis of X
let P be Subset-Family of X; ::_thesis: ( P =  {  (a + U) where a is Point of X, U is Subset of X : U in O  }  implies P is basis of X )
assume A1: P =  {  (a + U) where a is Point of X, U is Subset of X : U in O  }  ; ::_thesis: P is basis of X
let p be Point of X; :: according to YELLOW13:def_4 ::_thesis: P is basis of p
let A be a_neighborhood of p; :: according to YELLOW13:def_2 ::_thesis: ex b1 being a_neighborhood of p st
( b1 in P & b1 c= A )
 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 being 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; ::_thesis: ( U is a_neighborhood of p & U in P & U c= A )
 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) by RLVECT_1:4;
 p + (Int V) c= Int U by Th37;
hence  U is a_neighborhood of p by A4, CONNSP_2:def_1; ::_thesis: ( U in P & U c= A )
thus  U in P by A1, A2; ::_thesis: U c= A
 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  U c= A by XBOOLE_1:1; ::_thesis: verum
end;

definition
let X be non empty RLTopStruct ;
let r be Real;
func mlt (r,X) ->  Function of X,X means :Def13: :: RLTOPSP1:def 13
 for x being Point of X holds it . x = r * x;
existence
 ex b1 being Function of X,X st
for x being Point of X holds b1 . x = r * x
proof
deffunc H1( Point of X) ->  Element of the carrier of X = r * $1;
consider F being Function of the carrier of X, the carrier of X such that
A1: for x being Point of X holds F . x = H1(x) from FUNCT_2:sch_4();
reconsider F = F as Function of X,X ;
take  F ; ::_thesis: for x being Point of X holds F . x = r * x
thus  for x being Point of X holds F . x = r * x by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of X,X st ( for x being Point of X holds b1 . x = r * x ) & ( for x being Point of X holds b2 . x = r * x ) holds
b1 = b2
proof
let F, G be Function of X,X; ::_thesis: ( ( for x being Point of X holds F . x = r * x ) & ( for x being Point of X holds G . x = r * x ) implies F = G )
assume that
A2: for x being Point of X holds F . x = r * x and
A3: for x being Point of X holds G . x = r * x ; ::_thesis: F = G
now__::_thesis:_for_x_being_Point_of_X_holds_F_._x_=_G_._x
let x be Point of X; ::_thesis: F . x = G . x
thus F . x = r * x by A2
.= G . x by A3 ; ::_thesis: verum
end;
hence  F = G by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def13 defines mlt RLTOPSP1:def_13_:_
 for X being non empty RLTopStruct
for r being Real
for b3 being Function of X,X holds
( b3 = mlt (r,X) iff for x being Point of X holds b3 . x = r * x );

theorem Th46: :: RLTOPSP1:46
for X being non empty RLTopStruct
for V being Subset of X
for r being non zero Real holds (mlt (r,X)) .: V = r * V
proof
let X be non empty RLTopStruct ; ::_thesis: for V being Subset of X
for r being non zero Real holds (mlt (r,X)) .: V = r * V
let V be Subset of X; ::_thesis: for r being non zero Real holds (mlt (r,X)) .: V = r * V
let r be non zero Real; ::_thesis: (mlt (r,X)) .: V = r * V
thus  (mlt (r,X)) .: V c= r * V :: according to XBOOLE_0:def_10 ::_thesis: r * V c= (mlt (r,X)) .: V
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (mlt (r,X)) .: V or y in r * V )
assume  y in (mlt (r,X)) .: V ; ::_thesis: y in r * V
then consider c being 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  y in r * V by A1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in r * V or x in (mlt (r,X)) .: V )
assume  x in r * V ; ::_thesis: x in (mlt (r,X)) .: V
then consider u being Point of X such that
A3: x = r * u and
A4: u in V ;
 x = (mlt (r,X)) . u by A3, Def13;
hence  x in (mlt (r,X)) .: V by A4, FUNCT_2:35; ::_thesis: verum
end;

theorem Th47: :: RLTOPSP1:47
for X being LinearTopSpace
for r being non zero Real holds rng (mlt (r,X)) = [#] X
proof
let X be LinearTopSpace; ::_thesis: for r being non zero Real holds rng (mlt (r,X)) = [#] X
let r be non zero Real; ::_thesis: rng (mlt (r,X)) = [#] X
thus  rng (mlt (r,X)) c= [#] X ; :: according to XBOOLE_0:def_10 ::_thesis: [#] X c= rng (mlt (r,X))
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in [#] X or y in rng (mlt (r,X)) )
assume  y in [#] X ; ::_thesis: y in rng (mlt (r,X))
then reconsider y = 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  y in rng (mlt (r,X)) by FUNCT_2:4; ::_thesis: verum
end;

Lm13:  for X being LinearTopSpace
for r being non zero Real holds mlt (r,X) is one-to-one
proof
let X be LinearTopSpace; ::_thesis: for r being non zero Real holds mlt (r,X) is one-to-one
let r be non zero Real; ::_thesis: mlt (r,X) is one-to-one
now__::_thesis:_for_x1,_x2_being_set_st_x1_in_the_carrier_of_X_&_x2_in_the_carrier_of_X_&_(mlt_(r,X))_._x1_=_(mlt_(r,X))_._x2_holds_
x1_=_x2
let x1, x2 be set ; ::_thesis: ( x1 in the carrier of X & x2 in the carrier of X & (mlt (r,X)) . x1 = (mlt (r,X)) . x2 implies x1 = x2 )
assume that
A1: ( x1 in the carrier of X & x2 in the carrier of X ) and
A2: (mlt (r,X)) . x1 = (mlt (r,X)) . x2 ; ::_thesis: x1 = 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; ::_thesis: verum
end;
hence  mlt (r,X) is one-to-one by FUNCT_2:19; ::_thesis: verum
end;

theorem Th48: :: RLTOPSP1:48
for X being LinearTopSpace
for r being non zero Real holds (mlt (r,X)) " = mlt ((r "),X)
proof
let X be LinearTopSpace; ::_thesis: for r being non zero Real holds (mlt (r,X)) " = mlt ((r "),X)
let r be non zero Real; ::_thesis: (mlt (r,X)) " = mlt ((r "),X)
A1: rng (mlt (r,X)) = [#] X by Th47;
now__::_thesis:_for_x_being_Point_of_X_holds_((mlt_(r,X))_")_._x_=_(mlt_((r_"),X))_._x
let x be Point of X; ::_thesis: ((mlt (r,X)) ") . x = (mlt ((r "),X)) . x
consider u being set  such that
A2: u in dom (mlt (r,X)) and
A3: x = (mlt (r,X)) . u by A1, FUNCT_1:def_3;
reconsider u = u as Point of X by A2;
A4: x = r * u by A3, Def13;
 ( mlt (r,X) is onto & mlt (r,X) is one-to-one ) by A1, Lm13, FUNCT_2:def_3;
hence ((mlt (r,X)) ") . x = ((mlt (r,X)) ") . 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 ;
::_thesis: verum
end;
hence  (mlt (r,X)) " = mlt ((r "),X) by FUNCT_2:63; ::_thesis: verum
end;

Lm14:  for X being LinearTopSpace
for r being non zero Real holds mlt (r,X) is continuous
proof
let X be LinearTopSpace; ::_thesis: for r being non zero Real holds mlt (r,X) is continuous
let r be non zero Real; ::_thesis: mlt (r,X) is continuous
A1: now__::_thesis:_for_P_being_Subset_of_X_st_P_is_open_holds_
(mlt_(r,X))_"_P_is_open
let P be Subset of X; ::_thesis: ( P is open implies (mlt (r,X)) " P is open )
defpred S1[ Subset of X] means ( $1 is open & r * $1 c= P );
consider F being Subset-Family of X such that
A2: for A being Subset of X holds
( A in F iff S1[A] ) from SUBSET_1:sch_3();
reconsider F = F as Subset-Family of X ;
assume A3: P is open ; ::_thesis: (mlt (r,X)) " P is open
A4: union F = (mlt (r,X)) " P
proof
thus  union F c= (mlt (r,X)) " P :: according to XBOOLE_0:def_10 ::_thesis: (mlt (r,X)) " P c= union F
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union F or x in (mlt (r,X)) " P )
assume  x in union F ; ::_thesis: x in (mlt (r,X)) " P
then consider A being set  such that
A5: x in A and
A6: A in F by TARSKI:def_4;
reconsider A = A as Subset of X by A6;
 A is Subset of X ;
then reconsider x = 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  x in (mlt (r,X)) " P by A7, FUNCT_2:38; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (mlt (r,X)) " P or x in union F )
assume A8: x in (mlt (r,X)) " P ; ::_thesis: x in union F
then reconsider x = 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 being positive Real, W being Subset of X such that
A9: W is open and
A10: x in W and
A11: for s being Real st abs (s - r) < e holds
s * W c= P by A3, Def9;
 abs (r - r) < e by ABSVALUE:2;
then  r * W c= P by A11;
then  W in F by A2, A9;
hence  x in union F by A10, TARSKI:def_4; ::_thesis: verum
end;
 F is open
proof
let A be Subset of X; :: according to TOPS_2:def_1 ::_thesis: ( not A in F or A is open )
assume  A in F ; ::_thesis: A is open
hence  A is open by A2; ::_thesis: verum
end;
hence  (mlt (r,X)) " P is open by A4, TOPS_2:19; ::_thesis: verum
end;
 [#] X <> {} ;
hence  mlt (r,X) is continuous by A1, TOPS_2:43; ::_thesis: verum
end;

registration
let X be LinearTopSpace;
let r be non zero Real;
cluster mlt (r,X) ->  being_homeomorphism ;
coherence
 mlt (r,X) is being_homeomorphism
proof
thus  dom (mlt (r,X)) = [#] X by FUNCT_2:def_1; :: according to TOPS_2:def_5 ::_thesis: ( rng (mlt (r,X)) = [#] X & mlt (r,X) is one-to-one & mlt (r,X) is continuous & (mlt (r,X)) " is continuous )
thus  rng (mlt (r,X)) = [#] X by Th47; ::_thesis: ( mlt (r,X) is one-to-one & mlt (r,X) is continuous & (mlt (r,X)) " is continuous )
thus  mlt (r,X) is one-to-one by Lm13; ::_thesis: ( mlt (r,X) is continuous & (mlt (r,X)) " is continuous )
thus  mlt (r,X) is continuous by Lm14; ::_thesis: (mlt (r,X)) " is continuous
 (mlt (r,X)) " = mlt ((r "),X) by Th48;
hence  (mlt (r,X)) " is continuous by Lm14; ::_thesis: verum
end;
end;

theorem Th49: :: RLTOPSP1:49
for X being LinearTopSpace
for V being open Subset of X
for r being non zero Real holds r * V is open
proof
let X be LinearTopSpace; ::_thesis: for V being open Subset of X
for r being non zero Real holds r * V is open
let V be open Subset of X; ::_thesis: for r being non zero Real holds r * V is open
let r be non zero Real; ::_thesis: r * V is open
 (mlt (r,X)) .: V = r * V by Th46;
hence  r * V is open by TOPGRP_1:25; ::_thesis: verum
end;

theorem Th50: :: RLTOPSP1:50
for X being LinearTopSpace
for V being closed Subset of X
for r being non zero Real holds r * V is closed
proof
let X be LinearTopSpace; ::_thesis: for V being closed Subset of X
for r being non zero Real holds r * V is closed
let V be closed Subset of X; ::_thesis: for r being non zero Real holds r * V is closed
let r be non zero Real; ::_thesis: r * V is closed
 (mlt (r,X)) .: V = r * V by Th46;
hence  r * V is closed by TOPS_2:58; ::_thesis: verum
end;

theorem Th51: :: RLTOPSP1:51
for X being LinearTopSpace
for V being Subset of X
for r being non zero Real holds r * (Int V) = Int (r * V)
proof
let X be LinearTopSpace; ::_thesis: for V being Subset of X
for r being non zero Real holds r * (Int V) = Int (r * V)
let V be Subset of X; ::_thesis: for r being non zero Real holds r * (Int V) = Int (r * V)
let r be non zero Real; ::_thesis: r * (Int V) = Int (r * V)
 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; :: according to XBOOLE_0:def_10 ::_thesis: Int (r * V) c= r * (Int V)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Int (r * V) or x in r * (Int V) )
assume A1: x in Int (r * V) ; ::_thesis: x in r * (Int V)
then reconsider x = x as Point of X ;
consider Q being 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  x in r * (Int V) by RLVECT_1:def_8; ::_thesis: verum
end;

theorem Th52: :: RLTOPSP1:52
for X being LinearTopSpace
for A being Subset of X
for r being non zero Real holds r * (Cl A) = Cl (r * A)
proof
let X be LinearTopSpace; ::_thesis: for A being Subset of X
for r being non zero Real holds r * (Cl A) = Cl (r * A)
let A be Subset of X; ::_thesis: for r being non zero Real holds r * (Cl A) = Cl (r * A)
let r be non zero Real; ::_thesis: r * (Cl A) = Cl (r * A)
thus  r * (Cl A) c= Cl (r * A) :: according to XBOOLE_0:def_10 ::_thesis: Cl (r * A) c= r * (Cl A)
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in r * (Cl A) or z in Cl (r * A) )
assume A1: z in r * (Cl A) ; ::_thesis: z in Cl (r * A)
then reconsider z = z as Point of X ;
now__::_thesis:_for_G_being_Subset_of_X_st_G_is_open_&_z_in_G_holds_
r_*_A_meets_G
let G be Subset of X; ::_thesis: ( G is open & z in G implies r * A meets G )
assume  ( G is open & z in G ) ; ::_thesis: r * A meets G
then A2: ( (r ") * z in (r ") * G & (r ") * G is open ) by Th49;
consider v being 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 being set  such that
A5: x in A and
A6: x in (r ") * G by XBOOLE_0:3;
reconsider x = x as Point of X by A5;
consider u being 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; ::_thesis: verum
end;
hence  z in Cl (r * A) by PRE_TOPC:24; ::_thesis: verum
end;
 r * A c= r * (Cl A) by CONVEX1:39, PRE_TOPC:18;
hence  Cl (r * A) c= r * (Cl A) by Th50, TOPS_1:5; ::_thesis: verum
end;

theorem :: RLTOPSP1:53
for X being LinearTopSpace
for A being Subset of X st X is T_1 holds
0 * (Cl A) = Cl (0 * A)
proof
let X be LinearTopSpace; ::_thesis: for A being Subset of X st X is T_1 holds
0 * (Cl A) = Cl (0 * A)
let A be Subset of X; ::_thesis: ( X is T_1 implies 0 * (Cl A) = Cl (0 * A) )
assume A1: X is T_1 ; ::_thesis: 0 * (Cl A) = Cl (0 * A)
percases ( A is empty or not A is empty ) ;
supposeA2: A is empty ; ::_thesis: 0 * (Cl A) = Cl (0 * A)
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 ;
::_thesis: verum
end;
supposeA4: not A is empty ; ::_thesis: 0 * (Cl A) = Cl (0 * A)
then  not Cl A is 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 ;
::_thesis: verum
end;
end;
end;

theorem Th54: :: RLTOPSP1:54
for X being LinearTopSpace
for x being Point of X
for V being a_neighborhood of x
for r being non zero Real holds r * V is a_neighborhood of r * x
proof
let X be LinearTopSpace; ::_thesis: for x being Point of X
for V being a_neighborhood of x
for r being non zero Real holds r * V is a_neighborhood of r * x
let x be Point of X; ::_thesis: for V being a_neighborhood of x
for r being non zero Real holds r * V is a_neighborhood of r * x
let V be a_neighborhood of x; ::_thesis: for r being non zero Real holds r * V is a_neighborhood of r * x
let r be non zero Real; ::_thesis: r * V is a_neighborhood of r * x
 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; :: according to CONNSP_2:def_1 ::_thesis: verum
end;

theorem Th55: :: RLTOPSP1:55
for X being LinearTopSpace
for V being a_neighborhood of 0. X
for r being non zero Real holds r * V is a_neighborhood of 0. X
proof
let X be LinearTopSpace; ::_thesis: for V being a_neighborhood of 0. X
for r being non zero Real holds r * V is a_neighborhood of 0. X
let V be a_neighborhood of 0. X; ::_thesis: for r being non zero Real holds r * V is a_neighborhood of 0. X
let r be non zero Real; ::_thesis: r * V is a_neighborhood of 0. X
 r * V is a_neighborhood of r * (0. X) by Th54;
hence  r * V is a_neighborhood of 0. X by RLVECT_1:10; ::_thesis: verum
end;

Lm15:  for X being LinearTopSpace
for V being bounded Subset of X
for r being Real holds r * V is bounded
proof
let X be LinearTopSpace; ::_thesis: for V being bounded Subset of X
for r being Real holds r * V is bounded
let V be bounded Subset of X; ::_thesis: for r being Real holds r * V is bounded
let r be Real; ::_thesis: r * V is bounded
percases ( r = 0 or r <> 0 ) ;
supposeA1: r = 0 ; ::_thesis: r * V is bounded
percases ( V is empty or not V is empty ) ;
suppose V is empty ; ::_thesis: r * V is bounded
hence  r * V is bounded by CONVEX1:33; ::_thesis: verum
end;
supposeA2: not V is empty ; ::_thesis: r * V is bounded
let U be a_neighborhood of 0. X; :: according to RLTOPSP1:def_12 ::_thesis: ex s being Real st
( s > 0 & ( for t being Real st t > s holds
r * V c= t * U ) )
take s = 1; ::_thesis: ( s > 0 & ( for t being Real st t > s holds
r * V c= t * U ) )
thus  s > 0 ; ::_thesis: for t being Real st t > s holds
r * V c= t * U
let t be Real; ::_thesis: ( t > s implies r * V c= t * U )
assume  t > s ; ::_thesis: r * V c= t * U
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  r * V c= t * U by A3, ZFMISC_1:31; ::_thesis: verum
end;
end;
end;
supposeA4: r <> 0 ; ::_thesis: r * V is bounded
let U be a_neighborhood of 0. X; :: according to RLTOPSP1:def_12 ::_thesis: ex s being Real st
( s > 0 & ( for t being Real st t > s holds
r * V c= t * U ) )
 (1 / r) * U is a_neighborhood of 0. X by A4, Th55;
then consider s being Real such that
A5: s > 0 and
A6: for t being Real st t > s holds
V c= t * ((1 / r) * U) by Def12;
take  s ; ::_thesis: ( s > 0 & ( for t being Real st t > s holds
r * V c= t * U ) )
thus  s > 0 by A5; ::_thesis: for t being Real st t > s holds
r * V c= t * U
let t be Real; ::_thesis: ( t > s implies r * V c= t * U )
assume  t > s ; ::_thesis: r * V c= t * U
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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in r * V or x in t * U )
assume  x in r * V ; ::_thesis: x in t * U
hence  x in t * U by A7; ::_thesis: verum
end;
end;
end;

registration
let X be LinearTopSpace;
let V be bounded Subset of X;
let r be Real;
clusterr * V ->  bounded ;
coherence
 r * V is bounded by Lm15;
end;

theorem Th56: :: RLTOPSP1:56
for X being LinearTopSpace
for W being a_neighborhood of 0. X ex U being open a_neighborhood of 0. X st
( U is symmetric & U + U c= W )
proof
let X be LinearTopSpace; ::_thesis: for W being a_neighborhood of 0. X ex U being open a_neighborhood of 0. X st
( U is symmetric & U + U c= W )
let W be a_neighborhood of 0. X; ::_thesis: ex U being open a_neighborhood of 0. X st
( U is symmetric & U + U c= W )
 (0. X) + (0. X) = 0. X by RLVECT_1:4;
then consider V1, V2 being 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 (((Int V1) /\ (Int V2)) /\ ((- 1) * (Int V1))) /\ ((- 1) * (Int V2)) by A3, XBOOLE_0:def_4;
then  0. X in Int ((((Int V1) /\ (Int V2)) /\ ((- 1) * (Int V1))) /\ ((- 1) * (Int V2))) by A2, TOPS_1:23;
then reconsider U = (((Int V1) /\ (Int V2)) /\ ((- 1) * (Int V1))) /\ ((- 1) * (Int V2)) as open a_neighborhood of 0. X by A2, CONNSP_2:def_1;
take  U ; ::_thesis: ( U is symmetric & U + U c= W )
 ((- 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 ; :: according to RLTOPSP1:def_5 ::_thesis: U + U c= W
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in U + U or x in W )
assume  x in U + U ; ::_thesis: x in W
then  x in  {  (u + v) where u, v is Point of X : ( u in U & v in U )  }  by RUSUB_4:def_9;
then consider u, v being 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 is 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  x in W by A1, A7; ::_thesis: verum
end;

theorem Th57: :: RLTOPSP1:57
for X being LinearTopSpace
for K being compact Subset of X
for C being closed Subset of X st K misses C holds
ex V being a_neighborhood of 0. X st K + V misses C + V
proof
let X be LinearTopSpace; ::_thesis: for K being compact Subset of X
for C being closed Subset of X st K misses C holds
ex V being a_neighborhood of 0. X st K + V misses C + V
let K be compact Subset of X; ::_thesis: for C being closed Subset of X st K misses C holds
ex V being a_neighborhood of 0. X st K + V misses C + V
let C be closed Subset of X; ::_thesis: ( K misses C implies ex V being a_neighborhood of 0. X st K + V misses C + V )
assume A1: K misses C ; ::_thesis: ex V being a_neighborhood of 0. X st K + V misses C + V
percases ( K = {} or K <> {} ) ;
supposeA2: K = {} ; ::_thesis: ex V being a_neighborhood of 0. X st K + V misses C + V
take V = [#] X; ::_thesis: ( V is a_neighborhood of 0. X & K + V misses C + V )
thus  V is a_neighborhood of 0. X by TOPGRP_1:21; ::_thesis: K + V misses C + V
 K + V = {} by A2, CONVEX1:40;
hence  K + V misses C + V by XBOOLE_1:65; ::_thesis: verum
end;
supposeA3: K <> {} ; ::_thesis: ex V being a_neighborhood of 0. X st K + V misses C + V
set xV =  {  [x,Vx] where x is Point of X, Vx is open a_neighborhood of 0. X : ( x in K & Vx is symmetric & ((x + Vx) + Vx) + Vx misses C )  }  ;
A4: now__::_thesis:_for_x_being_Point_of_X_st_x_in_K_holds_
ex_Vx_being_open_a_neighborhood_of_0._X_st_
(_Vx_is_symmetric_&_((x_+_Vx)_+_Vx)_+_Vx_misses_C_)
let x be Point of X; ::_thesis: ( x in K implies ex Vx being open a_neighborhood of 0. X st
( Vx is symmetric & ((x + Vx) + Vx) + Vx misses C ) )
assume A5: x in K ; ::_thesis: ex Vx being open a_neighborhood of 0. X st
( Vx is symmetric & ((x + Vx) + Vx) + Vx misses C )
 ( (- x) + (C `) =  {  ((- x) + u) where u is 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 being open a_neighborhood of 0. X such that
 V9 is symmetric and
A6: V9 + V9 c= (- x) + (C `) by Th56;
consider Vx being open a_neighborhood of 0. X such that
A7: Vx is symmetric and
A8: Vx + Vx c= V9 by Th56;
take Vx = Vx; ::_thesis: ( Vx is symmetric & ((x + Vx) + Vx) + Vx misses C )
thus  Vx is symmetric by A7; ::_thesis: ((x + Vx) + Vx) + Vx misses C
 Vx c= V9
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Vx or z in V9 )
assume A9: z in Vx ; ::_thesis: z in V9
then reconsider z = 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 by RLVECT_1:4;
hence  z in V9 by A8; ::_thesis: verum
end;
then  Vx + (Vx + Vx) c= V9 + V9 by A8, Th11;
then  (Vx + Vx) + Vx c= (- x) + (C `) by A6, XBOOLE_1:1;
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; ::_thesis: verum
end;
A10: now__::_thesis:_ex_z_being_Element_of_[:_the_carrier_of_X,(bool_the_carrier_of_X):]_st_z_in__{__[x,Vx]_where_x_is_Point_of_X,_Vx_is_open_a_neighborhood_of_0._X_:_(_x_in_K_&_Vx_is_symmetric_&_((x_+_Vx)_+_Vx)_+_Vx_misses_C_)__}_
consider x being set  such that
A11: x in K by A3, XBOOLE_0:def_1;
reconsider x = x as Point of X by A11;
consider Vx being 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]; ::_thesis: z in  {  [x,Vx] where x is Point of X, Vx is open a_neighborhood of 0. X : ( x in K & Vx is symmetric & ((x + Vx) + Vx) + Vx misses C )  }
thus  z in  {  [x,Vx] where x is Point of X, Vx is open a_neighborhood of 0. X : ( x in K & Vx is symmetric & ((x + Vx) + Vx) + Vx misses C )  }  by A11, A12; ::_thesis: verum
end;
defpred S1[ set , set ] means  ex v1, v2 being Point of X ex V1, V2 being open a_neighborhood of 0. X st
( $1 = [v1,V1] & $2 = [v2,V2] & v1 + V1 = v2 + V2 );
A13: for x, y, z being set st S1[x,y] & S1[y,z] holds
S1[x,z]
proof
let x, y, z be set ; ::_thesis: ( S1[x,y] & S1[y,z] implies S1[x,z] )
given v1, v2 being Point of X, V1, V2 being open a_neighborhood of 0. X such that A14: x = [v1,V1] and
A15: y = [v2,V2] and
A16: v1 + V1 = v2 + V2 ; ::_thesis: ( not S1[y,z] or S1[x,z] )
given w1, w2 being Point of X, W1, W2 being open a_neighborhood of 0. X such that A17: y = [w1,W1] and
A18: ( z = [w2,W2] & w1 + W1 = w2 + W2 ) ; ::_thesis: S1[x,z]
take  v1 ; ::_thesis: ex v2 being Point of X ex V1, V2 being open a_neighborhood of 0. X st
( x = [v1,V1] & z = [v2,V2] & v1 + V1 = v2 + V2 )
take  w2 ; ::_thesis: ex V1, V2 being open a_neighborhood of 0. X st
( x = [v1,V1] & z = [w2,V2] & v1 + V1 = w2 + V2 )
take  V1 ; ::_thesis: ex V2 being open a_neighborhood of 0. X st
( x = [v1,V1] & z = [w2,V2] & v1 + V1 = w2 + V2 )
take  W2 ; ::_thesis: ( x = [v1,V1] & z = [w2,W2] & v1 + V1 = w2 + W2 )
 v2 = w1 by A15, A17, XTUPLE_0:1;
hence  ( x = [v1,V1] & z = [w2,W2] & v1 + V1 = w2 + W2 ) by A14, A15, A16, A17, A18, XTUPLE_0:1; ::_thesis: verum
end;
reconsider xV =  {  [x,Vx] where x is Point of X, Vx is open a_neighborhood of 0. X : ( x in K & Vx is symmetric & ((x + Vx) + Vx) + Vx misses C )  }  as non empty set by A10;
A19: for x being set st x in xV holds
S1[x,x]
proof
let x be set ; ::_thesis: ( x in xV implies S1[x,x] )
assume  x in xV ; ::_thesis: S1[x,x]
then  ex v being Point of X ex V being open a_neighborhood of 0. X st
( x = [v,V] & v in K & V is symmetric & ((v + V) + V) + V misses C ) ;
hence  S1[x,x] ; ::_thesis: verum
end;
A20: for x, y being set st S1[x,y] holds
S1[y,x] ;
consider eqR being Equivalence_Relation of xV such that
A21: for x, y being set holds
( [x,y] in eqR iff ( x in xV & y in xV & S1[x,y] ) ) from EQREL_1:sch_1(A19, A20, A13);
now__::_thesis:_for_X_being_set_st_X_in_Class_eqR_holds_
X_<>_{}
let X be set ; ::_thesis: ( X in Class eqR implies X <> {} )
assume  X in Class eqR ; ::_thesis: X <> {}
then  ex x being set st
( x in xV & X = Class (eqR,x) ) by EQREL_1:def_3;
hence  X <> {} by EQREL_1:20; ::_thesis: verum
end;
then consider g being Function such that
A22: dom g = Class eqR and
A23: for X being 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 is Point of X, Vx is open a_neighborhood of 0. X : [x,Vx] in rng g  }  ;
  {  (x + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : [x,Vx] in rng g  }  c= bool the carrier of X
proof
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in  {  (x + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : [x,Vx] in rng g  }  or A in bool the carrier of X )
assume  A in  {  (x + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : [x,Vx] in rng g  }  ; ::_thesis: A in bool the carrier of X
then  ex x being Point of X ex Vx being open a_neighborhood of 0. X st
( A = x + Vx & [x,Vx] in rng g ) ;
hence  A in bool the carrier of X ; ::_thesis: verum
end;
then reconsider F =  {  (x + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : [x,Vx] in rng g  }  as Subset-Family of X ;
A24: F is Cover of K
proof
let x be set ; :: according to TARSKI:def_3,SETFAM_1:def_11 ::_thesis: ( not x in K or x in union F )
assume A25: x in K ; ::_thesis: x in union F
then reconsider x = x as Point of X ;
consider Vx being 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 rng g by A22, FUNCT_1:def_3;
 x + (0. X) in x + Vx by Lm1, CONNSP_2:4;
then A29: x in x + Vx by RLVECT_1:4;
 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 being Point of X, V1, V2 being 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  x in union F by A29, TARSKI:def_4; ::_thesis: verum
end;
 F is open
proof
let P be Subset of X; :: according to TOPS_2:def_1 ::_thesis: ( not P in F or P is open )
assume  P in F ; ::_thesis: P is open
then  ex x being Point of X ex Vx being open a_neighborhood of 0. X st
( P = x + Vx & [x,Vx] in rng g ) ;
hence  P is open ; ::_thesis: verum
end;
then consider G being 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 is open a_neighborhood of 0. X : ex x being Point of X st
( x + Vx in G & [x,Vx] in rng g )  }  ;
  {  Vx where Vx is open a_neighborhood of 0. X : ex x being Point of X st
( x + Vx in G & [x,Vx] in rng g )  }  c= bool the carrier of X
proof
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in  {  Vx where Vx is open a_neighborhood of 0. X : ex x being Point of X st
( x + Vx in G & [x,Vx] in rng g )  }  or A in bool the carrier of X )
assume  A in  {  Vx where Vx is open a_neighborhood of 0. X : ex x being Point of X st
( x + Vx in G & [x,Vx] in rng g )  }  ; ::_thesis: A in bool the carrier of X
then  ex Vx being open a_neighborhood of 0. X st
( A = Vx & ex x being Point of X st
( x + Vx in G & [x,Vx] in rng g ) ) ;
hence  A in bool the carrier of X ; ::_thesis: verum
end;
then reconsider FVx =  {  Vx where Vx is open a_neighborhood of 0. X : ex x being Point of X st
( x + Vx in G & [x,Vx] in rng g )  }  as Subset-Family of X ;
defpred S2[ set , set ] means  ex x being Point of X ex Vx being open a_neighborhood of 0. X st
( $1 = x + Vx & x + Vx in G & [x,Vx] in rng g & $2 = Vx );
A36: for x being set st x in G holds
ex y being set st
( y in FVx & S2[x,y] )
proof
let x be set ; ::_thesis: ( x in G implies ex y being set st
( y in FVx & S2[x,y] ) )
assume A37: x in G ; ::_thesis: ex y being set st
( y in FVx & S2[x,y] )
then  x in F by A33;
then consider z being Point of X, Vz being open a_neighborhood of 0. X such that
A38: ( x = z + Vz & [z,Vz] in rng g ) ;
take  Vz ; ::_thesis: ( Vz in FVx & S2[x,Vz] )
thus  ( Vz in FVx & S2[x,Vz] ) by A37, A38; ::_thesis: verum
end;
consider f being Function of G,FVx such that
A39: for x being set st x in G holds
S2[x,f . x] from FUNCT_2:sch_1(A36);
set FxVxVx =  {  ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g )  }  ;
take V = meet FVx; ::_thesis: ( V is a_neighborhood of 0. X & K + V misses C + V )
A40: rng g c= xV
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng g or x in xV )
assume  x in rng g ; ::_thesis: x in xV
then consider y being set  such that
A41: y in dom g and
A42: x = g . y by FUNCT_1:def_3;
 x in y by A22, A23, A41, A42;
hence  x in xV by A22, A41; ::_thesis: verum
end;
A43: for A being Subset of X st A in G holds
ex x being Point of X ex Vx being open a_neighborhood of 0. X st
( A = x + Vx & [x,Vx] in rng g )
proof
let A be Subset of X; ::_thesis: ( A in G implies ex x being Point of X ex Vx being open a_neighborhood of 0. X st
( A = x + Vx & [x,Vx] in rng g ) )
assume  A in G ; ::_thesis: ex x being Point of X ex Vx being open a_neighborhood of 0. X st
( A = x + Vx & [x,Vx] in rng g )
then  A in F by A33;
hence  ex x being Point of X ex Vx being open a_neighborhood of 0. X st
( A = x + Vx & [x,Vx] in rng g ) ; ::_thesis: verum
end;
A44: now__::_thesis:_ex_z_being_set_st_z_in_FVx
consider y being Point of X such that
A45: y in K by A3, SUBSET_1:4;
consider W being Subset of X such that
 y in W and
A46: W in G by A34, A45, Th2;
consider x being Point of X, Vx being open a_neighborhood of 0. X such that
A47: ( W = x + Vx & [x,Vx] in rng g ) by A43, A46;
 Vx in FVx by A46, A47;
hence  ex z being set st z in FVx ; ::_thesis: verum
end;
then A48: dom f = G by FUNCT_2:def_1;
A49: FVx c= rng f
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in FVx or z in rng f )
assume  z in FVx ; ::_thesis: z in rng f
then consider Vx being open a_neighborhood of 0. X such that
A50: z = Vx and
A51: ex x being Point of X st
( x + Vx in G & [x,Vx] in rng g ) ;
consider x being Point of X such that
A52: x + Vx in G and
A53: [x,Vx] in rng g by A51;
consider v being Point of X, Vv being open a_neighborhood of 0. X such that
A54: x + Vx = v + Vv and
 v + Vv in G and
A55: [v,Vv] in rng g 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 being set  such that
A58: A in dom g and
A59: [x,Vx] = g . A by A53, FUNCT_1:def_3;
consider a being set  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 being set  such that
A63: B in dom g and
A64: [v,Vv] = g . B by A55, FUNCT_1:def_3;
consider b being set  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  z in rng f by A48, A50, A52, A56, FUNCT_1:3; ::_thesis: verum
end;
A67: for x being Point of X
for Vx being open a_neighborhood of 0. X st x + Vx in G & [x,Vx] in rng g holds
( x in K & Vx is symmetric & ((x + Vx) + Vx) + Vx misses C )
proof
let x be Point of X; ::_thesis: for Vx being open a_neighborhood of 0. X st x + Vx in G & [x,Vx] in rng g holds
( x in K & Vx is symmetric & ((x + Vx) + Vx) + Vx misses C )
let Vx be open a_neighborhood of 0. X; ::_thesis: ( x + Vx in G & [x,Vx] in rng g implies ( x in K & Vx is symmetric & ((x + Vx) + Vx) + Vx misses C ) )
assume that
A68: x + Vx in G and
A69: [x,Vx] in rng g ; ::_thesis: ( x in K & Vx is symmetric & ((x + Vx) + Vx) + Vx misses C )
consider A being set  such that
A70: A in dom g and
A71: [x,Vx] = g . A by A69, FUNCT_1:def_3;
consider a being set  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 being Point of X, Vv being open a_neighborhood of 0. X such that
A75: x + Vx = v + Vv and
A76: [v,Vv] in rng g ;
 [[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 being set  such that
A78: B in dom g and
A79: [v,Vv] = g . B by A76, FUNCT_1:def_3;
consider b being set  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 being Point of X, Vu being 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  ( x in K & Vx is symmetric & ((x + Vx) + Vx) + Vx misses C ) by A84, A85, A82, A83, XTUPLE_0:1; ::_thesis: verum
end;
now__::_thesis:_for_Z_being_set_holds_
(_(_Z_in_{{}}_implies_ex_A,_B_being_set_st_
(_A_in_{(C_+_V)}_&_B_in__{__((x_+_Vx)_+_Vx)_where_x_is_Point_of_X,_Vx_is_open_a_neighborhood_of_0._X_:_(_x_+_Vx_in_G_&_[x,Vx]_in_rng_g_)__}__&_Z_=_A_/\_B_)_)_&_(_ex_A,_B_being_set_st_
(_A_in_{(C_+_V)}_&_B_in__{__((x_+_Vx)_+_Vx)_where_x_is_Point_of_X,_Vx_is_open_a_neighborhood_of_0._X_:_(_x_+_Vx_in_G_&_[x,Vx]_in_rng_g_)__}__&_Z_=_A_/\_B_)_implies_Z_in_{{}}_)_)
let Z be set ; ::_thesis: ( ( Z in {{}} implies ex A, B being set st
( A in {(C + V)} & B in  {  ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g )  }  & Z = A /\ B ) ) & ( ex A, B being set st
( A in {(C + V)} & B in  {  ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g )  }  & Z = A /\ B ) implies Z in {{}} ) )
hereby  ::_thesis: ( ex A, B being set st
( A in {(C + V)} & B in  {  ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g )  }  & Z = A /\ B ) implies Z in {{}} )
reconsider A = C + V as set ;
assume  Z in {{}} ; ::_thesis: ex A, B being set st
( A in {(C + V)} & B in  {  ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g )  }  & Z = A /\ B )
then A86: Z = {} by TARSKI:def_1;
consider y being Point of X such that
A87: y in K by A3, SUBSET_1:4;
consider W being Subset of X such that
 y in W and
A88: W in G by A34, A87, Th2;
consider x being Point of X, Vx being open a_neighborhood of 0. X such that
A89: ( W = x + Vx & [x,Vx] in rng g ) by A43, A88;
A90: ((x + Vx) + Vx) + Vx misses C by A67, A88, A89;
reconsider B = (x + Vx) + Vx as set ;
take A = A; ::_thesis: ex B being set st
( A in {(C + V)} & B in  {  ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g )  }  & Z = A /\ B )
take B = B; ::_thesis: ( A in {(C + V)} & B in  {  ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g )  }  & Z = A /\ B )
thus  A in {(C + V)} by TARSKI:def_1; ::_thesis: ( B in  {  ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g )  }  & Z = A /\ B )
thus  B in  {  ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g )  }  by A88, A89; ::_thesis: Z = A /\ B
A91: Vx is symmetric by A67, A88, A89;
now__::_thesis:_not_A_meets_B
A92: C + V =  {  (u + v) where u, v is Point of X : ( u in C & v in V )  }  by RUSUB_4:def_9;
assume  A meets B ; ::_thesis: contradiction
then consider z being set  such that
A93: z in A and
A94: z in B by XBOOLE_0:3;
reconsider z = z as Point of X by A93;
consider u, v being 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 by RLVECT_1:4 ;
hence  contradiction by A90, A96, A98, XBOOLE_0:3; ::_thesis: verum
end;
hence  Z = A /\ B by A86, XBOOLE_0:def_7; ::_thesis: verum
end;
given A, B being set  such that A99: A in {(C + V)} and
A100: B in  {  ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g )  }  and
A101: Z = A /\ B ; ::_thesis: Z in {{}}
A102: A = C + V by A99, TARSKI:def_1;
consider x being Point of X, Vx being open a_neighborhood of 0. X such that
A103: B = (x + Vx) + Vx and
A104: ( x + Vx in G & [x,Vx] in rng g ) by A100;
A105: ((x + Vx) + Vx) + Vx misses C by A67, A104;
A106: Vx is symmetric by A67, A104;
now__::_thesis:_not_A_meets_B
A107: C + V =  {  (u + v) where u, v is Point of X : ( u in C & v in V )  }  by RUSUB_4:def_9;
assume  A meets B ; ::_thesis: contradiction
then consider z being set  such that
A108: z in A and
A109: z in B by XBOOLE_0:3;
reconsider z = z as Point of X by A99, A108;
consider u, v being 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 by RLVECT_1:4 ;
hence  contradiction by A105, A111, A113, XBOOLE_0:3; ::_thesis: verum
end;
then  A /\ B = {} by XBOOLE_0:def_7;
hence  Z in {{}} by A101, TARSKI:def_1; ::_thesis: verum
end;
then  INTERSECTION ({(C + V)}, {  ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g )  }  ) = {{}} by SETFAM_1:def_5;
then  union (INTERSECTION ({(C + V)}, {  ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g )  }  )) = {} by ZFMISC_1:25;
then  (C + V) /\ (union  {  ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g )  }  ) = {} by SETFAM_1:25;
then A114: C + V misses union  {  ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g )  }  by XBOOLE_0:def_7;
A115: FVx is open
proof
let P be Subset of X; :: according to TOPS_2:def_1 ::_thesis: ( not P in FVx or P is open )
assume  P in FVx ; ::_thesis: P is open
then  ex Vx being open a_neighborhood of 0. X st
( P = Vx & ex x being Point of X st
( x + Vx in G & [x,Vx] in rng g ) ) ;
hence  P is open ; ::_thesis: verum
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__::_thesis:_for_A_being_set_st_A_in_FVx_holds_
0._X_in_A
let A be set ; ::_thesis: ( A in FVx implies 0. X in A )
assume A117: A in FVx ; ::_thesis: 0. X in A
then reconsider A9 = A as Subset of X ;
 ex Vx being open a_neighborhood of 0. X st
( A = Vx & ex x being Point of X st
( x + Vx in G & [x,Vx] in rng g ) ) 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 ; ::_thesis: verum
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; ::_thesis: K + V misses C + V
set FxVxV =  {  ((x + Vx) + V) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g )  }  ;
A118: union  {  ((x + Vx) + V) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g )  }  c= union  {  ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g )  }
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union  {  ((x + Vx) + V) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g )  }  or z in union  {  ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g )  }  )
assume  z in union  {  ((x + Vx) + V) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g )  }  ; ::_thesis: z in union  {  ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g )  }
then consider Y being set  such that
A119: z in Y and
A120: Y in  {  ((x + Vx) + V) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g )  }  by TARSKI:def_4;
consider x being Point of X, Vx being open a_neighborhood of 0. X such that
A121: Y = (x + Vx) + V and
A122: ( x + Vx in G & [x,Vx] in rng g ) by A120;
A123: (x + Vx) + Vx in  {  ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g )  }  by A122;
 (x + Vx) + V =  {  (u + v) where u, v is Point of X : ( u in x + Vx & v in V )  }  by RUSUB_4:def_9;
then consider u, v being 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  z in union  {  ((x + Vx) + Vx) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g )  }  by A124, A123, TARSKI:def_4; ::_thesis: verum
end;
 K + V c= union  {  ((x + Vx) + V) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g )  }
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in K + V or z in union  {  ((x + Vx) + V) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g )  }  )
A127: K + V =  {  (u + v) where u, v is Point of X : ( u in K & v in V )  }  by RUSUB_4:def_9;
assume  z in K + V ; ::_thesis: z in union  {  ((x + Vx) + V) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g )  }
then consider u, v being Point of X such that
A128: z = u + v and
A129: u in K and
A130: v in V by A127;
consider Vu being Subset of X such that
A131: u in Vu and
A132: Vu in G by A34, A129, Th2;
consider x being Point of X, Vx being open a_neighborhood of 0. X such that
A133: Vu = x + Vx and
A134: [x,Vx] in rng g by A43, A132;
A135: (x + Vx) + V in  {  ((x + Vx) + V) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g )  }  by A132, A133, A134;
 z in (x + Vx) + V by A128, A130, A131, A133, Th3;
hence  z in union  {  ((x + Vx) + V) where x is Point of X, Vx is open a_neighborhood of 0. X : ( x + Vx in G & [x,Vx] in rng g )  }  by A135, TARSKI:def_4; ::_thesis: verum
end;
hence  K + V misses C + V by A118, A114, XBOOLE_1:1, XBOOLE_1:63; ::_thesis: verum
end;
end;
end;

theorem Th58: :: RLTOPSP1:58
for X being LinearTopSpace
for B being local_base of X
for V being a_neighborhood of 0. X ex W being a_neighborhood of 0. X st
( W in B & Cl W c= V )
proof
let X be LinearTopSpace; ::_thesis: for B being local_base of X
for V being a_neighborhood of 0. X ex W being a_neighborhood of 0. X st
( W in B & Cl W c= V )
let B be local_base of X; ::_thesis: for V being a_neighborhood of 0. X ex W being a_neighborhood of 0. X st
( W in B & Cl W c= V )
let V be a_neighborhood of 0. X; ::_thesis: ex W being a_neighborhood of 0. X st
( W in B & Cl W c= V )
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 being a_neighborhood of 0. X such that
A1: {(0. X)} + P misses ((Int V) `) + 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;
 ( {(0. X)} + P9 c= {(0. X)} + P & ((Int V) `) + P9 c= ((Int V) `) + P ) by Lm3, TOPS_1:16;
then  {(0. X)} + P9 misses ((Int V) `) + P9 by A1, XBOOLE_1:64;
then  Cl ({(0. X)} + P9) misses ((Int V) `) + P9 by TSEP_1:36;
then  Cl ({(0. X)} + P9) misses (Int V) ` by A2, Th12, XBOOLE_1:63;
then  Cl P9 misses (Int V) ` by CONVEX1:35;
then A3: Cl P9 c= Int V by SUBSET_1:24;
consider W being a_neighborhood of 0. X such that
A4: W in B and
A5: W c= P9 by YELLOW13:def_2;
take  W ; ::_thesis: ( W in B & Cl W c= V )
thus  W in B by A4; ::_thesis: Cl W c= V
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, XBOOLE_1:1;
hence  Cl W c= V by A6, XBOOLE_1:1; ::_thesis: verum
end;

theorem Th59: :: RLTOPSP1:59
for X being LinearTopSpace
for V being a_neighborhood of 0. X ex W being a_neighborhood of 0. X st Cl W c= V
proof
let X be LinearTopSpace; ::_thesis: for V being a_neighborhood of 0. X ex W being a_neighborhood of 0. X st Cl W c= V
let V be a_neighborhood of 0. X; ::_thesis: ex W being a_neighborhood of 0. X st Cl W c= V
set B =  {  U where U is a_neighborhood of 0. X : verum  }  ;
  {  U where U is a_neighborhood of 0. X : verum  }  c= bool the carrier of X
proof
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in  {  U where U is a_neighborhood of 0. X : verum  }  or A in bool the carrier of X )
assume  A in  {  U where U is a_neighborhood of 0. X : verum  }  ; ::_thesis: A in bool the carrier of X
then  ex U being a_neighborhood of 0. X st A = U ;
hence  A in bool the carrier of X ; ::_thesis: verum
end;
then   {  U where U is a_neighborhood of 0. X : verum  }  is local_base of X by Th44;
then consider W being a_neighborhood of 0. X such that
 W in  {  U where U is a_neighborhood of 0. X : verum  }  and
A1: Cl W c= V by Th58;
take  W ; ::_thesis: Cl W c= V
thus  Cl W c= V by A1; ::_thesis: verum
end;

registration
cluster non empty TopSpace-like T_1 right_complementable Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital add-continuous Mult-continuous  ->  Hausdorff for RLTopStruct ;
coherence
 for b1 being LinearTopSpace st b1 is T_1 holds
b1 is Hausdorff
proof
let X be LinearTopSpace; ::_thesis: ( X is T_1 implies X is Hausdorff )
assume A1: X is T_1 ; ::_thesis: X is Hausdorff
let p, q be Point of X; :: according to PRE_TOPC:def_10 ::_thesis: ( p = q or ex b1, b2 being Element of bool the carrier of X st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 ) )
assume A2: p <> q ; ::_thesis: ex b1, b2 being Element of bool the carrier of X st
( b1 is open & b2 is open & p in b1 & q in b2 & b1 misses b2 )
 {q} is closed by A1, URYSOHN1:19;
then consider V being a_neighborhood of 0. X such that
A3: {p} + V misses {q} + V by A2, Th57, ZFMISC_1:11;
take  p + (Int V) ; ::_thesis: ex b1 being Element of bool the carrier of X st
( p + (Int V) is open & b1 is open & p in p + (Int V) & q in b1 & p + (Int V) misses b1 )
take  q + (Int V) ; ::_thesis: ( p + (Int V) is open & q + (Int V) is open & p in p + (Int V) & q in q + (Int V) & p + (Int V) misses 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 ) ; ::_thesis: ( p in p + (Int V) & q in q + (Int V) & p + (Int V) misses q + (Int V) )
 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) ) by RLVECT_1:4; ::_thesis: p + (Int V) misses q + (Int V)
 ( p + (Int V) c= p + V & q + (Int V) c= q + V ) by Th8, TOPS_1:16;
hence  p + (Int V) misses q + (Int V) by A3, A4, XBOOLE_1:64; ::_thesis: verum
end;
end;

theorem :: RLTOPSP1:60
for X being LinearTopSpace
for A being Subset of X holds Cl A = meet  {  (A + V) where V is a_neighborhood of 0. X : verum  }
proof
let X be LinearTopSpace; ::_thesis: for A being Subset of X holds Cl A = meet  {  (A + V) where V is a_neighborhood of 0. X : verum  }
let A be Subset of X; ::_thesis: Cl A = meet  {  (A + V) where V is a_neighborhood of 0. X : verum  }
set AV =  {  (A + V) where V is a_neighborhood of 0. X : verum  }  ;
set V = the a_neighborhood of 0. X;
A1: for x being Point of X
for V being 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; ::_thesis: for V being a_neighborhood of 0. X holds
( A meets x + (Int V) iff x in A + ((- 1) * (Int V)) )
let V be a_neighborhood of 0. X; ::_thesis: ( A meets x + (Int V) iff x in A + ((- 1) * (Int V)) )
A2: A + ((- 1) * (Int V)) =  {  (a + v) where a, v is Point of X : ( a in A & v in (- 1) * (Int V) )  }  by RUSUB_4:def_9;
hereby  ::_thesis: ( x in A + ((- 1) * (Int V)) implies A meets x + (Int V) )
assume  A meets x + (Int V) ; ::_thesis: x in A + ((- 1) * (Int V))
then  x in A + (- (Int V)) by Th24;
hence  x in A + ((- 1) * (Int V)) ; ::_thesis: verum
end;
assume  x in A + ((- 1) * (Int V)) ; ::_thesis: A meets x + (Int V)
then consider a, v being 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 being 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 by RLVECT_1:4 ;
 x + (Int V) =  {  (x + w) where w is Point of X : w in Int V  }  by RUSUB_4:def_8;
then  x + v9 in x + (Int V) by A7;
hence  A meets x + (Int V) by A4, A8, XBOOLE_0:3; ::_thesis: verum
end;
  {  (A + V) where V is a_neighborhood of 0. X : verum  }  c= bool the carrier of X
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  (A + V) where V is a_neighborhood of 0. X : verum  }  or x in bool the carrier of X )
assume  x in  {  (A + V) where V is a_neighborhood of 0. X : verum  }  ; ::_thesis: x in bool the carrier of X
then  ex V being a_neighborhood of 0. X st x = A + V ;
hence  x in bool the carrier of X ; ::_thesis: verum
end;
then reconsider AV9 =  {  (A + V) where V is a_neighborhood of 0. X : verum  }  as Subset-Family of X ;
A9: for x being Point of X holds
( x in Cl A iff for V being a_neighborhood of 0. X holds A meets x + (Int V) )
proof
let x be Point of X; ::_thesis: ( x in Cl A iff for V being a_neighborhood of 0. X holds A meets x + (Int V) )
hereby  ::_thesis: ( ( for V being a_neighborhood of 0. X holds A meets x + (Int V) ) implies x in Cl A )
assume A10: x in Cl A ; ::_thesis: for V being a_neighborhood of 0. X holds A meets x + (Int V)
let V be a_neighborhood of 0. X; ::_thesis: A meets x + (Int V)
 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) by RLVECT_1:4;
hence  A meets x + (Int V) by A10, TOPS_1:12; ::_thesis: verum
end;
assume A11: for V being a_neighborhood of 0. X holds A meets x + (Int V) ; ::_thesis: x in Cl A
now__::_thesis:_for_V_being_Subset_of_X_st_V_is_open_&_x_in_V_holds_
A_meets_V
let V be Subset of X; ::_thesis: ( V is open & x in V implies A meets V )
assume that
A12: V is open and
A13: x in V ; ::_thesis: A meets 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; ::_thesis: verum
end;
hence  x in Cl A by TOPS_1:12; ::_thesis: verum
end;
A15: A + the a_neighborhood of 0. X in  {  (A + V) where V is a_neighborhood of 0. X : verum  }  ;
thus  Cl A c= meet  {  (A + V) where V is a_neighborhood of 0. X : verum  }  :: according to XBOOLE_0:def_10 ::_thesis: meet  {  (A + V) where V is a_neighborhood of 0. X : verum  }  c= Cl A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Cl A or x in meet  {  (A + V) where V is a_neighborhood of 0. X : verum  }  )
assume A16: x in Cl A ; ::_thesis: x in meet  {  (A + V) where V is a_neighborhood of 0. X : verum  }
then reconsider x = x as Point of X ;
now__::_thesis:_for_Y_being_set_st_Y_in__{__(A_+_V)_where_V_is_a_neighborhood_of_0._X_:_verum__}__holds_
x_in_Y
let Y be set ; ::_thesis: ( Y in  {  (A + V) where V is a_neighborhood of 0. X : verum  }  implies x in Y )
assume  Y in  {  (A + V) where V is a_neighborhood of 0. X : verum  }  ; ::_thesis: x in Y
then consider V being a_neighborhood of 0. X such that
A17: Y = A + V ;
A18: A + V =  {  (a + v) where a, v is 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 is 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 being Point of X such that
A20: ( x = a + v & a in A ) and
A21: v in (- 1) * (Int ((- 1) * V)) ;
consider v9 being 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 being 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; ::_thesis: verum
end;
hence  x in meet  {  (A + V) where V is a_neighborhood of 0. X : verum  }  by A15, SETFAM_1:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in meet  {  (A + V) where V is a_neighborhood of 0. X : verum  }  or x in Cl A )
assume A26: x in meet  {  (A + V) where V is a_neighborhood of 0. X : verum  }  ; ::_thesis: x in Cl A
 meet AV9 c= the carrier of X ;
then reconsider x = x as Point of X by A26;
now__::_thesis:_for_V_being_a_neighborhood_of_0._X_holds_A_meets_x_+_(Int_V)
let V be a_neighborhood of 0. X; ::_thesis: A meets x + (Int V)
 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  {  (A + V) where V is a_neighborhood of 0. X : verum  }  ;
then  x in A + ((- 1) * (Int V)) by A26, SETFAM_1:def_1;
hence  A meets x + (Int V) by A1; ::_thesis: verum
end;
hence  x in Cl A by A9; ::_thesis: verum
end;

theorem Th61: :: RLTOPSP1:61
for X being LinearTopSpace
for A, B being Subset of X holds (Int A) + (Int B) c= Int (A + B)
proof
let X be LinearTopSpace; ::_thesis: for A, B being Subset of X holds (Int A) + (Int B) c= Int (A + B)
let A, B be Subset of X; ::_thesis: (Int A) + (Int B) c= Int (A + B)
 ( Int A c= A & Int B c= B ) by TOPS_1:16;
then  (Int A) + (Int B) c= A + B by Th11;
hence  (Int A) + (Int B) c= Int (A + B) by TOPS_1:24; ::_thesis: verum
end;

theorem Th62: :: RLTOPSP1:62
for X being LinearTopSpace
for A, B being Subset of X holds (Cl A) + (Cl B) c= Cl (A + B)
proof
let X be LinearTopSpace; ::_thesis: for A, B being Subset of X holds (Cl A) + (Cl B) c= Cl (A + B)
let A, B be Subset of X; ::_thesis: (Cl A) + (Cl B) c= Cl (A + B)
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in (Cl A) + (Cl B) or z in Cl (A + B) )
assume A1: z in (Cl A) + (Cl B) ; ::_thesis: z in Cl (A + B)
then reconsider z = z as Point of X ;
  {  (u + v) where u, v is Point of X : ( u in Cl A & v in Cl B )  }  = (Cl A) + (Cl B) by RUSUB_4:def_9;
then consider a, b being Point of X such that
A2: z = a + b and
A3: a in Cl A and
A4: b in Cl B by A1;
now__::_thesis:_for_W_being_Subset_of_X_st_W_is_open_&_z_in_W_holds_
A_+_B_meets_W
let W be Subset of X; ::_thesis: ( W is open & z in W implies A + B meets W )
assume that
A5: W is open and
A6: z in W ; ::_thesis: A + B meets W
 W is a_neighborhood of z by A5, A6, CONNSP_2:3;
then consider W1 being a_neighborhood of a, W2 being 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 being set  such that
A8: x in A and
A9: x in Int W1 by XBOOLE_0:3;
reconsider x = 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 being set  such that
A11: y in B and
A12: y in Int W2 by XBOOLE_0:3;
reconsider y = 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; ::_thesis: verum
end;
hence  z in Cl (A + B) by TOPS_1:12; ::_thesis: verum
end;

Lm16:  for X being LinearTopSpace
for C being convex Subset of X holds Cl C is convex
proof
let X be LinearTopSpace; ::_thesis: for C being convex Subset of X holds Cl C is convex
let C be convex Subset of X; ::_thesis: Cl C is convex
now__::_thesis:_for_r_being_Real_st_0_<_r_&_r_<_1_holds_
(r_*_(Cl_C))_+_((1_-_r)_*_(Cl_C))_c=_Cl_C
let r be Real; ::_thesis: ( 0 < r & r < 1 implies (r * (Cl C)) + ((1 - r) * (Cl C)) c= Cl C )
assume that
A1: 0 < r and
A2: r < 1 ; ::_thesis: (r * (Cl C)) + ((1 - r) * (Cl C)) c= Cl C
 (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, XBOOLE_1:1; ::_thesis: verum
end;
hence  Cl C is convex by CONVEX1:4; ::_thesis: verum
end;

registration
let X be LinearTopSpace;
let C be convex Subset of X;
cluster Cl C ->  convex ;
coherence
 Cl C is convex by Lm16;
end;

Lm17:  for X being LinearTopSpace
for C being convex Subset of X holds Int C is convex
proof
let X be LinearTopSpace; ::_thesis: for C being convex Subset of X holds Int C is convex
let C be convex Subset of X; ::_thesis: Int C is convex
now__::_thesis:_for_r_being_Real_st_0_<_r_&_r_<_1_holds_
(r_*_(Int_C))_+_((1_-_r)_*_(Int_C))_c=_Int_C
let r be Real; ::_thesis: ( 0 < r & r < 1 implies (r * (Int C)) + ((1 - r) * (Int C)) c= Int C )
assume that
A1: 0 < r and
A2: r < 1 ; ::_thesis: (r * (Int C)) + ((1 - r) * (Int C)) c= Int C
 (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, XBOOLE_1:1; ::_thesis: verum
end;
hence  Int C is convex by CONVEX1:4; ::_thesis: verum
end;

registration
let X be LinearTopSpace;
let C be convex Subset of X;
cluster Int C ->  convex ;
coherence
 Int C is convex by Lm17;
end;

Lm18:  for X being LinearTopSpace
for B being circled Subset of X holds Cl B is circled
proof
let X be LinearTopSpace; ::_thesis: for B being circled Subset of X holds Cl B is circled
let B be circled Subset of X; ::_thesis: Cl B is circled
let r be Real; :: according to RLTOPSP1:def_6 ::_thesis: ( abs r <= 1 implies r * (Cl B) c= Cl B )
assume A1: abs r <= 1 ; ::_thesis: r * (Cl B) c= Cl B
percases ( r = 0 or r <> 0 ) ;
supposeA2: r = 0 ; ::_thesis: r * (Cl B) c= Cl B
now__::_thesis:_r_*_(Cl_B)_c=_Cl_B
percases ( B = {} X or B <> {} X ) ;
suppose B = {} X ; ::_thesis: r * (Cl B) c= Cl B
then  Cl B = {} X by PRE_TOPC:22;
hence  r * (Cl B) c= Cl B by CONVEX1:33; ::_thesis: verum
end;
supposeA3: B <> {} X ; ::_thesis: r * (Cl B) c= Cl B
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  r * (Cl B) c= Cl B by A5, A4, ZFMISC_1:31; ::_thesis: verum
end;
end;
end;
hence  r * (Cl B) c= Cl B ; ::_thesis: verum
end;
supposeA6: r <> 0 ; ::_thesis: r * (Cl B) c= Cl B
 r * B c= B by A1, Def6;
then  Cl (r * B) c= Cl B by PRE_TOPC:19;
hence  r * (Cl B) c= Cl B by A6, Th52; ::_thesis: verum
end;
end;
end;

registration
let X be LinearTopSpace;
let B be circled Subset of X;
cluster Cl B ->  circled ;
coherence
 Cl B is circled by Lm18;
end;

theorem :: RLTOPSP1:63
for X being LinearTopSpace
for B being circled Subset of X st 0. X in Int B holds
Int B is circled
proof
let X be LinearTopSpace; ::_thesis: for B being circled Subset of X st 0. X in Int B holds
Int B is circled
let B be circled Subset of X; ::_thesis: ( 0. X in Int B implies Int B is circled )
assume A1: 0. X in Int B ; ::_thesis: Int B is circled
let r be Real; :: according to RLTOPSP1:def_6 ::_thesis: ( abs r <= 1 implies r * (Int B) c= Int B )
assume  abs r <= 1 ; ::_thesis: r * (Int B) c= Int B
then  r * B c= B by Def6;
then A2: Int (r * B) c= Int B by TOPS_1:19;
percases ( r = 0 or r <> 0 ) ;
suppose r = 0 ; ::_thesis: r * (Int B) c= Int B
then  r * (Int B) = {(0. X)} by A1, CONVEX1:34;
hence  r * (Int B) c= Int B by A1, ZFMISC_1:31; ::_thesis: verum
end;
suppose r <> 0 ; ::_thesis: r * (Int B) c= Int B
hence  r * (Int B) c= Int B by A2, Th51; ::_thesis: verum
end;
end;
end;

Lm19:  for X being LinearTopSpace
for E being bounded Subset of X holds Cl E is bounded
proof
let X be LinearTopSpace; ::_thesis: for E being bounded Subset of X holds Cl E is bounded
let E be bounded Subset of X; ::_thesis: Cl E is bounded
let V be a_neighborhood of 0. X; :: according to RLTOPSP1:def_12 ::_thesis: ex s being Real st
( s > 0 & ( for t being Real st t > s holds
Cl E c= t * V ) )
consider W being a_neighborhood of 0. X such that
A1: Cl W c= V by Th59;
consider s being Real such that
A2: s > 0 and
A3: for t being Real st t > s holds
E c= t * W by Def12;
take  s ; ::_thesis: ( s > 0 & ( for t being Real st t > s holds
Cl E c= t * V ) )
thus  s > 0 by A2; ::_thesis: for t being Real st t > s holds
Cl E c= t * V
let t be Real; ::_thesis: ( t > s implies Cl E c= t * V )
assume  t > s ; ::_thesis: Cl E c= t * V
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  Cl E c= t * V by A4, XBOOLE_1:1; ::_thesis: verum
end;

registration
let X be LinearTopSpace;
let E be bounded Subset of X;
cluster Cl E ->  bounded ;
coherence
 Cl E is bounded by Lm19;
end;

Lm20:  for X being LinearTopSpace
for U, V being a_neighborhood of 0. X
for F being Subset-Family of X
for r being positive Real st ( for s being Real st abs s < r holds
s * V c= U ) & F =  {  (a * V) where a is Real : abs a < r  }  holds
( union F is a_neighborhood of 0. X & union F is circled & union F c= U )
proof
let X be LinearTopSpace; ::_thesis: for U, V being a_neighborhood of 0. X
for F being Subset-Family of X
for r being positive Real st ( for s being Real st abs s < r holds
s * V c= U ) & F =  {  (a * V) where a is Real : abs a < r  }  holds
( union F is a_neighborhood of 0. X & union F is circled & union F c= U )
let U, V be a_neighborhood of 0. X; ::_thesis: for F being Subset-Family of X
for r being positive Real st ( for s being Real st abs s < r holds
s * V c= U ) & F =  {  (a * V) where a is Real : abs a < r  }  holds
( union F is a_neighborhood of 0. X & union F is circled & union F c= U )
let F be Subset-Family of X; ::_thesis: for r being positive Real st ( for s being Real st abs s < r holds
s * V c= U ) & F =  {  (a * V) where a is Real : abs a < r  }  holds
( union F is a_neighborhood of 0. X & union F is circled & union F c= U )
let r be positive Real; ::_thesis: ( ( for s being Real st abs s < r holds
s * V c= U ) & F =  {  (a * V) where a is Real : abs a < r  }  implies ( union F is a_neighborhood of 0. X & union F is circled & union F c= U ) )
assume that
A1: for s being Real st abs s < r holds
s * V c= U and
A2: F =  {  (a * V) where a is Real : abs a < r  }  ; ::_thesis: ( union F is a_neighborhood of 0. X & union F is circled & union F c= U )
set W = union F;
thus  union F is a_neighborhood of 0. X ::_thesis: ( union F is circled & union F c= U )
proof
set F9 =  {  (a * (Int V)) where a is non zero Real : abs a < r  }  ;
consider a being real number  such that
A3: 0 < a and
A4: a < r by XREAL_1:5;
reconsider a = a as Real by XREAL_0:def_1;
 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) by RLVECT_1:10;
A6:  {  (a * (Int V)) where a is non zero Real : abs a < r  }  c= bool the carrier of X
proof
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in  {  (a * (Int V)) where a is non zero Real : abs a < r  }  or A in bool the carrier of X )
assume  A in  {  (a * (Int V)) where a is non zero Real : abs a < r  }  ; ::_thesis: A in bool the carrier of X
then  ex a being non zero Real st
( A = a * (Int V) & abs a < r ) ;
hence  A in bool the carrier of X ; ::_thesis: verum
end;
 abs a < r by A3, A4, ABSVALUE:def_1;
then  a * (Int V) in  {  (a * (Int V)) where a is non zero Real : abs a < r  }  by A3;
then A7: 0. X in union  {  (a * (Int V)) where a is non zero Real : abs a < r  }  by A5, TARSKI:def_4;
reconsider F9 =  {  (a * (Int V)) where a is non zero Real : abs a < r  }  as Subset-Family of X by A6;
 union F9 c= union F
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union F9 or x in union F )
A8: Int V c= V by TOPS_1:16;
assume  x in union F9 ; ::_thesis: x in union F
then consider P being set  such that
A9: x in P and
A10: P in F9 by TARSKI:def_4;
consider a being non zero Real such that
A11: P = a * (Int V) and
A12: abs a < r by A10;
 ex v being 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  x in union F by A13, TARSKI:def_4; ::_thesis: verum
end;
then A14: Int (union F9) c= Int (union F) by TOPS_1:19;
 F9 is open
proof
let P be Subset of X; :: according to TOPS_2:def_1 ::_thesis: ( not P in F9 or P is open )
assume  P in F9 ; ::_thesis: P is open
then  ex a being non zero Real st
( P = a * (Int V) & abs a < r ) ;
hence  P is open by Th49; ::_thesis: verum
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 (union F) by A14; :: according to CONNSP_2:def_1 ::_thesis: verum
end;
thus  union F is circled ::_thesis: union F c= U
proof
let s be Real; :: according to RLTOPSP1:def_6 ::_thesis: ( abs s <= 1 implies s * (union F) c= union F )
assume  abs s <= 1 ; ::_thesis: s * (union F) c= union F
then A15: (abs s) * r <= r by XREAL_1:153;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in s * (union F) or z in union F )
assume  z in s * (union F) ; ::_thesis: z in union F
then consider u being Point of X such that
A16: z = s * u and
A17: u in union F ;
consider Y being set  such that
A18: u in Y and
A19: Y in F by A17, TARSKI:def_4;
consider a being Real such that
A20: Y = a * V and
A21: abs a < r by A2, A19;
consider v being 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;
percases ( 0 <> abs s or abs s = 0 ) ;
suppose 0 <> abs s ; ::_thesis: z in union F
then  s <> 0 by ABSVALUE:2;
then  0 < abs s by COMPLEX1:47;
then  (abs s) * (abs a) < (abs s) * r by A21, XREAL_1:68;
then  (abs s) * (abs a) < r by A15, XXREAL_0:2;
then  abs (s * a) < r by COMPLEX1:65;
then  (s * a) * V in F by A2;
hence  z in union F by A24, TARSKI:def_4; ::_thesis: verum
end;
suppose abs s = 0 ; ::_thesis: z in union F
then  s = 0 by ABSVALUE:2;
then  abs (s * a) = 0 by ABSVALUE:def_1;
then  (s * a) * V in F by A2;
hence  z in union F by A24, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in union F or z in U )
assume A25: z in union F ; ::_thesis: z in U
then reconsider z = z as Point of X ;
consider Y being set  such that
A26: z in Y and
A27: Y in F by A25, TARSKI:def_4;
consider a being Real such that
A28: Y = a * V and
A29: abs a < r by A2, A27;
 a * V c= U by A1, A29;
hence  z in U by A26, A28; ::_thesis: verum
end;

theorem Th64: :: RLTOPSP1:64
for X being LinearTopSpace
for U being a_neighborhood of 0. X ex W being a_neighborhood of 0. X st
( W is circled & W c= U )
proof
let X be LinearTopSpace; ::_thesis: for U being a_neighborhood of 0. X ex W being a_neighborhood of 0. X st
( W is circled & W c= U )
let U be a_neighborhood of 0. X; ::_thesis: ex W being a_neighborhood of 0. X st
( W is circled & W c= U )
 0. X = 0 * (0. X) by RLVECT_1:10;
then consider r being positive Real, V being a_neighborhood of 0. X such that
A1: for s being Real st abs (s - 0) < r holds
s * V c= U by Th32;
set F =  {  (a * V) where a is Real : abs a < r  }  ;
  {  (a * V) where a is Real : abs a < r  }  c= bool the carrier of X
proof
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in  {  (a * V) where a is Real : abs a < r  }  or A in bool the carrier of X )
assume  A in  {  (a * V) where a is Real : abs a < r  }  ; ::_thesis: A in bool the carrier of X
then  ex a being Real st
( A = a * V & abs a < r ) ;
hence  A in bool the carrier of X ; ::_thesis: verum
end;
then reconsider F =  {  (a * V) where a is Real : abs a < r  }  as Subset-Family of X ;
take  union F ; ::_thesis: ( union F is a_neighborhood of 0. X & union F is circled & union F c= U )
now__::_thesis:_for_s_being_Real_st_abs_s_<_r_holds_
s_*_V_c=_U
let s be Real; ::_thesis: ( abs s < r implies s * V c= U )
assume  abs s < r ; ::_thesis: s * V c= U
then  abs (s - 0) < r ;
hence  s * V c= U by A1; ::_thesis: verum
end;
hence  ( union F is a_neighborhood of 0. X & union F is circled & union F c= U ) by Lm20; ::_thesis: verum
end;

theorem Th65: :: RLTOPSP1:65
for X being LinearTopSpace
for U being a_neighborhood of 0. X st U is convex holds
ex W being a_neighborhood of 0. X st
( W is circled & W is convex & W c= U )
proof
let X be LinearTopSpace; ::_thesis: for U being a_neighborhood of 0. X st U is convex holds
ex W being a_neighborhood of 0. X st
( W is circled & W is convex & W c= U )
let U be a_neighborhood of 0. X; ::_thesis: ( U is convex implies ex W being a_neighborhood of 0. X st
( W is circled & W is convex & W c= U ) )
assume A1: U is convex ; ::_thesis: ex W being a_neighborhood of 0. X st
( W is circled & W is convex & W c= U )
set V = U /\ (- U);
 - U is a_neighborhood of 0. X by Th55;
then reconsider V = U /\ (- U) as a_neighborhood of 0. X by CONNSP_2:2;
take  V ; ::_thesis: ( V is circled & V is convex & V c= U )
A2: - U is convex by A1, CONVEX1:1;
thus  V is circled ::_thesis: ( V is convex & V c= U )
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; :: according to RLTOPSP1:def_6 ::_thesis: ( abs r <= 1 implies r * V c= V )
assume A5: abs r <= 1 ; ::_thesis: r * V c= V
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in r * V or u in V )
assume  u in r * V ; ::_thesis: u in V
then consider v being 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;
percases ( r < 0 or r >= 0 ) ;
supposeA10: r < 0 ; ::_thesis: u in V
then A11: - r <= 1 by A5, ABSVALUE:def_1;
then  ((- r) * v) + ((1 - (- r)) * (0. X)) in - U by A2, A8, A3, A10, Def1;
then  ((- r) * v) + (0. X) in - U by RLVECT_1:10;
then  (- r) * v in - U by RLVECT_1:def_4;
then consider u9 being 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, Def1;
then  ((- r) * v) + (0. X) in U by RLVECT_1:10;
then  (- r) * v in U by RLVECT_1:def_4;
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  u in V by A6, A13, A14, XBOOLE_0:def_4; ::_thesis: verum
end;
supposeA15: r >= 0 ; ::_thesis: u in V
A16: r <= 1 by A5, ABSVALUE:def_1;
then  (r * v) + ((1 - r) * (0. X)) in - U by A2, A8, A3, A15, Def1;
then  (r * v) + (0. X) in - U by RLVECT_1:10;
then A17: r * v in - U by RLVECT_1:def_4;
 (r * v) + ((1 - r) * (0. X)) in U by A1, A9, A4, A15, A16, Def1;
then  (r * v) + (0. X) in U by RLVECT_1:10;
then  r * v in U by RLVECT_1:def_4;
hence  u in V by A6, A17, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
end;
thus  V is convex by A1, A2; ::_thesis: V c= U
thus  V c= U by XBOOLE_1:17; ::_thesis: verum
end;

theorem :: RLTOPSP1:66
for X being LinearTopSpace ex P being local_base of X st P is circled-membered
proof
let X be LinearTopSpace; ::_thesis: ex P being local_base of X st P is circled-membered
defpred S1[ Subset of X] means $1 is circled ;
consider P being Subset-Family of X such that
A1: for V being Subset of X holds
( V in P iff S1[V] ) from SUBSET_1:sch_3();
reconsider P = P as Subset-Family of X ;
take  P ; ::_thesis: ( P is local_base of X & P is circled-membered )
thus  P is local_base of X ::_thesis: P is circled-membered
proof
let V be a_neighborhood of 0. X; :: according to YELLOW13:def_2 ::_thesis: ex b1 being a_neighborhood of 0. X st
( b1 in P & b1 c= V )
consider W being a_neighborhood of 0. X such that
A2: W is circled and
A3: W c= V by Th64;
take  W ; ::_thesis: ( W in P & W c= V )
thus  W in P by A1, A2; ::_thesis: W c= V
thus  W c= V by A3; ::_thesis: verum
end;
let V be Subset of X; :: according to RLTOPSP1:def_7 ::_thesis: ( V in P implies V is circled )
assume  V in P ; ::_thesis: V is circled
hence  V is circled by A1; ::_thesis: verum
end;

theorem :: RLTOPSP1:67
for X being LinearTopSpace st X is locally-convex holds
ex P being local_base of X st P is convex-membered
proof
let X be LinearTopSpace; ::_thesis: ( X is locally-convex implies ex P being local_base of X st P is convex-membered )
assume A1: X is locally-convex ; ::_thesis: ex P being local_base of X st P is convex-membered
defpred S1[ Subset of X] means ( $1 is circled & $1 is convex );
consider P being Subset-Family of X such that
A2: for V being Subset of X holds
( V in P iff S1[V] ) from SUBSET_1:sch_3();
reconsider P = P as Subset-Family of X ;
take  P ; ::_thesis: ( P is local_base of X & P is convex-membered )
thus  P is local_base of X ::_thesis: P is convex-membered
proof
let V be a_neighborhood of 0. X; :: according to YELLOW13:def_2 ::_thesis: ex b1 being a_neighborhood of 0. X st
( b1 in P & b1 c= V )
consider Q being local_base of X such that
A3: Q is convex-membered by A1, Def11;
consider U being a_neighborhood of 0. X such that
A4: U in Q and
A5: U c= V by YELLOW13:def_2;
 U is convex by A3, A4, Def3;
then consider W being a_neighborhood of 0. X such that
A6: ( W is circled & W is convex ) and
A7: W c= U by Th65;
take  W ; ::_thesis: ( W in P & W c= V )
thus  W in P by A2, A6; ::_thesis: W c= V
thus  W c= V by A5, A7, XBOOLE_1:1; ::_thesis: verum
end;
let V be Subset of X; :: according to RLTOPSP1:def_3 ::_thesis: ( V in P implies V is convex )
assume  V in P ; ::_thesis: V is convex
hence  V is convex by A2; ::_thesis: verum
end;

begin


theorem Th68: :: RLTOPSP1:68
for V being RealLinearSpace
for v, w being Point of V holds v in LSeg (v,w)
proof
let V be RealLinearSpace; ::_thesis: for v, w being Point of V holds v in LSeg (v,w)
let v, w be Point of V; ::_thesis: v in LSeg (v,w)
v = (1 - 0) * v by RLVECT_1:def_8
.= ((1 - 0) * v) + (0. V) by RLVECT_1:4
.= ((1 - 0) * v) + (0 * w) by RLVECT_1:10 ;
hence  v in LSeg (v,w) ; ::_thesis: verum
end;

theorem :: RLTOPSP1:69
for V being RealLinearSpace
for v, w being Point of V holds (1 / 2) * (v + w) in LSeg (v,w)
proof
let V be RealLinearSpace; ::_thesis: for v, w being Point of V holds (1 / 2) * (v + w) in LSeg (v,w)
let v, w be Point of V; ::_thesis: (1 / 2) * (v + w) in LSeg (v,w)
 (1 / 2) * (v + w) = ((1 - (1 / 2)) * v) + ((1 / 2) * w) by RLVECT_1:def_5;
hence  (1 / 2) * (v + w) in LSeg (v,w) ; ::_thesis: verum
end;

theorem :: RLTOPSP1:70
for V being RealLinearSpace
for v being Point of V holds LSeg (v,v) = {v}
proof
let V be RealLinearSpace; ::_thesis: for v being Point of V holds LSeg (v,v) = {v}
let v be Point of V; ::_thesis: LSeg (v,v) = {v}
thus  LSeg (v,v) c= {v} :: according to XBOOLE_0:def_10 ::_thesis: {v} c= LSeg (v,v)
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in LSeg (v,v) or a in {v} )
assume  a in LSeg (v,v) ; ::_thesis: a in {v}
then consider r being Real 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  a in {v} by TARSKI:def_1; ::_thesis: verum
end;
 v in LSeg (v,v) by Th68;
hence  {v} c= LSeg (v,v) by ZFMISC_1:31; ::_thesis: verum
end;

theorem :: RLTOPSP1:71
for V being RealLinearSpace
for v, w being Point of V st 0. V in LSeg (v,w) holds
ex r being Real st
( v = r * w or w = r * v )
proof
let V be RealLinearSpace; ::_thesis: for v, w being Point of V st 0. V in LSeg (v,w) holds
ex r being Real st
( v = r * w or w = r * v )
let v, w be Point of V; ::_thesis: ( 0. V in LSeg (v,w) implies ex r being Real st
( v = r * w or w = r * v ) )
assume  0. V in LSeg (v,w) ; ::_thesis: ex r being Real st
( v = r * w or w = r * v )
then consider s being 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;
percases ( - s <> 0 or - s = 0 ) ;
supposeA3: - s <> 0 ; ::_thesis: ex r being Real st
( v = r * w or w = r * v )
take r = ((- s) ") * (1 - s); ::_thesis: ( v = r * w or w = r * v )
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  ( v = r * w or w = r * v ) ; ::_thesis: verum
end;
supposeA4: - s = 0 ; ::_thesis: ex r being Real st
( v = r * w or w = r * v )
take  - s ; ::_thesis: ( v = (- s) * w or w = (- s) * v )
thus  ( v = (- s) * w or w = (- s) * v ) by A2, A4, RLVECT_1:def_8; ::_thesis: verum
end;
end;
end;