set f = the Lipschitzian linear-Functional of X;
the Lipschitzian linear-Functional of X in BoundedLinearFunctionals X by Def10;
hence ( not BoundedLinearFunctionals X is empty & BoundedLinearFunctionals X is linearly-closed ) by Th17; :: thesis: verum