let X be non empty compact TopSpace; :: thesis: R_Algebra_of_ContinuousFunctions X is Subalgebra of R_Algebra_of_BoundedFunctions the carrier of X
A1: the carrier of (R_Algebra_of_ContinuousFunctions X) c= the carrier of (R_Algebra_of_BoundedFunctions the carrier of X) by Lm1;
A2: R_Algebra_of_ContinuousFunctions X is Subalgebra of RAlgebra the carrier of X by C0SP1:6;
R_Algebra_of_BoundedFunctions the carrier of X is Subalgebra of RAlgebra the carrier of X by C0SP1:10;
hence R_Algebra_of_ContinuousFunctions X is Subalgebra of R_Algebra_of_BoundedFunctions the carrier of X by A1, A2, Th8; :: thesis: verum