:: deftheorem Def20 defines gen_NS_R^1 FINTOPO8:def 20 :
for b₁ being Function of the carrier of FMT_R^1,(bool (bool the carrier of FMT_R^1)) holds
( b₁ = gen_NS_R^1 iff for r being Real ex x being Point of (TopSpaceMetr RealSpace) st
( x = r & b₁ . r = Balls x ) );