let X be LinearTopSpace; :: thesis: for x being Point of X
for O being local_base of X
for B being Subset-Family of X st B = { (x + U) where U is Subset of X : ( U in O & U is a_neighborhood of 0. X ) } holds
B is basis of (BOOL2F (NeighborhoodSystem x))
let x be Point of X; :: thesis: for O being local_base of X
for B being Subset-Family of X st B = { (x + U) where U is Subset of X : ( U in O & U is a_neighborhood of 0. X ) } holds
B is basis of (BOOL2F (NeighborhoodSystem x))
let O be local_base of X; :: thesis: for B being Subset-Family of X st B = { (x + U) where U is Subset of X : ( U in O & U is a_neighborhood of 0. X ) } holds
B is basis of (BOOL2F (NeighborhoodSystem x))
let B be Subset-Family of X; :: thesis: ( B = { (x + U) where U is Subset of X : ( U in O & U is a_neighborhood of 0. X ) } implies B is basis of (BOOL2F (NeighborhoodSystem x)) )
assume A1: B = { (x + U) where U is Subset of X : ( U in O & U is a_neighborhood of 0. X ) } ; :: thesis: B is basis of (BOOL2F (NeighborhoodSystem x))
set F = BOOL2F (NeighborhoodSystem x);
A2: BOOL2F (NeighborhoodSystem x) c= <.B.]

proof

now :: thesis: for t being object st t in BOOL2F (NeighborhoodSystem x) holds
t in <.B.]

let t be object ; :: thesis: ( t in BOOL2F (NeighborhoodSystem x) implies t in <.B.] )
assume t in BOOL2F (NeighborhoodSystem x) ; :: thesis: t in <.B.]
then t in NeighborhoodSystem x by CARDFIL2:def 20;
then t in { A where A is a_neighborhood of x : verum } by YELLOW19:def 1;
then consider A being a_neighborhood of x such that
A3: t = A ;
x in Int A by CONNSP_2:def 1;
then (- x) + (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
A4: V in O and
A5: V c= (- x) + (Int A) by YELLOW13:def 2;
set U = x + V;
A6: x + V in B by A1, A4;
x + V c= x + ((- x) + (Int A)) by A5, RLTOPSP1:8;
then x + V c= (x + (- x)) + (Int A) by RLTOPSP1:6;
then x + V c= (0. X) + (Int A) by RLVECT_1:5;
then ( Int A c= A & x + V c= Int A ) by RLTOPSP1:5, TOPS_1:16;
then x + V c= A ;
hence t in <.B.] by A3, A6, CARDFIL2:def 8; :: thesis: verum

end;

hence BOOL2F (NeighborhoodSystem x) c= <.B.] ; :: thesis: verum

end;

<.B.] c= BOOL2F (NeighborhoodSystem x)

proof

now :: thesis: for t being object st t in <.B.] holds
t in BOOL2F (NeighborhoodSystem x)

let t be object ; :: thesis: ( t in <.B.] implies t in BOOL2F (NeighborhoodSystem x) )
assume A7: t in <.B.] ; :: thesis: t in BOOL2F (NeighborhoodSystem x)
then reconsider t1 = t as Subset of X ;
consider b being Element of B such that
A8: b c= t1 by A7, CARDFIL2:def 8;
set v0 = the Element of O;
not B is empty by A1, Lm2;
then b in B ;
then consider U1 being Subset of X such that
A9: b = x + U1 and
U1 in O and
A10: U1 is a_neighborhood of 0. X by A1;
reconsider t2 = b as Element of B ;
A11: x + (0. X) in x + (Int U1) by Lm1, A10, CONNSP_2:def 1;
x + (Int U1) c= Int (x + U1) by RLTOPSP1:37;
then t2 is a_neighborhood of x by A9, A11, CONNSP_2:def 1;
then t2 in { A where A is a_neighborhood of x : verum } ;
then t2 in NeighborhoodSystem x by YELLOW19:def 1;
then t2 in BOOL2F (NeighborhoodSystem x) by CARDFIL2:def 20;
hence t in BOOL2F (NeighborhoodSystem x) by A8, CARD_FIL:def 1; :: thesis: verum

end;

hence <.B.] c= BOOL2F (NeighborhoodSystem x) ; :: thesis: verum

end;

hence B is basis of (BOOL2F (NeighborhoodSystem x)) by CARDFIL2:22, A2, XBOOLE_0:def 10; :: thesis: verum