theorem Th5: :: WAYBEL14:5

for L being non empty antisymmetric complete RelStr
for X being lower Subset of L st sup X in X holds
X = downarrow (sup X)