:: deftheorem defines BA2TBAA LATTBA_1:def 14 :
for B being Boolean Lattice holds BA2TBAA B = TBALattStr(# the carrier of B, the L_join of B, the L_meet of B,(comp B),(RosTrn B) #);