:: deftheorem defines BA2TBA LATTBA_1:def 13 :
for B being Boolean Lattice holds BA2TBA B = TBAStruct(# the carrier of B,(comp B),(RosTrn B) #);