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