:: deftheorem Def5 defines value_of MMLQUER2:def 5 :
for X being set
for f being Function of X,NAT
for b₃ being Relation of X holds
( b₃ = value_of f iff for x, y being set holds
( x,y in b₃ iff ( x in X & y in X & f . x < f . y ) ) );