theorem :: WAYBEL_4:24

for L being non empty upper-bounded Poset holds uparrow (Top L) = {(Top L)}