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₁ being a_neighborhood of a st
( b₁ in P & b₁ 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