:: deftheorem Def2 defines ternaryreal ALGSTR_3:def 2 :
for b₁ being TriOp of REAL holds
( b₁ = ternaryreal iff for a, b, c being Real holds b₁ . (a,b,c) = (a * b) + c );