:: deftheorem defines is_maximal_wrt WAYBEL_4:def 23 :
for X being set
for x being object
for R being Relation holds
( x is_maximal_wrt X,R iff ( x in X & ( for y being set holds
( not y in X or not y <> x or not [x,y] in R ) ) ) );