:: deftheorem defines TBA2BA LATTBA_1:def 10 :
for T being Ternary_Boolean_Algebra
for x being Element of T holds TBA2BA (T,x) = LattStr(# the carrier of T,(JoinTBA (T,x)),(MeetTBA (T,x)) #);