theorem :: WAYBEL_7:37

for L being continuous LATTICE st Top L is compact holds
( ( for A being non empty finite Subset of L st inf A << Top L holds
ex a being Element of L st
( a in A & a <= Top L ) ) & uparrow (fininfs ((downarrow (Top L)) `)) meets waybelow (Top L) )