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

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