for B being B_Lattice
for FB being Filter of B holds B /\/ FB is B_Lattice