theorem :: CC0SP1:4

for X being non empty set holds C_Algebra_of_BoundedFunctions X is ComplexSubAlgebra of CAlgebra X by Th2;