theorem Th21: :: FILTER_2:21

for L being Lattice
for D being non empty Subset of L holds
( D is Ideal of L iff ( ( for p, q being Element of L st p in D & q in D holds
p "\/" q in D ) & ( for p, q being Element of L st p in D & q [= p holds
q in D ) ) )