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 CLOPBAN1:def 7; :: thesis: verum