:: deftheorem defines first-countable FRECHET:def 2 :
for T being non empty TopStruct holds
( T is first-countable iff for x being Point of T ex B being Basis of x st B is countable );