:: deftheorem defines ContinuousFunctions C0SP2:def 2 :
for X being non empty TopSpace holds ContinuousFunctions X = { f where f is continuous RealMap of X : verum } ;