let X be non empty compact TopSpace; :: thesis: C_Algebra_of_ContinuousFunctions X is ComplexSubAlgebra of C_Algebra_of_BoundedFunctions the carrier of X
A1: the carrier of (C_Algebra_of_ContinuousFunctions X) c= the carrier of (C_Algebra_of_BoundedFunctions the carrier of X) by Lm1;
A2: C_Algebra_of_ContinuousFunctions X is ComplexSubAlgebra of CAlgebra the carrier of X by CC0SP1:2;
C_Algebra_of_BoundedFunctions the carrier of X is ComplexSubAlgebra of CAlgebra the carrier of X by CC0SP1:4;
hence C_Algebra_of_ContinuousFunctions X is ComplexSubAlgebra of C_Algebra_of_BoundedFunctions the carrier of X by A1, A2, Th15; :: thesis: verum