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

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