set X = the non trivial RealBanachSpace;
take R_Normed_Algebra_of_BoundedLinearOperators the non trivial RealBanachSpace ; :: thesis: R_Normed_Algebra_of_BoundedLinearOperators the non trivial RealBanachSpace is Banach_Algebra-like
thus R_Normed_Algebra_of_BoundedLinearOperators the non trivial RealBanachSpace is Banach_Algebra-like ; :: thesis: verum