theorem Th27: :: FILTER_2:27

for L being Lattice holds the carrier of L is Ideal of L