theorem Th7: :: WAYBEL_8:7

for L being LATTICE holds
( L is algebraic iff ( L is continuous & ( for x, y being Element of L st x << y holds
ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x <= k & k <= y ) ) ) )