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_{1} being linear-Functional of X st b_{1} is Lipschitzian
; :: thesis: verum

reconsider f = the carrier of X --> 0 as linear-Functional of X by DUALSP01:9;

f is Lipschitzian by Th21X;

hence ex b