cluster non zero Element of REAL ;
existence
not for b₁ being Real holds b₁ is empty

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 )

let X be RealLinearSpace;
let M be empty Subset of X;
cluster conv M -> empty ;
coherence
conv M is empty

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

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 )

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

let V be non empty RLSStruct ;
cluster non empty convex-membered Element of bool (bool the carrier of V);
existence
ex b₁ being Subset-Family of V st
( not b₁ is empty & b₁ is convex-membered )

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 ;

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

let X be RealLinearSpace;
cluster non empty symmetric Element of bool the carrier of X;
existence
ex b₁ being Subset of X st
( not b₁ is empty & b₁ is symmetric )

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

let X be non empty RLSStruct ;
cluster {} X -> circled ;
coherence
{} X is circled by Lm6;

let X be RealLinearSpace;
cluster non empty circled Element of bool the carrier of X;
existence
ex b₁ being Subset of X st
( not b₁ is empty & b₁ is circled )

let X be RealLinearSpace;
let A, B be circled Subset of X;
cluster A + B -> circled ;
coherence
A + B is circled by Lm7;

let X be RealLinearSpace;
cluster circled -> symmetric Element of bool the carrier of X;
coherence
for b₁ being Subset of X st b₁ is circled holds
b₁ is symmetric by Lm8;

let X be RealLinearSpace;
let M be circled Subset of X;
cluster conv M -> symmetric circled ;
coherence
conv M is circled by Lm9;

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

let V be non empty RLSStruct ;
cluster non empty circled-membered Element of bool (bool the carrier of V);
existence
ex b₁ being Subset-Family of V st
( not b₁ is empty & b₁ is circled-membered )

attr c₁ is strict;
struct RLTopStruct -> RLSStruct , TopStruct ;
aggr RLTopStruct(# carrier, Zero, add, Mult, topology #) -> RLTopStruct ;

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 by STRUCT_0:def 1;

cluster non empty strict RLTopStruct ;
existence
ex b₁ being RLTopStruct st
( b₁ is strict & not b₁ is empty )

let X be non empty RLTopStruct ;
attr X 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 );
attr X 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 ) );

cluster non empty TopSpace-like Abelian add-associative right_zeroed right_complementable RealLinearSpace-like strict add-continuous Mult-continuous RLTopStruct ;
existence
ex b₁ being non empty RLTopStruct st
( b₁ is strict & b₁ is add-continuous & b₁ is Mult-continuous & b₁ is TopSpace-like & b₁ is Abelian & b₁ is add-associative & b₁ is right_zeroed & b₁ is right_complementable & b₁ is RealLinearSpace-like )

mode LinearTopSpace is non empty TopSpace-like Abelian add-associative right_zeroed right_complementable RealLinearSpace-like add-continuous Mult-continuous RLTopStruct ;

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 b₁ being Function of X,X st
for x being Point of X holds b₁ . x = a + x uniqueness
for b₁, b₂ being Function of X,X st ( for x being Point of X holds b₁ . x = a + x ) & ( for x being Point of X holds b₂ . x = a + x ) holds
b₁ = b₂

let X be LinearTopSpace;
let a be Point of X;
cluster transl a,X -> being_homeomorphism ;
coherence
transl a,X is being_homeomorphism

let X be LinearTopSpace;
let E be open Subset of X;
let x be Point of X;
cluster x + E -> open ;
coherence
x + E is open by Lm12;

let X be LinearTopSpace;
let E be open Subset of X;
let K be Subset of X;
cluster K + E -> open ;
coherence
K + E is open by Lm13;

let X be LinearTopSpace;
let D be closed Subset of X;
let x be Point of X;
cluster x + D -> closed ;
coherence
x + D is closed by Lm14;

let X be non empty RLTopStruct ;
mode local_base of X is basis of 0. X;

let X be non empty RLTopStruct ;
attr X is locally-convex means :Def11: :: RLTOPSP1:def 11
ex P being local_base of X st P is convex-membered;

let X be LinearTopSpace;
let E be Subset of X;
attr E 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 ) );

let X be LinearTopSpace;
cluster {} X -> symmetric circled bounded ;
coherence
{} X is bounded

let X be LinearTopSpace;
cluster bounded Element of bool the carrier of X;
existence
ex b₁ being Subset of X st b₁ is bounded

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 b₁ being Function of X,X st
for x being Point of X holds b₁ . x = r * x uniqueness
for b₁, b₂ being Function of X,X st ( for x being Point of X holds b₁ . x = r * x ) & ( for x being Point of X holds b₂ . x = r * x ) holds
b₁ = b₂

let X be LinearTopSpace;
let r be non zero Real;
cluster mlt r,X -> being_homeomorphism ;
coherence
mlt r,X is being_homeomorphism

let X be LinearTopSpace;
let V be bounded Subset of X;
let r be Real;
cluster r * V -> bounded ;
coherence
r * V is bounded by Lm17;

cluster being_T1 -> Hausdorff RLTopStruct ;
coherence
for b₁ being LinearTopSpace st b₁ is being_T1 holds
b₁ is being_T2

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

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

let X be LinearTopSpace;
let B be circled Subset of X;
cluster Cl B -> symmetric circled ;
coherence
Cl B is circled by Lm20;

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