:: deftheorem defines tern ALGSTR_3:def 4 :
for a, b, c being Scalar of TernaryFieldEx holds tern (a,b,c) = the TernOp of TernaryFieldEx . (a,b,c);