theorem :: FILTER_0:60

for L being Lattice
for p being Element of L st L is B_Lattice holds
latt <.p.) is B_Lattice