:: deftheorem TDis defines ternary-distributive LATTBA_1:def 3 :
for T being non empty TBAStruct holds
( T is ternary-distributive iff for a, b, c, d, e being Element of T holds Tern ((Tern (a,b,c)),d,(Tern (a,b,e))) = Tern (a,b,(Tern (c,d,e))) );