set f = the carrier of X --> 0;
reconsider f = the carrier of X --> 0 as Function of the carrier of X,REAL by FUNCOP_1:45, XREAL_0:def 1;
reconsider f = f as Functional of X ;
reconsider f = f as linear-Functional of X by Th21X;
f is Lipschitzian by Th21X;
hence ex b₁ being linear-Functional of X st b₁ is Lipschitzian ; :: thesis: verum