:: deftheorem TLIDef defines ternary-left-idempotent LATTBA_1:def 4 :
for T being non empty TBAStruct holds
( T is ternary-left-idempotent iff for a, b being Element of T holds Tern (b,b,a) = b );