theorem :: FILTER_2:75

for L being Lattice
for I being Ideal of L st L is lower-bounded holds
latt (L,I) is lower-bounded