set f = the Lipschitzian linear-Functional of X;
the Lipschitzian linear-Functional of X in BoundedLinearFunctionals X by Def9;
hence not BoundedLinearFunctionals X is empty ; :: thesis: verum