set f = the carrier of X --> 0;
reconsider f = the carrier of X --> 0 as linear-Functional of X by DUALSP01:9;
f is Lipschitzian by Th21X;
hence ex b₁ being linear-Functional of X st b₁ is Lipschitzian ; :: thesis: verum