:: deftheorem defines Banach_Algebra-like_1 LOPBAN_2:def 9 :
for X being non empty Normed_AlgebraStr holds
( X is Banach_Algebra-like_1 iff for x, y being Element of X holds ||.(x * y).|| <= ||.x.|| * ||.y.|| );