theorem Th29: :: WAYBEL30:29

for S being Scott meet-continuous TopLattice
for F being finite Subset of S holds Int (uparrow F) c= union { (wayabove x) where x is Element of S : x in F }