theorem Th9: :: CC0SP1:9

for X being non empty set holds 1_ (C_Algebra_of_BoundedFunctions X) = X --> 1r