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 b₁ being a_neighborhood of p st
( b₁ in P & b₁ 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) ;
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 ; :: thesis: verum