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.]

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

end;

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

t in <.B.]

hence
BOOL2F (NeighborhoodSystem x) c= <.B.]
; :: thesis: verumt 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;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

proof

end;

hence
B is basis of (BOOL2F (NeighborhoodSystem x))
by CARDFIL2:22, A2, XBOOLE_0:def 10; :: thesis: verumnow :: thesis: for t being object st t in <.B.] holds

t in BOOL2F (NeighborhoodSystem x)

hence
<.B.] c= BOOL2F (NeighborhoodSystem x)
; :: thesis: verumt 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;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