theorem Th18: :: CC0SP1:18

for X being non empty set holds X --> 0 = 0. (C_Normed_Algebra_of_BoundedFunctions X)