:: deftheorem defines is_superior_of ORDERS_1:def 14 :
for R being Relation
for x being set holds
( x is_superior_of R iff ( x in field R & ( for y being set st y in field R & y <> x holds
[y,x] in R ) ) );