for X, Y being ComplexNormSpace holds
( C_NormSpace_of_BoundedLinearOperators (X,Y) is reflexive & C_NormSpace_of_BoundedLinearOperators (X,Y) is discerning & C_NormSpace_of_BoundedLinearOperators (X,Y) is ComplexNormSpace-like )