:: deftheorem defines Banach_Algebra-like LOPBAN_2:def 12 :
for X being Normed_Algebra holds
( X is Banach_Algebra-like iff ( X is Banach_Algebra-like_1 & X is Banach_Algebra-like_2 & X is Banach_Algebra-like_3 & X is left_unital & X is left-distributive & X is complete ) );