reconsider C = ContinuousFunctions (X,Y) as Subset of (R_NormSpace_of_BoundedFunctions (X,Y)) ;
C is closed by Lm5;
hence ex b₁ being Subset of (R_NormSpace_of_BoundedFunctions (X,Y)) st b₁ is closed ; :: thesis: verum