theorem Th7: :: LATTICE4:7

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