theorem :: FILTER_1:20

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