:: deftheorem Def8 defines REAL? FRECHET:def 8 :
for b₁ being non empty strict TopSpace holds
( b₁ = REAL? iff ( the carrier of b₁ = (REAL \ NAT) \/ {REAL} & ex f being Function of R^1,b₁ st
( f = (id REAL) +* (NAT --> REAL) & ( for A being Subset of b₁ holds
( A is closed iff f " A is closed ) ) ) ) );