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