:: deftheorem defines UpperCone ORDERS_2:def 8 :
for A being non empty Poset
for S being Subset of A holds UpperCone S = { a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a2 < a1 } ;