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