theorem :: FILTER_2:85

for L being Lattice
for p, q being Element of L st L is B_Lattice & p [= q holds
latt (L,[#p,q#]) is B_Lattice