id the carrier of X is Lipschitzian LinearOperator of X,X
by Th3;

hence id the carrier of X is Element of BoundedLinearOperators (X,X) by LOPBAN_1:def 9; :: thesis: verum

hence id the carrier of X is Element of BoundedLinearOperators (X,X) by LOPBAN_1:def 9; :: thesis: verum