:: deftheorem defines satisfying_TBA1 LATTBA_1:def 15 :
for T being non empty TBAStruct holds
( T is satisfying_TBA1 iff for x, y, z, u, v, v6, w being Element of T holds Tern ((Tern (x,(x `),y)),((Tern ((Tern (z,u,v)),w,(Tern (z,u,v6)))) `),(Tern (u,(Tern (v6,w,v)),z))) = y );