theorem :: CC0SP2:9

for X being non empty TopSpace holds C_Algebra_of_ContinuousFunctions X is ComplexSubAlgebra of CAlgebra the carrier of X by CC0SP1:2;