:: deftheorem defines is_maximal_in ORDERS_1:def 12 :
for R being Relation
for x being set holds
( x is_maximal_in R iff ( x in field R & ( for y being set holds
( not y in field R or not y <> x or not [x,y] in R ) ) ) );