for B being B_Lattice
for a being Element of B holds B,[:(B /\/ <.a.)),(latt <.a.)):] are_isomorphic