:: deftheorem Def9 defines resource MMLQUER2:def 9 :
for X being set
for A being FinSequence
for f being Function
for b₄ being Relation of X holds
( b₄ = resource (X,A,f) iff for x, y being set holds
( x,y in b₄ iff ( x in X & y in X & A <- (f . x) <> 0 & ( A <- (f . x) < A <- (f . y) or A <- (f . y) = 0 ) ) ) );