let X be LinearTopSpace; :: thesis: NeighborhoodSystem (0. X) is local_base of X

reconsider p = 0. X as Point of X ;

BOOL2F (NeighborhoodSystem (0. X)) is Subset-Family of X ;

then reconsider NS0 = NeighborhoodSystem (0. X) as Subset-Family of X by CARDFIL2:def 20;

for A being a_neighborhood of p ex P being a_neighborhood of p st

( P in NeighborhoodSystem p & P c= A ) by YELLOW19:2;

then NS0 is basis of p by YELLOW13:def 2;

hence NeighborhoodSystem (0. X) is local_base of X ; :: thesis: verum

reconsider p = 0. X as Point of X ;

BOOL2F (NeighborhoodSystem (0. X)) is Subset-Family of X ;

then reconsider NS0 = NeighborhoodSystem (0. X) as Subset-Family of X by CARDFIL2:def 20;

for A being a_neighborhood of p ex P being a_neighborhood of p st

( P in NeighborhoodSystem p & P c= A ) by YELLOW19:2;

then NS0 is basis of p by YELLOW13:def 2;

hence NeighborhoodSystem (0. X) is local_base of X ; :: thesis: verum