:: deftheorem defines basis YELLOW13:def 2 :
for T being non empty TopSpace
for p being Point of T
for b₃ being Subset-Family of T holds
( b₃ is basis of p iff for A being a_neighborhood of p ex P being a_neighborhood of p st
( P in b₃ & P c= A ) );