for T being Ternary_Boolean_Algebra
for p being Element of T holds Bottom LattStr(# the carrier of (TBA2BA (T,p)), the L_join of (TBA2BA (T,p)), the L_meet of (TBA2BA (T,p)) #) = p `