theorem :: WAYBEL31:18

for L1 being non empty complete Poset
for x being Element of L1 st x is compact holds
x = inf (wayabove x)