theorem :: FILTER_1:61

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