theorem Th14: :: CC0SP2:14

for X being non empty TopSpace holds 1_ (C_Algebra_of_ContinuousFunctions X) = X --> 1r