let X be LinearTopSpace; :: thesis: for O being local_base of X

for a being Point of X

for P being Subset-Family of X st P = { (a + U) where U is Subset of X : U in O } holds

P is basis of a

let O be basis of 0. X; :: thesis: for a being Point of X

for P being Subset-Family of X st P = { (a + U) where U is Subset of X : U in O } holds

P is basis of a

let a be Point of X; :: thesis: for P being Subset-Family of X st P = { (a + U) where U is Subset of X : U in O } holds

P is basis of a

let P be Subset-Family of X; :: thesis: ( P = { (a + U) where U is Subset of X : U in O } implies P is basis of a )

assume A1: P = { (a + U) where U is Subset of X : U in O } ; :: thesis: P is basis of a

let A be a_neighborhood of a; :: according to YELLOW13:def 2 :: thesis: ex b_{1} being a_neighborhood of a st

( b_{1} in P & b_{1} c= A )

a in Int A by CONNSP_2:def 1;

then (- a) + (Int A) is a_neighborhood of 0. X by RLTOPSP1:9, CONNSP_2:3;

then consider V being a_neighborhood of 0. X such that

A2: V in O and

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

take U = a + V; :: thesis: ( U is a_neighborhood of a & U in P & U c= A )

A4: a + (0. X) in a + (Int V) by Lm1, CONNSP_2:def 1;

a + (Int V) c= Int U by RLTOPSP1:37;

hence U is a_neighborhood of a 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= a + ((- a) + (Int A)) by A3, RLTOPSP1:8;

then U c= (a + (- a)) + (Int A) by RLTOPSP1:6;

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

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

hence U c= A ; :: thesis: verum

for a being Point of X

for P being Subset-Family of X st P = { (a + U) where U is Subset of X : U in O } holds

P is basis of a

let O be basis of 0. X; :: thesis: for a being Point of X

for P being Subset-Family of X st P = { (a + U) where U is Subset of X : U in O } holds

P is basis of a

let a be Point of X; :: thesis: for P being Subset-Family of X st P = { (a + U) where U is Subset of X : U in O } holds

P is basis of a

let P be Subset-Family of X; :: thesis: ( P = { (a + U) where U is Subset of X : U in O } implies P is basis of a )

assume A1: P = { (a + U) where U is Subset of X : U in O } ; :: thesis: P is basis of a

let A be a_neighborhood of a; :: according to YELLOW13:def 2 :: thesis: ex b

( b

a in Int A by CONNSP_2:def 1;

then (- a) + (Int A) is a_neighborhood of 0. X by RLTOPSP1:9, CONNSP_2:3;

then consider V being a_neighborhood of 0. X such that

A2: V in O and

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

take U = a + V; :: thesis: ( U is a_neighborhood of a & U in P & U c= A )

A4: a + (0. X) in a + (Int V) by Lm1, CONNSP_2:def 1;

a + (Int V) c= Int U by RLTOPSP1:37;

hence U is a_neighborhood of a 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= a + ((- a) + (Int A)) by A3, RLTOPSP1:8;

then U c= (a + (- a)) + (Int A) by RLTOPSP1:6;

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

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

hence U c= A ; :: thesis: verum