:: deftheorem Def5 defines Ternary-Field-like ALGSTR_3:def 5 :
for IT being non empty TernaryFieldStr holds
( IT is Ternary-Field-like iff ( 0. IT <> 1. IT & ( for a being Scalar of IT holds Tern (a,(1. IT),(0. IT)) = a ) & ( for a being Scalar of IT holds Tern ((1. IT),a,(0. IT)) = a ) & ( for a, b being Scalar of IT holds Tern (a,(0. IT),b) = b ) & ( for a, b being Scalar of IT holds Tern ((0. IT),a,b) = b ) & ( for u, a, b being Scalar of IT ex v being Scalar of IT st Tern (u,a,v) = b ) & ( for u, a, v, v9 being Scalar of IT st Tern (u,a,v) = Tern (u,a,v9) holds
v = v9 ) & ( for a, a9 being Scalar of IT st a <> a9 holds
for b, b9 being Scalar of IT ex u, v being Scalar of IT st
( Tern (u,a,v) = b & Tern (u,a9,v) = b9 ) ) & ( for u, u9 being Scalar of IT st u <> u9 holds
for v, v9 being Scalar of IT ex a being Scalar of IT st Tern (u,a,v) = Tern (u9,a,v9) ) & ( for a, a9, u, u9, v, v9 being Scalar of IT st Tern (u,a,v) = Tern (u9,a,v9) & Tern (u,a9,v) = Tern (u9,a9,v9) & not a = a9 holds
u = u9 ) ) );