:: deftheorem Def1 defines basis YELLOW13:def 1 :
for T being TopStruct
for p being Point of T
for b₃ being Subset-Family of T holds
( b₃ is basis of p iff for A being Subset of T st p in Int A holds
ex P being Subset of T st
( P in b₃ & p in Int P & P c= A ) );