theorem TopTBA: :: LATTBA_1:17

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