theorem Th29: :: WAYBEL_8:29

for X being set
for x being Element of (BoolePoset X) holds compactbelow x = { y where y is finite Subset of x : verum }