:: deftheorem Def4 defines basis YELLOW13:def 4 :
for T being TopStruct
for b₂ being Subset-Family of T holds
( b₂ is basis of T iff for p being Point of T holds b₂ is basis of p );