set L = BA2TBAA B;
the L_join of B absorbs the L_meet of B by LATTICE2:26;
hence BA2TBAA B is Lattice-like by LATTICE2:11, LATTICE2:27; :: thesis: verum