theorem :: WAYBEL31:15

for L1 being non empty Poset
for A being Subset of L1
for a being Element of L1 st a in uparrow A holds
Way_Up (a,A) = {}