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