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