theorem :: ORDERS_2:22

for A being non empty Poset
for a, c being Element of A holds
( c < a iff a in UpperCone {c} )