theorem Th16: :: C0SP1:16

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