id the carrier of X is bounded LinearOperator of X,X by Th3;
hence id the carrier of X is Element of BoundedLinearOperators X,X by CLOPBAN1:def 8; :: thesis: verum